allanblanchard / tutoriel_wp Goto Github PK
View Code? Open in Web Editor NEWFrama-C and WP tutorial
License: Other
Frama-C and WP tutorial
License: Other
Describe interactive proof editor and how to use it.
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);
}
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
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.
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?
Hi,
While reading through your tutorial I spotted a small typo in this section:
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."
Org
General
Update acknowledgment
Vocab (#44)
Images
Contracts
main
somewhereexits
terminates
WP calculus
assert
, admit
, check
#58loop invariant
and new loop invariant
computation, #58check
and admit
for function contracts (#64)terminates
+ decreases
(#43)Predicates
unchanged-loc
screen (0dcb27e)Functions
Lemmas
check lemma
#58Inductive
Axiomatic
Minimal contracts
Triggering lemmas
assert
etc.Lemma functions
ghost-code-usage-2
to updateThis (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)
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
Bonjour,
Voilà les quelques questions ou remarques sur le document :
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.
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 !
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.
is not
implied by
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.
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
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).
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
Je trouve le "pas incapables" suspicieux...
Je crois que "bord" ne prend pas de "s".
"que nous obtenir" -> obtenons
tutoriel_wp/french/proof-methodologies/lemma-functions.tex
Lines 275 to 276 in ec0d0cb
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.
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)
Do you have a script to generate latex or pdf?
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).
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."?
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:
loop variant 20 - i ;
, right?A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.