--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on August 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with using "predicate" in "loop invariant"



Hi,

I find a problem when using "predicate" in "loop invariant".
I use the wp plugin of Frama-C, whose version is "Frama-C Carbon-20110201
+dev".
I start Frama-C with the following command:  "frama-c-gui -wp
-wp-proof alt-ergo max_element1.c &".

In the file "max_element1.c", Frama-C can prove all the specifications.
In the file "max_element1.c", in Line 43,   "loop invariant !(\exists
integer k; 0 <= k < i && (a[max] <a[k]));"  can be proved, while
in the file "max_element2.c", in Line 43,   "loop invariant IsMaximum(a, i,
max);" cannot be proved.

According to the predicate "IsMaximum":
" predicate IsMaximum{L}(value_type* a, integer n, integer max) =

 10 max_element.h   | 10     !(\exists integer i; 0 <= i < n && (a[max] <
a[i]));",
the two "loop invariant"s represent the same meaning.

If Frama-c with plugin wp can prove the first "loop invariant", it should
also be able to prove the second "loop invariant".

Liangliang Gu
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110805/93e2f0cc/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: max_element1.c
Type: text/x-csrc
Size: 1174 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110805/93e2f0cc/attachment.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: max_element2.c
Type: text/x-csrc
Size: 1143 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110805/93e2f0cc/attachment-0001.c>