allanblanchard/tutoriel_wp

Frama-C and WP tutorial

About this tutorial

Frama-C (FRAmework for Modular Analysis of C programs) is a set of interoperable program analyzers for C programs. I have used this software during all my PhD thesis and after, mostly for deductive proof using the WP plugin. So, I wrote a tutorial that allows to learn ACSL (the specification language of Frama-C) and the use of WP by practice, also getting some theorical rudiments about deductive proof.

It can be used for both learning and teaching, I hope you will have some fun with it :) .

The last version is available on my website in English and in French.

An online French version is available on Zeste de Savoir.

Building

In order to build the files, you can use docker

docker build -t tutoriel_wp .
docker run --rm -v $PWD:/mnt -w /mnt tutoriel_wp make

tutoriel_wp's Issues

Quelques coquilles

Bonjour,

Voilà les quelques questions ou remarques sur le document :

tutoriel_wp/french/statements/function-calls.tex

Line 66 in ab0b3b7

dans la postcondition est \CodeInline{*a} au label \CodeInline{L2}. Par conséquent,

Est-ce que ce ne devrait pas plutôt être "*a + 1 au label L2" ?

https://github.com/AllanBlanchard/tutoriel_wp/blob/master/french/acsl-properties/lemmas.tex#L154

"au sens que chaque élément soit plus ..."

https://github.com/AllanBlanchard/tutoriel_wp/blob/master/french/acsl-logic-definitions.tex#L12

"ces 3 notions" ou "2 définitions", peut-être.

https://github.com/AllanBlanchard/tutoriel_wp/blob/master/french/proof-methodologies/lemma-functions.tex#L515

Répétition de "la plupart du temps" mais c'est un détail.

J'avais d'autres remarques plus importantes mais je me suis rendu compte qu'elles étaient déjà prises en compte sur git !

Add a script to check all examples

Frama-C 29

• 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 OCamlPro/alt-ergo#505)
  • Update tools versions (9f90986)

• Update acknowledgment

  • Costava (8e04443)

• Vocab (#44)

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

• Images

  • fix link to frama-c logo on ZdS

• Contracts

  • #42 (#45)
  • #49
  • Add an explanation about main somewhere
    (https://stackoverflow.com/questions/72812151/why-does-wp-care-about-main)
    (#51)
  • Talk about exits
  • Talk about terminates

• WP calculus

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

• 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 #58

• Inductive

  • fix even example (#53)

• Axiomatic

  • detail lemmas in EX3
  • explain clusters (#52)

• Minimal contracts

  • search +1 proved

• Triggering lemmas

  • reminder on assert etc.
  • update displayed VC.

• Lemma functions

  • screen ghost-code-usage-2 to update

generate pdf

Do you have a script to generate latex or pdf?

Exercise 4.1.6.2. Empty “then” branch in conditional

Hello and thank you for the great tutorial!

In the second paragraph of Exercise 4.1.6.2. Empty “then” branch in conditional:
"Show that when, instead of the “else” branch, the “then” branch is empty, the conjunction of
the condition and the precondition must implies the postcondition of the “else” branch."

I think that this is typo but I'm not sure how to fix it. Do you mean "conjunction of
the negation of condition and precondition must imply the postcondition of the “else” branch."?

3.2.5.1 post conditions are not successfully proved (without pre conditions)

In the exercise 3.2.5.1 it says "specify the post conditions until successfully proved (run without rte)". IMO, the tutorial solution would be:

/*@
	ensures *q * y + r == x;
	ensures *r < y;
*/
void div_rem(unsigned x, unsigned y, unsigned* q, unsigned* r) {
    *q = x / y;
    *r = x % y;
}

Unfortunately, I cannot get them proved without specifying pre-conditions. I would expect at least the latter one to be proved by Frama-C. The generated error is timeout (default is 10 sec).

ACSL by Example

In the the tutorial "ACSL by Example" mentioned but, unfortunately, with the old URL at Fraunhofer FOKUS.

Please link directly to https://github.com/fraunhoferfokus/acsl-by-example

Exercise 3.2.5.3: separation of pointer arguments not really required

In exercise 3.2.5.3 (addition of pointed values) part 2, this is the solution provided:

#include <limits.h>

/*@ 
  requires INT_MIN <= *p + *q <= INT_MAX ;
  requires \valid_read(p) && \valid_read(q) && \valid(r) ;
  requires \separated(p, r);
  requires \separated(q, r);
  assigns *r ;
  ensures *r == *p + *q ;
*/
void add(int *p, int *q, int *r){
  *r = *p + *q ;
}

However, I was able to prove this function to be correct (as well as the examples that call this function) without requiring the separation between pointer arguments, just with a slightly different postcondition:

/*@
    requires \valid_read(a) && \valid_read(b) && \valid(r);
    requires INT_MIN <= *a + *b <= INT_MAX;

    assigns *r;

    ensures *r == \old(*a) + \old(*b);
 */
void add(int *a, int *b, int *r) {
  *r = *a + *b;
}

I'm just showing this in case you prefer this solution, or in case the exercise actually consisted in identifying the separation between pointer arguments (which as you can see, it's not really required).

Stephen Gaito's comments on the Tutorial

This (single?) issue will contain my evolving comments and issues with this (wonderful!) tutorial.
I intend to keep an expanding task list of items I think need addressing. (Feel free to strikethrough any tasks which are out of scope).

• an Appendix describing the WP interactive proof editor (all in one place) which is more detailed than the WP user document's coverage. (created issue #47)

  • discussion of how to exit the proof editor and return to the list of WP goals.
  • discussion of what "verified (but has dependencies with Unknown status)" means.... how do I find these dependencies? (I now see that these dependencies are highlighted if I know what to look for.... indeed I now even see a right-click-menu-item devoted to dependencies... however a discussion of what they are and how to find then would be welcome)

• Exercise 3.1.3.3 Alphabet Letter: the provided answer takes longer than the frama-c-gui's default timeout of 10ms(?) -- you might want to add some comments about the possible need to up/change the default timeout? (using this answer with frama-c on the command line succeeds, so your regression tests probably do not show this issue).

... more to come...

See also

• #48

Contextual information

• Frama-C, Why3, Alt-Ergo installation mode: all via Opam
• Frama-C version: 25.0-beta (Manganese)
• Plug-in used: WP
• Why3 version: Why3 platform, version 1.5.0
• Alt-Ergo version: 2.4.1
• OS name: Ubuntu
• OS version: 21.10 (Impish)
• Number of CPU's: 2
• CPU speed: 2.80GHz
• RAM: 16Gb

Interactive proof editor

Describe interactive proof editor and how to use it.

Différentes typos repérées

Voici les petites typos que je pense avoir relevées dans la version française :

tutoriel_wp/french/function-contract/contract.tex

Lines 414 to 415 in ec0d0cb

	répondre autre chose que « oui », « non » ou « inconnu », ils ne sont pas
	incapables d'extraire le « pourquoi » d'un « non » ou d'un « inconnu ». Il

Je trouve le "pas incapables" suspicieux...

tutoriel_wp/french/function-contract/well-specified.tex

Line 355 in ec0d0cb

En effet, nous n'avons pas spécifié les effets de bords autorisés pour notre

tutoriel_wp/french/function-contract/well-specified.tex

Line 381 in ec0d0cb

provoque pas d'effets de bords. Ce cas est précisé en donnant \CodeInline{\textbackslash{}nothing}

Je crois que "bord" ne prend pas de "s".

tutoriel_wp/french/proof-methodologies/lemma-functions.tex

Line 219 in ec0d0cb

(en supposant que la conclusion que nous obtenir des prémisses a toujours du

"que nous obtenir" -> obtenons

tutoriel_wp/french/proof-methodologies/lemma-functions.tex

Lines 275 to 276 in ec0d0cb

	retourne son indice, ou ce n'est pas le cas, et dans ce cas la fonction retourne
	-1. Le premier comportement est facile à montrer, le retour correspondant à cette

Elle ne retourne pas -1 mais SIZE_MAX d'après le code du dépot et UINT_MAX d'après l'ancien pdf.

Mathematics of indirect assignment (C-pointers)

Yet again many thanks for an excellent tutorial.

Alas, I have fallen into my "Mathematician of very little brain" mode.... I am having trouble understanding the mathematics which underlies your discussion in section 4.1.1.1 "Assignment of pointed value".

At the height of 10,000 meters, I can follow your discussion (after a couple of re-readings).

However I am finding it difficult to find, what is for me, a Mathematically rigorous interpretation of your discussion. For me, at the moment, I think you are mixing syntax and semantics, which for me should be kept as distinct parts of your discussion.

The rest of the chapter (which I have skimmed) is fairly standard and I know of other expositions which give pretty much the same mathematical meaning/exposition.

As we both know, there are very few, if any, expositions which deal directly with indirect assignment (C-pointers).

Where can I find a rigorous discussion of the "weakest precondition predicate" for indirect assignment (C-pointers)?

Which discussions/papers are you or your team using?

Version of Coq used in the tutorial

First let me say thank you for this nice tutorial!

I have one question: is there a specific reason for using Coq 8.9.0 in a document from March 2020? Are there issues with the tools when more recent versions of Coq are used or is it just a bit hard to setup so that you keep your setup for a few years?

You might want to leave a few words in the tutorial on the rationale behind this and some advice.

Exercice "Le dernier angle d’un triangle"

Bonjour et merci pour ce tutoriel très complet.
Je m'interroge sur l'exercice "Le dernier angle d’un triangle" au §3.1.4.5.
Si l'angle calculé respecte les mêmes priorités que les 2 angles en paramètres, c'est-à-dire être compris en 0 et 180 degrés, alors il n'est pas possible de prouver cette dernière propriété sans l'ajout d'une précondition qui est : first + second < 180

Peut-être que la solution devrait plutôt être :

/*@
    requires 0 <= a <= 180 ;
    requires 0 <= b <= 180 ;
    requires a + b < 180 ;

    ensures \result + a + b == 180 ;
    ensures 0 <= \result <= 180 ;
*/
int last_tri(int a, int b){
    return 180 - a - b;
}

Qu'en pensez-vous ? Ai-je mal compris l'exercice ?
Bonne journée

Question about order3

is not

tutoriel_wp/code/function-contract/well-specified/ex-5-order-3-answer.c

Line 10 in f4c1be5

ensures \old(*a == *b == *c) ==> *a == *b == *c ;

implied by

tutoriel_wp/code/function-contract/well-specified/ex-5-order-3-answer.c

Line 8 in f4c1be5

ensures { *a, *b, *c } == \old({ *a, *b, *c }) ;

Small typo in chapter 3 of the English version (page 29 in the PDF)

Hi,
While reading through your tutorial I spotted a small typo in this section:

https://github.com/AllanBlanchard/tutoriel_wp/blob/25ac4605307f1b12f4a7413dbd71f3e4c6f5cdd2/english/function-contract/contract.tex#LL372-L374C14

Currently it says:

"This is the verification condition generated by WP about our property and our
program, we do need to understand everything here, but we can get the
general idea."

But it should properly be this instead:

"This is the verification condition generated by WP about our property and our
program, we do not need to understand everything here, but we can get the
general idea."

Exercise 7.3.6.1: additionnal assert needed to prove post-condition

Using the code from the correction of 7.3.6.1 in Frama-C 21 Scandium, WP fails to prove the post-condition of sum_n with either Alt-Ergo or CVC4. Somehow, adding //@ assert 0 <= n * (n + 1); allows either to prove it.

ex. 4.2.6.4, wrong clauses?

In the exercise 4.2.6.4 the provided answer is the following:

void foo(){
  int i ;
  int x = 0 ;
  /*@
    loop invariant 0 <= i <= 19 ;
    loop assigns i ;
    loop variant 20 - i ;
  */
  for(i = 0 ; i < 20 ; ++i){
    if(i == 19){
      x++ ;
      break ;
    }
  }
  //@ assert x == 1 ;
  //@ assert i == 19 ;
}

I see three issues here:

• Shouldn't we include "x" as well in the loop assigns clause?
• I don't see how this is verified by WP. First we say that loop doesn't assign "x", i.e. x value isn't changed, and then Frama-C asserts that x is equal to 1.
• the loop variant clause can change to loop variant 20 - i ;, right?

Exercise 4.2.6.4: incorrect simplification of weakest precondition

In the penultimate step of the correction for exercise 4.2.6.4, we have:

(x < 0 ==> y <  0 ==> -15 <= 0 + 5 - y <= 25) &&
(x < 0 ==> y >= 0 ==> -15 <= 0 - 5 - y <= 25) &&
(x >= 0 ==> y <  0 ==> -15 <= x + 5 - y <= 25) &&
(x >= 0 ==> y >= 0 ==> -15 <= x - 5 - y <= 25) --> (* Simpl *)

(x < 0 ==> y <  0 ==> -20 <= y <= 20) &&
(x < 0 ==> y >= 0 ==> -20 <= y <= 20) &&
(x >= 0 ==> y <  0 ==> -20 <= x - y <= 20) &&
(x >= 0 ==> y >= 0 ==> -20 <= x - y <= 20)

Shouldn't that be:

(x < 0 ==> y <  0 ==> -15 <= 0 + 5 - y <= 25) &&
(x < 0 ==> y >= 0 ==> -15 <= 0 - 5 - y <= 25) &&
(x >= 0 ==> y <  0 ==> -15 <= x + 5 - y <= 25) &&
(x >= 0 ==> y >= 0 ==> -15 <= x - 5 - y <= 25) --> (* Simpl *)

(x < 0 ==> y <  0 ==> -20 <= y <= 20) &&
(x < 0 ==> y >= 0 ==> -30 <= y <= 10) &&
(x >= 0 ==> y <  0 ==> -20 <= x - y <= 20) &&
(x >= 0 ==> y >= 0 ==> -10 <= x - y <= 30)

?

This can then only be simplified to:

(x < 0 ==> -20 <= -y <= 10) &&
(x >= 0 ==> y <  0 ==> x - y <= 20) &&
(x >= 0 ==> y >= 0 ==> -10 <= x - y <= 30)

Exercise 6.1.4.4: incorrect specification of permutation

In the correction of 6.1.4.4, we are given the definition of permutation:

/*@
  inductive permutation{L1, L2}(int* arr, integer fst, integer last){
  case reflexive{L1}: 
    \forall int* a, integer b,e ; permutation{L1,L1}(a, b, e);
  case rotate_left{L1,L2}:
    \forall int* a, integer b, e, i ;
      b < i <= e ==> rotate{L1, L2}(a, b, i) ==> permutation{L1, L2}(a, b, e) ;
  case rotate_right{L1,L2}:
    \forall int* a, integer b, e, i ;
      b <= i < e ==> rotate{L1, L2}(a, i, e) ==> permutation{L1, L2}(a, b, e) ;
  case transitive{L1,L2,L3}:
    \forall int* a, integer b,e ; 
      permutation{L1,L2}(a, b, e) && permutation{L2,L3}(a, b, e) ==> 
        permutation{L1,L3}(a, b, e);
  }
*/

Note that rotate_left and rotate_right do not make any assumption on the rest of the array, outside the rotation. Thus, the following code is valid:

/*@
  requires \valid(arr + (0..1));
  assigns arr[0..1];
  ensures permutation{Pre, Post}(arr, 0, 2);
*/
void f(int arr[2]) {
    arr[0] = 0;
    //@assert rotate{Pre, Here}(arr, 1, 2);
}

I think the appropriate definition of permutation should be:

/*@
  inductive permutation{L1, L2}(int* arr, integer fst, integer last){
  case reflexive{L1}: 
    \forall int* a, integer b,e ; permutation{L1,L1}(a, b, e);
  case rotate_left{L1,L2}:
    \forall int* a, integer b, e, i ;
      b < i <= e ==> rotate{L1, L2}(a, b, i) ==> unchanged{L1, L2}(a, i, e) ==> permutation{L1, L2}(a, b, e) ;
  case rotate_right{L1,L2}:
    \forall int* a, integer b, e, i ;
      b <= i < e ==> unchanged{L1, L2}(a, b, i) ==> rotate{L1, L2}(a, i, e) ==> permutation{L1, L2}(a, b, e) ;
  case transitive{L1,L2,L3}:
    \forall int* a, integer b,e ; 
      permutation{L1,L2}(a, b, e) && permutation{L2,L3}(a, b, e) ==> 
        permutation{L1,L3}(a, b, e);
  }
*/

It does make life harder for the provers, and I had to insert the following asserts:

/*@
  requires beg+1 < end && \valid(arr + (beg .. end-1)) ;
  assigns arr[beg .. end-1] ;
  ensures permutation{Pre,Post}(arr, beg, end);
*/
void two_rotates(int* arr, size_t beg, size_t end){
  rotate(arr, beg, beg+(end-beg)/2) ;
  //@assert unchanged{Pre, Here}(arr, beg+(end-beg)/2, end);
  //@ assert permutation{Pre, Here}(arr, beg, end) ;
  //@ghost Mid: ;
  rotate(arr, beg+(end-beg)/2, end) ;
  //@assert unchanged{Mid, Here}(arr, beg, beg+(end-beg)/2);
}

\begin{zdsalertblock} without {}

In the English version, this block is showing with title "P" and text "lease note...":

\begin{zdsalertblock}
  Please note that this document is the very first english version of the
  tutorial...

I think there's a {} missing after \begin{zdsalertblock} to prevent it from happening.