--- layout: fc_discuss_archives title: Message 98 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems with ensures



Hello,

Le jeu. 31 oct. 2013 09:49:13 CET,
Alessio Iotti <alle.iot at gmail.com> a ?crit :

> the attached file is a simple C program that (perhaps) computes the
> greatest common divisor
> of two integers.
> I have defined a predicate, IsGCD(a, b, val), that is true if val is
> the GCD of a and b.
> Frama-C can prove the loop invariant and variant, but cannot prove the
> ensures clause of the contract: I don't understand why.

First, your Divides and IsGCD predicates do not need to take a label as
parameter: this is only needed for predicates that access C memory
(e.g. use the value of a global variable and/or dereference some
pointer), which is not the case here: you express a property about the
mathematical integer that are given as argument. You might also want to
add some positivity conditions in the definition of IsGCD

Second, the last part of your loop invariant:
\forall integer z ; (IsGCD{Here}(a, b, z)) ==> (IsGCD{Pre}(a, b, z))
is a tautology: since Here and Pre are irrelevant, it amounts to
\forall z; P(z) ==> P(z). It is thus completely useless in proving the
ensures. I suspect that you wanted to write
IsGCD(a,b,z) ==> IsGCD(\at(a,Pre),\at(b,Pre),z).
However, I'm not completely sure that existing ATP will have much luck
in proving IsGCD(a-b,b,z) ==> IsGCD(a,b,z).

Best regards,

-- 
E tutto per oggi, a la prossima volta.
Virgile