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] 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