Ocaml Beginners is a Restricted Group with 1215 members.
 Ocaml Beginners

 Restricted Group,
 1215 members
Re: "ocaml_beginners"::[] Does OCaml need proofs?
Expand Messages
  In ocaml_beginners@yahoogroups.com, Thomas Hutchinson
<thomas.hutchinson@...> wrote:> I don't know a lot about formal methods, so I'm not sure what tools are
You would imagine so, but I've never heard of any. OCaml is a popular
> out there to prove things about OCaml code (I would imagine that there
> are a number of projects to do this).
implementation language in the formal methods community, but the
source languages are usually things like C, Java, and HDL. I'd be
interested to hear of any tool to check interesting properties on
OCaml programs. Even a simple lintlike tool would be nice.
Chris   In ocaml_beginners@yahoogroups.com, silviu andrica
<silviu_andrica@...> wrote:> I was wondering if a program written in OCaml needs to be
theoremproved to be sure it does what it is intended.
> I mean, is there a theorem prover for OCaml, or a tool that
translates OCaml code into Coq's input or other theorem provers?
If you want to prove a theorem about the program which is stronger
than the theorems you get "for free" from the type checker [1] (e.g.,
termination, race and deadlockfreedom) then yes, of course you need
a separate theorem proving tool. I'm not aware of any such tool for
OCaml programs. (As others have pointed out, Coq goes in the opposite
direction: proofs to programs, not programs to proofs.)
Regards,
Chris
[1][http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps Philip
Wadler. Theorems for free!]  On Thursday 19 February 2009 14:56:41 Richard Jones wrote:
> There's also a good paper where the authors translated the OCaml
I'd be interested to know what the bugs were...
> stdlib Map module by hand into Coq, proved it, then automatically
> extracted the code back to OCaml. (And found a bug or two along the
> way). Unfortunately I can't find that paper right now.

Dr Jon Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?e  Richard Jones wrote:
>
Actually, It was in the Set module.
> There's also a good paper where the authors translated the OCaml
> stdlib Map module by hand into Coq, proved it, then automatically
> extracted the code back to OCaml. (And found a bug or two along the
> way). Unfortunately I can't find that paper right now.
>
The paper can be found here:
Functors for Proofs and Programs
(J.C. Filliâtre and P. Letouzey)
http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz

Mehdi Dogguy مهدي الدقي
http://www.pps.jussieu.fr/~dogguy
Tel.: (+33).1.44.27.28.38  On Thu, Feb 19, 2009 at 03:59:28PM +0000, Jon Harrop wrote:
> I'd be interested to know what the bugs were...
AVL balancing bugs. Basically what they proved (IIRC the author of the
proofs was JeanChristophe Filliatre) is that the previous
implementation did not guarantee maximal balancing at any specific
time in the internal data structure.
Out of memory, I don't think there is a paper, but more likely a
contrib entry in the Coq library.
Cheers.

Stefano Zacchiroli o PhD in Computer Science \ PostDoc @ Univ. Paris 7
zack@{upsilon.cc,pps.jussieu.fr,debian.org} <> http://upsilon.cc/zack/
Dietro un grande uomo c'è .. . . Et ne m'en veux pas si je te tutoie
sempre uno zaino ........... ..: .... Je dis tu à tous ceux que j'aime  On Thursday 19 February 2009 16:01:11 Mehdi Dogguy wrote:
> Richard Jones wrote:
Hmm, it only says "two internal functions were producing incorrectly balanced
> > There's also a good paper where the authors translated the OCaml
> > stdlib Map module by hand into Coq, proved it, then automatically
> > extracted the code back to OCaml. (And found a bug or two along the
> > way). Unfortunately I can't find that paper right now.
>
> Actually, It was in the Set module.
> The paper can be found here:
>
> Functors for Proofs and Programs
> (J.C. Filliâtre and P. Letouzey)
> http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz
trees" but not what the exact mistakes were in the source code... :(

Dr Jon Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?e  De Christopher Conway (19 February, 15:47) :
>  In ocaml_beginners@yahoogroups.com, silviu andrica
The Why tool [1], developed by JeanChristophe Filliâtre, produces «
> <silviu_andrica@...> wrote:
> > I was wondering if a program written in OCaml needs to be
> theoremproved to be sure it does what it is intended.
> > I mean, is there a theorem prover for OCaml, or a tool that
> translates OCaml code into Coq's input or other theorem provers?
>
> If you want to prove a theorem about the program which is stronger
> than the theorems you get "for free" from the type checker [1] (e.g.,
> termination, race and deadlockfreedom) then yes, of course you need
> a separate theorem proving tool. I'm not aware of any such tool for
> OCaml programs. (As others have pointed out, Coq goes in the opposite
> direction: proofs to programs, not programs to proofs.)
verification conditions » from annotated Ocaml code. Then , it sends
them to external provers (Coq, PVS, ...) and decision procedures
(Simplify, ...). Most of the time, human interaction is necessary to
complete the proofs.
[1] http://why.lri.fr/index.en.html
>
> Regards,
> Chris
>
> [1][http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps Philip
> Wadler. Theorems for free!]
>
>
>
>
> <!DOCTYPE HTML PUBLIC "//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
> <html>
> <head>
> </head>
>
>
>
>
> <body style="backgroundcolor: #ffffff;">
>
> <!~**PrettyHtmlStartT**~>
> <div id="ygrpmlmsg" style="width:655px; position:relative;">
> <div id="ygrpmsg" style="width: 470px; margin:0; padding:0 25px 0 0; float:left; zindex:1;">
> <!~**PrettyHtmlEndT**~>
>
> <div id="ygrptext">
> <p> In <a href="mailto:ocaml_beginners%40yahoogroups.com">ocaml_beginners@<wbr>yahoogroups.<wbr>com</a>, silviu andrica<br>
> <silviu_andrica@<wbr>...> wrote:<br>
> > I was wondering if a program written in OCaml needs to be<br>
> theoremproved to be sure it does what it is intended.<br>
> > I mean, is there a theorem prover for OCaml, or a tool that<br>
> translates OCaml code into Coq's input or other theorem provers?<br>
> <br>
> If you want to prove a theorem about the program which is stronger<br>
> than the theorems you get "for free" from the type checker [1] (e.g.,<br>
> termination, race and deadlockfreedom) then yes, of course you need<br>
> a separate theorem proving tool. I'm not aware of any such tool for<br>
> OCaml programs. (As others have pointed out, Coq goes in the opposite<br>
> direction: proofs to programs, not programs to proofs.)<br>
> <br>
> Regards,<br>
> Chris<br>
> <br>
> [1][<a href="http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps">http://homepages.<wbr>inf.ed.ac.<wbr>uk/wadler/<wbr>papers/free/<wbr>free.ps</a> Philip<br>
> Wadler. Theorems for free!]<br>
> <br>
> </p>
>
>
> </div>
>
> <!~**PrettyHtmlStart**~>
> <div width="1" style="color: white; clear: both;"></div>
> <!~**PrettyHtmlEnd**~>
> </body>
> <!~**PrettyHtmlStart**~>
> <head>
> <style type="text/css">
> <!
> #ygrpmkp{
> border: 1px solid #d8d8d8;
> fontfamily: Arial;
> margin: 14px 0px;
> padding: 0px 14px;
> }
> #ygrpmkp hr{
> border: 1px solid #d8d8d8;
> }
> #ygrpmkp #hd{
> color: #628c2a;
> fontsize: 85%;
> fontweight: bold;
> lineheight: 122%;
> margin: 10px 0px;
> }
> #ygrpmkp #ads{
> marginbottom: 10px;
> }
> #ygrpmkp .ad{
> padding: 0 0;
> }
> #ygrpmkp .ad a{
> color: #0000ff;
> textdecoration: none;
> }
> >
> </style>
> </head>
> <head>
> <style type="text/css">
> <!
> #ygrpsponsor #ygrplc{
> fontfamily: Arial;
> }
> #ygrpsponsor #ygrplc #hd{
> margin: 10px 0px;
> fontweight: bold;
> fontsize: 78%;
> lineheight: 122%;
> }
> #ygrpsponsor #ygrplc .ad{
> marginbottom: 10px;
> padding: 0 0;
> }
> >
> </style>
> </head>
> <head>
> <style type="text/css">
> <!
> #ygrpmlmsg {fontsize:13px; fontfamily: arial,helvetica,clean,sansserif;*fontsize:small;*font:xsmall;}
> #ygrpmlmsg table {fontsize:inherit;font:100%;}
> #ygrpmlmsg select, input, textarea {font:99% arial,helvetica,clean,sansserif;}
> #ygrpmlmsg pre, code {font:115% monospace;*fontsize:100%;}
> #ygrpmlmsg * {lineheight:1.22em;}
> #ygrptext{
> fontfamily: Georgia;
> }
> #ygrptext p{
> margin: 0 0 1em 0;
> }
>
> dd.last p a {
> fontfamily: Verdana;
> fontweight: bold;
> }
>
> #ygrpvitnav{
> paddingtop: 10px;
> fontfamily: Verdana;
> fontsize: 77%;
> margin: 0;
> }
> #ygrpvitnav a{
> padding: 0 1px;
> }
> #ygrpmlmsg #logo{
> paddingbottom: 10px;
> }
>
> #ygrpreco {
> marginbottom: 20px;
> padding: 0px;
> }
> #ygrpreco #recohead {
> fontweight: bold;
> color: #ff7900;
> }
>
> #recocategory{
> fontsize: 77%;
> }
> #recodesc{
> fontsize: 77%;
> }
>
> #ygrpvital a{
> textdecoration: none;
> }
>
> #ygrpvital a:hover{
> textdecoration: underline;
> }
>
> #ygrpsponsor #ov ul{
> padding: 0 0 0 8px;
> margin: 0;
> }
> #ygrpsponsor #ov li{
> liststyletype: square;
> padding: 6px 0;
> fontsize: 77%;
> }
> #ygrpsponsor #ov li a{
> textdecoration: none;
> fontsize: 130%;
> }
> #ygrpsponsor #nc{
> backgroundcolor: #eee;
> marginbottom: 20px;
> padding: 0 8px;
> }
> #ygrpsponsor .ad{
> padding: 8px 0;
> }
> #ygrpsponsor .ad #hd1{
> fontfamily: Arial;
> fontweight: bold;
> color: #628c2a;
> fontsize: 100%;
> lineheight: 122%;
> }
> #ygrpsponsor .ad a{
> textdecoration: none;
> }
> #ygrpsponsor .ad a:hover{
> textdecoration: underline;
> }
> #ygrpsponsor .ad p{
> margin: 0;
> }
> o{fontsize: 0; }
> .MsoNormal{
> margin: 0 0 0 0;
> }
> #ygrptext tt{
> fontsize: 120%;
> }
> blockquote{margin: 0 0 0 4px;}
> .replbq{margin:4}
>
> dd.last p span {
> marginright: 10px;
> fontfamily: Verdana;
> fontweight: bold;
> }
>
> dd.last p span.yshortcuts {
> marginright: 0;
> }
>
> div.phototitle a,
> div.phototitle a:active,
> div.phototitle a:hover,
> div.phototitle a:visited {
> textdecoration: none;
> }
>
> div.filetitle a,
> div.filetitle a:active,
> div.filetitle a:hover,
> div.filetitle a:visited {
> textdecoration: none;
> }
>
> #ygrpmsg p {
> clear: both;
> padding: 15px 0 3px 0;
> overflow: hidden;
> }
>
> #ygrpmsg p span {
> color: #1E66AE;
> fontweight: bold;
> }
>
> div#ygrpmlmsg #ygrpmsg p a span.yshortcuts {
> fontfamily: Verdana;
> fontsize: 10px;
> fontweight: normal;
> }
>
> #ygrpmsg p a {
> fontfamily: Verdana;
> fontsize: 10px;
> }
>
> #ygrpmlmsg a {
> color: #1E66AE;
> }
>
> div.attachtable div div a {
> textdecoration: none;
> }
>
> div.attachtable {
> width: 400px;
> }
>
> >
> </style>
> </head>
> <!~**PrettyHtmlEnd**~>
> </html><!End group email >
>   In ocaml_beginners@yahoogroups.com, "François Puitg"
<francois.puitg@...> wrote:>
(e.g.,
> De Christopher Conway (19 February, 15:47) :
>
> >  In ocaml_beginners@yahoogroups.com, silviu andrica
> > <silviu_andrica@> wrote:
> > > I was wondering if a program written in OCaml needs to be
> > theoremproved to be sure it does what it is intended.
> > > I mean, is there a theorem prover for OCaml, or a tool that
> > translates OCaml code into Coq's input or other theorem provers?
> >
> > If you want to prove a theorem about the program which is stronger
> > than the theorems you get "for free" from the type checker [1]
> > termination, race and deadlockfreedom) then yes, of course you
need
> > a separate theorem proving tool. I'm not aware of any such tool for
opposite
> > OCaml programs. (As others have pointed out, Coq goes in the
> > direction: proofs to programs, not programs to proofs.)
I know about Why, and should have mentioned it, but I didn't realize
>
> The Why tool [1], developed by JeanChristophe Filliâtre, produces «
> verification conditions » from annotated Ocaml code. Then , it sends
> them to external provers (Coq, PVS, ...) and decision procedures
> (Simplify, ...). Most of the time, human interaction is necessary to
> complete the proofs.
>
> [1] http://why.lri.fr/index.en.html
it works on plainvanilla OCaml code. Is there a tool that strips Why
annotations from the input and produces an OCaml output parsable by
ocamlc?
Regards,
Chris  On Thu, Feb 19, 2009 at 8:01 PM, Christopher Conway <cconway@...> wrote:
> <francois.puitg@...> wrote:
This isn't quite right. While Why's syntax is inspired by OCaml's, it
>> The Why tool [1], developed by JeanChristophe Filliâtre, produces «
>> verification conditions » from annotated Ocaml code. Then , it sends
>> them to external provers (Coq, PVS, ...) and decision procedures
>> (Simplify, ...). Most of the time, human interaction is necessary to
>> complete the proofs.
> I know about Why, and should have mentioned it, but I didn't realize
> it works on plainvanilla OCaml code. Is there a tool that strips Why
> annotations from the input and produces an OCaml output parsable by
> ocamlc?
really isn't the same language at all. Why doesn't have variant types,
objects, polymorphic variants, records, modules. It's references are
not really first class values. They can't be returned by functions,
for example. Also, support for higherorder programs is very limited;
you can write them, but not prove them correct.
However you can see Why as a (small) subset of OCaml, and there is
indeed an option to output OCaml.

Johannes Kanig
johannes.kanig@...  On Thu, Feb 19, 2009 at 04:25:57PM +0000, Jon Harrop wrote:
> On Thursday 19 February 2009 16:01:11 Mehdi Dogguy wrote:
As you might have gathered I only have a vague memory of this
> > Richard Jones wrote:
> > > There's also a good paper where the authors translated the OCaml
> > > stdlib Map module by hand into Coq, proved it, then automatically
> > > extracted the code back to OCaml. (And found a bug or two along the
> > > way). Unfortunately I can't find that paper right now.
> >
> > Actually, It was in the Set module.
> > The paper can be found here:
> >
> > Functors for Proofs and Programs
> > (J.C. Filliâtre and P. Letouzey)
> > http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz
>
> Hmm, it only says "two internal functions were producing incorrectly balanced
> trees" but not what the exact mistakes were in the source code... :(
(sets / maps .. whatever!) but IIRC the bugs were fixed.
Rich.

Richard Jones
Red Hat  Richard Jones a écrit :
> On Thu, Feb 19, 2009 at 04:25:57PM +0000, Jon Harrop wrote:
And is there a way to, sort of semiautomatically, get OCaml code, or a
>> On Thursday 19 February 2009 16:01:11 Mehdi Dogguy wrote:
>>
>>> Richard Jones wrote:
>>>> There's also a good paper where the authors translated the OCaml
>>>> stdlib Map module by hand into Coq, proved it, then automatically
>>>> extracted the code back to OCaml. (And found a bug or two along the
>>>> way). Unfortunately I can't find that paper right now.
subset of the core language, into Coq?
All the best,

Guillaume Yziquel
http://yziquel.homelinux.org/  On Mon, Feb 23, 2009 at 07:02:56PM +0100, Guillaume Yziquel wrote:
> And is there a way to, sort of semiautomatically, get OCaml code, or a
No.
> subset of the core language, into Coq?
I have only a very shallow understanding of this, but I'll speculate
anyway: It wouldn't make sense. You write your Coq proof, and from
that can generate working OCaml code, which directly and correctly
implements the proof. But to go from random OCaml code to ... what?
You're probably better off asking someone on the Coq mailing list.
Rich.

Richard Jones
Red Hat  Richard Jones a écrit :
> On Mon, Feb 23, 2009 at 07:02:56PM +0100, Guillaume Yziquel wrote:
I half agree with wour "wouldn't make sense" statement. The Coq to Ocaml
>> And is there a way to, sort of semiautomatically, get OCaml code, or a
>> subset of the core language, into Coq?
>
> No.
>
> I have only a very shallow understanding of this, but I'll speculate
> anyway: It wouldn't make sense. You write your Coq proof, and from
> that can generate working OCaml code, which directly and correctly
> implements the proof. But to go from random OCaml code to ... what?
is indeed the cleanest path. However, I was thinking of something more like:
http://www.cl.cam.ac.uk/~so294/ocaml/
You get the ocaml code "somehow" into Coq, and then you'd be busy
painfully proving the operational semantics of your code. Of course,
it's not as neat as the purely functional Coq > Ocaml way.
But the whole painful thing is that, well, there's nothing automated in
such an import to Coq. I just hoped there was...
> You're probably better off asking someone on the Coq mailing list.
OK. I will. Thanks.
> Rich.

Guillaume Yziquel
http://yziquel.homelinux.org/  Guillaume Yziquel a écrit :
>
There is also PAF, which is a Proof Assistant for ML Programs
> And is there a way to, sort of semiautomatically, get OCaml code, or a
> subset of the core language, into Coq?
>
Verification. PAF lets you prove directly you OCaml (or a subset)
program. It has been proven to be coherent (hopefully).
You can check this article:
http://www.springerlink.com/content/u3xtkcwdnh3jcvux/
But, for more updated news, you may contact Séverine Maingaud[1] who
works on PAF.
[1] http://www.pps.jussieu.fr/~maingaud/
Hope this helps,

Mehdi Dogguy مهدي الدقي
http://www.pps.jussieu.fr/~dogguy
Tel.: (+33).1.44.27.28.38
Your message has been successfully submitted and would be delivered to recipients shortly.