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] Composition of COMPLEX Contracts

  • Subject: [Frama-c-discuss] Composition of COMPLEX Contracts
  • From: yannick.moy at gmail.com (Yannick Moy)
  • Date: Tue Nov 11 11:41:35 2008
  • In-reply-to: <4C7D7838F1104A35B59E7185B6BE2567@AHARDPLACE>
  • References: <CAC50CFBBB324643893885ACDB6DFE3A@AHARDPLACE> <14791e30811101449w44a53343ne60c0d135a0daa27@mail.gmail.com> <4C7D7838F1104A35B59E7185B6BE2567@AHARDPLACE>
Hi,

>
> I added an assigns clause and a loop assigns but the post-condition cannot
> be proven (Hydrogen). Is there something else missing or is it due to the
> Hydrogen.
>

Loop assigns is not supported yet in the Jessie plugin, a warning is now
issued.
To better answer your question, we need precisions, such as:
- what VC exactly are not proved
- which ATP you use

In your case, you are directly using quantifiers, for which is not easy to
get automatic proofs. The best way is to hide quantifiers by defining
equivalent predicates and logic functions with appropriate axioms, that
should be expressed in a way that facilitates the proof by ATP. This last
thing is probably the hardest part, and needs most of all experiments on the
specific programs you want to prove, with the provers you want to use. To
help the prood go through, it is usually a good idea to add logical
assertions (//@ assert ...) that direct the proof, and help you understand
which parts of a bigger formula are not proved.

HTH
-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081111/b7d06f47/attachment.html