Frama-C 30

[AllanBlanchard]

• Org

  • [x] 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

  • [x] Update Alt-Ergo version ( + see https://github.com/OCamlPro/alt-ergo/issues/505)
  • [x] Update tools versions (9f909866e4fad567820f92ad0266e6e301310aaf)

• Update acknowledgment

  • [x] Costava (8e0444313225da2bbd7be74c75f0cb245360fe2a)

• Vocab (#44)

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

• Images

  • [x] fix link to frama-c logo on ZdS

• Contracts

  • [x] #42 (#45)
  • [x] #49
  • [x] Add an explanation about main somewhere (https://stackoverflow.com/questions/72812151/why-does-wp-care-about-main) (https://github.com/AllanBlanchard/tutoriel_wp/pull/51)
  • [x] Talk about exits and terminates (https://github.com/AllanBlanchard/tutoriel_wp/pull/67)

• WP calculus

  • [x] mention that WP does not build a single formula https://github.com/AllanBlanchard/tutoriel_wp/pull/59
  • [x] explain rules for assert, admit, check https://github.com/AllanBlanchard/tutoriel_wp/pull/58
  • [x] + corresponding loop invariant and new loop invariant computation, https://github.com/AllanBlanchard/tutoriel_wp/pull/58
  • [x] + corresponding check and admit for function contracts (#64)
  • [x] + explain how to write loop annotations and order invariants (https://github.com/AllanBlanchard/tutoriel_wp/pull/61)
  • [x] + apply guidance on loops-examples https://github.com/AllanBlanchard/tutoriel_wp/pull/60
  • [x] + check examples https://github.com/AllanBlanchard/tutoriel_wp/pull/60
  • [x] variant : introduce measure + general measure and (partially) drop induction (https://github.com/AllanBlanchard/tutoriel_wp/pull/55)
  • [x] terminates + decreases (#43)
  • [x] explain exits (https://github.com/AllanBlanchard/tutoriel_wp/pull/67)
  • [x] rework section on termination (https://github.com/AllanBlanchard/tutoriel_wp/pull/67)
  • [x] remove explanations about the additional WP options that have been removed in 28 (https://github.com/AllanBlanchard/tutoriel_wp/pull/67)
  • [x] rework exercise on termination (https://github.com/AllanBlanchard/tutoriel_wp/pull/67)

• Predicates

  • [x] fix unchanged-loc screen (0dcb27e6778b646253fb6b3b8c548592a9cdc6a2)

• Functions

  • [x] check auto linear (linear-1.c)

• Lemmas

  • [x] change explanations for linear, Alt-Ergo proves everything OK with 2.4.3
  • [x] add check lemma https://github.com/AllanBlanchard/tutoriel_wp/pull/58

• Inductive

  • [x] fix even example (https://github.com/AllanBlanchard/tutoriel_wp/pull/53)

• Axiomatic

  • [x] detail lemmas in EX3
  • [x] explain clusters (https://github.com/AllanBlanchard/tutoriel_wp/pull/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"