--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on August 2011 ---
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>