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

[Frama-c-discuss] wp <==> problem



Hi,

On 13/07/2011 11:50, mars Gu wrote:
> Hi,
>
> i find a problem with the wp plugin in 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 binary_search2.c &".
>
> In the file " binary_search2.c",  Frama-c can prove  line 46,47,49, but
> line 51.
> If line 46,46,49 can be proved, line 51 should be proved.
> Because if
> 1:a<==>b
> 2:b<==>c
> 3:( a<==>b && b<==>c) ==> (a<==>c)
> is true, then
> 4: a<==>c
> should also be true.


Your b in 1 and in 2 are not the same: please be careful with "<=" 
versus "<"

Generally speaking, I don't think you need to use so many <==> in 
specifications. See for example

http://proval.lri.fr/gallery/BinarySearchACSL.en.html

for a correct ASL-annotated binary search function

- Claude