maybe this kind of approach may be useful:
Producing Certified Functional Code from Inductive Specifications
http://cedric.cnam.fr/~delahaye/papers/relext-coq%20(CPP'12).pdf
cheers.
2014-05-09 11:18 GMT+02:00 Guillaume Melquiond :
> On 09/05/2014 10:42, Jean-Jacques Levy wrote:
>
> Yes, it is f
On a related note:
"Safety
OCaml programs are thoroughly checked at compile-time such that they are
proven to be entirely safe to run, e.g. a compiled OCaml program cannot
segfault." [1]
"errors such as “segmentation faults” cannot occur during execution" [2]
anyone wants to add something about
not exactly what you want, but
invariant {I(i+1) -> J(i)}
wouldn't do?
2014-03-26 15:31 GMT+01:00 Alan Schmitt :
> Hello,
>
> It seems to me that when several invariants are given for a loop, each
> one is proven separately assuming every invariant at the previous step.
> For instance, in
gt; https://www.lri.fr/~filliatr/types-summer-school-2007/notes.pdf
>
> Please, see section 1.3.
>
> regards,
> taimoor
>
>
>
> On 02/03/2014 10:25 AM, Nuno Gaspar wrote:
>
> Hello.
>
> I can see that this has been already asked [1] but I could not find it
Hello.
I can see that this has been already asked [1] but I could not find it
anywhere..
Is there a document indicating WhyML operational semantics?
Thank you.
[1]
http://lists.gforge.inria.fr/pipermail/why3-club/2013-February/000540.html
--
Bart: Look at me, I'm a grad student, I'm 30 years
