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] Partial correctness explained to children!

Hi Dillon,

Indeed, your postcondition is expressed in a state that is not reachable,
thus every proposition is true in that state!

By default, loop termination is not required with the Jessie plugin, thus
you do not get a VC stating that some variant should decrease on your
infinite loop, which you would not be able to prove. If you add a variant of
course, a VC will be generated.

There is nothing yet to check that you do not forget to add a variant... It
is still to be decided whether we define an option to force termination
checking, or if this should be the default, with an option to switch back to
the current behavior.

Cheers,
Yannick


On Thu, Oct 23, 2008 at 2:10 PM, Dillon Pariente <
dillon.pariente@dassault-aviation.fr> wrote:

> Hi there,
>
> (At first, please note that I'm currently running CVS version of Jessie &
> Why of october, 4)
>
> The following specification is verified by Automatic Theorem Provers on the
> small code just below:
>
> //@ requires \valid(p); assigns *p; ensures *p==4;
> void g(int*p){ while(1) *p=3; }
>
> In a way, [3==4] is validated because in the context of the related PO, one
> hypothesis is [true=false].
> Does [true=false] hypothesis come with never ending loop?
>
> Am I missing something important here? Jessie's behavior seems to be very
> different than Caduceus' one on the matter of loops.
> And more generally speaking, what if end-users forget to annotate and
> validate loop variants to ensure loop termination?
> Nothing can tell them that they might prove anything as post-condition?
>
> Your opinion and explanations will be very welcome on these points?
>
> Cheers,
> Dillon Pariente
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>



-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081023/893b89ea/attachment.htm