Frama-C 30

[AllanBlanchard]

• Org

  • Remove old markdown version from directory
  • Create new part "Improving confidence"
    • move minimal contracts here
    • add a section about specification testing
    • before proof methodology
  • add section on Why3 drivers in proof methodology ?
  • Use the new GUI
    • update installation part
    • update all screens

• General

  • Update Alt-Ergo version ( + see Proof performance regressions from 2.4.0 to 2.4.1+ OCamlPro/alt-ergo#505)
  • Update tools versions (9f90986)

• Update acknowledgment

  • Costava (8e04443)

• Vocab (Spell checking + changes some definitions #44)

  • respects specification vs. conforms to its specification
  • proof obligation vs. verification condition

• Images

  • fix link to frama-c logo on ZdS

• Contracts

  • Question about order3 #42 (Order 3 - Removes useless ensures #45)
  • Small typo in chapter 3 of the English version (page 29 in the PDF) #49
  • Add an explanation about main somewhere
    (https://stackoverflow.com/questions/72812151/why-does-wp-care-about-main)
    (New content: requires of main #51)
  • Talk about exits and terminates (WP now populates terminates exits #67)

• WP calculus

  • mention that WP does not build a single formula New content: WP vs Disjkstra WP #59
  • explain rules for assert, admit, check New-content: Check, admit and variations over loops and lemmas #58
  • + corresponding loop invariant and new loop invariant computation, New-content: Check, admit and variations over loops and lemmas #58
  • + corresponding check and admit for function contracts (New content: admit and check for requires and ensures #64)
  • + explain how to write loop annotations and order invariants (New content: Building loop annotations #61)
  • + apply guidance on loops-examples Minor changes in loops #60
  • + check examples Minor changes in loops #60
  • variant : introduce measure + general measure and (partially) drop induction
    (New content: measures #55)
  • terminates + decreases (New content : termination #43)
  • explain exits (WP now populates terminates exits #67)
  • rework section on termination (WP now populates terminates exits #67)
  • remove explanations about the additional WP options that have been removed in 28 (WP now populates terminates exits #67)
  • rework exercise on termination (WP now populates terminates exits #67)

• Predicates

  • fix unchanged-loc screen (0dcb27e)

• Functions

  • check auto linear (linear-1.c)

• Lemmas

  • change explanations for linear, Alt-Ergo proves everything OK with 2.4.3
  • add check lemma New-content: Check, admit and variations over loops and lemmas #58

• Inductive

  • fix even example (Fix content: better explanations in inductive #53)

• Axiomatic

  • detail lemmas in EX3
  • explain clusters (New content: axiomatic cluster #52)

• Minimal contracts

  • search +1 proved

• Triggering lemmas

  • reminder on assert etc.
  • update displayed VC.

• Lemma functions

  • screen ghost-code-usage-2 to update

[clouetm]

In section "4.1.1.1. Affectation de valeurs pointées", missing newline after "précondition à notre programme précédent :"

[clouetm]

In section "4.3.2. Exemple avec un tableau en lecture seule", missing part of the code in the example

[clouetm]

In section "4.3.2. Exemple avec un tableau en lecture seule", wrong code for the "invariant de boucle final"

[clouetm]

In "4.4.2. Fonctions récursives", change in the code // no verification needed, s in not in the cluster by // no verification needed, single in not in the cluster

[clouetm]

Typo in "5.1. Types primitifs supplémentaires" (ìntto int)

[clouetm]

Text overflows off page in section "7.3.4. Limitations" with element_level_sorted_is_sorted

[clouetm]

In "8.1.2. Avec la preuve déductive": "Why3 peut par extraire des conditions de vérification vers Coq"