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

[Frama-c-discuss] Partial correctness explained to children!



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