--- layout: fc_discuss_archives title: Message 87 from Frama-C-discuss on December 2009 ---
Thanks for the many replies. I tried it and it worked. At the same time I have to admit that I haven't really understood the necessity of the loop variant. In our example we have a lot of loops the would include loop annotations of the form loop invariant 0 <= i <= n; loop variant n-i; Is there a way to easily combine and shorten these two lines? Jens Am 08.12.2009 um 14:54 schrieb Claude Marche: > Jens Gerlach wrote: >> We were able to deductively verify the following implementation of >> linear search successfully with Jessie on top of why version 2.19. >> >> However, with why 2.23 there is one safety related VC that remains >> unproven. >> In the jessie gui, the unproven VC reads "variant decreases". >> >> Do we have to improve the specification to get rid of that issue? >> If so, how? > add "loop variant n-i;" and you should be done ! > > Since Why 2.22, the policy for generating termination VCS is as strict > as possible, to guarantee soundness > (see BTS #0000103) > > In the future, Jessie should support ACSL "terminates" clauses, to > manually annotate function for which you don;t care about termination. > > In a nearer future, there could a new pragma to control the generation > of such VCs. > > Anyway: any suggestion welcome ! > > - Claude >> >> Regards Jens >> >> /*@ >> requires n >= 0; >> requires \valid_range(a, 0, n-1); >> >> assigns \nothing; >> >> behavior some: >> assumes \exists int i; (0 <= i < n) && a[i] == v; >> ensures 0 <= \result < n; >> ensures a[\result] == v; >> ensures \forall int i; (0 <= i < \result) ==> a[i] != v; >> >> behavior none: >> assumes \forall int i; (0 <= i < n) ==> a[i] != v; >> ensures \result == n; >> */ >> int find(const int* a, int n, int v) >> { >> /*@ >> loop invariant 0 <= i <= n; >> loop invariant \forall int k; 0 <= k < i ==> a[k] != v; >> */ >> for (int i = 0; i < n; ++i) >> if (a[i] == v) >> return i; >> >> return n; >> } >> >> >> -- >> >> Dr.-Ing. Jens Gerlach >> Eingebettete Systeme - EST >> Tel.: +49 (0)30 6392 1841 >> Fax.: +49 (0)30 6392 1805 >> E-Mail: jens.gerlach at first.fraunhofer.de >> <mailto:jens.gerlach at first.fraunhofer.de> >> >> Fraunhofer-Institut f?r Rechnerarchitektur und Softwaretechnik, FIRST >> Kekul?stra?e 7 >> 12489 Berlin >> Germany >> http://www.first.fraunhofer.de >> >> >> >> >> ------------------------------------------------------------------------ >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > > -- > Claude March? | tel: +33 1 72 92 59 69 > INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 > Parc Orsay Universit? | fax: +33 1 74 85 42 29 > 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ > F-91893 ORSAY Cedex | > > > > > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Dr.-Ing. Jens Gerlach Eingebettete Systeme - EST Tel.: +49 (0)30 6392 1841 Fax.: +49 (0)30 6392 1805 E-Mail: jens.gerlach at first.fraunhofer.de Fraunhofer-Institut f?r Rechnerarchitektur und Softwaretechnik, FIRST Kekul?stra?e 7 12489 Berlin Germany http://www.first.fraunhofer.de -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091208/c547da73/attachment.htm