ACSL Mini Tutorial (811288), страница 4
Текст из файла (страница 4)
The variables defined and assigned in ghost code(ghost variables) can be used in the ACSL properties.The complete annotated function max_seq then becomes:int max_seq(int* p, int n) {int res = *p;//@ ghost int e = 0;/*@ loop invariant \forall integer j;0 <= j < i ==> res >= \at(p[j],Pre);loop invariant\valid(\at(p,Pre)+e) && \at(p,Pre)[e] == res;loop invariant 0<=i<=n;loop invariant p==\at(p,Pre)+i;loop invariant 0<=e<n;*/for(int i = 0; i < n; i++) {if (res < *p) {res = *p;//@ ghost e = i;}p++;}return res;}16Bibliography[1] Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and VirgilePrevosto.
ACSL: ANSI/ISO C Specification Language. Preliminary Design, version 1.4, 2008. http://www.frama-c.cea.fr/download/acsl_1.4.pdf.[2] Caduceus. http://why.lri.fr/caduceus/.[3] JML. http://www.cs.iastate.edu/~leavens/JML/..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
