# 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

*Subject*: [Frama-c-discuss] Problems with ensures*From*: virgile.prevosto at m4x.org (Virgile Prevosto)*Date*: Thu, 31 Oct 2013 11:09:40 +0100*In-reply-to*: <CABNEXcbFTnx7v2OtrQwcKRrrih5SmOD+wp8B0j7DAZGCJgHRtQ@mail.gmail.com>*References*: <CABNEXcbFTnx7v2OtrQwcKRrrih5SmOD+wp8B0j7DAZGCJgHRtQ@mail.gmail.com>

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

**References**:**[Frama-c-discuss] Problems with ensures***From:*alle.iot at gmail.com (Alessio Iotti)

- Prev by Date:
**[Frama-c-discuss] Problems with ensures** - Next by Date:
**[Frama-c-discuss] Array problem - Jessie plugin** - Previous by thread:
**[Frama-c-discuss] Problems with ensures** - Next by thread:
**[Frama-c-discuss] sums of arrays** - Index(es):