--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on November 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Composition of COMPLEX Contracts



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