Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

I did not try it yet, but I guess it is the same problem about labels  
that I pointed out in your previous example.
Thanks again for your report.
	L.


Le 5 ao?t 11 ? 12:16, mars Gu a ?crit :

> 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
> < 
> max_element1 
> .c><max_element2.c>_______________________________________________
> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110805/4a3ea19c/attachment.htm>