--- layout: fc_discuss_archives title: Message 76 from Frama-C-discuss on December 2009 ---
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? 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 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/89f06a22/attachment.htm