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!

  • Subject: [Frama-c-discuss] Partial correctness explained to children!
  • From: dillon.pariente at dassault-aviation.fr (Dillon Pariente)
  • Date: Thu Oct 23 14:10:43 2008
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