Closed arvidj closed 4 years ago
Hi,
Indeed, GOSPEL/VOCaL is still lacking documentation. That's the main reason why there was no public announcement yet.
This paper describes the Why3 workflow in vocal to some extend: https://hal.inria.fr/hal-01783851v2
Here is a brief how to.
The why3gospel plugin extends Why3 with the ability to read a GOSPEL-annotated .mli file. The result is a single Why3 module called "Sig". Therefore you can do
use file.Sig
in a Why3 file and if "file.mli" is found in the load path, you'll get the GOSPEL spec in Why3 format.
Now to prove that a WhyML implementation conforms to such a spec, you first write it, say in a module Impl
module Impl ... end
and then prove the refinement, as follows
module Correct use Impl clone file.Sig with val f, val g, ... end
(assuming functions are given the same names in the OCaml interface and in the WhyML implementation).
You have examples of that process in sub-directory vocal/proofs/why3/. Look for instance at Arrays_impl.mlw, which contains the implementation of vocal/src/Arrays.mli.
Jean-Christophe
On 02/19/2020 06:07 PM, arvidj wrote:
Would it be possible to provide a small tutorial or enhance the README? I manage to:
- install the vocal package
- create an interface .mli-file based on the examples in the README
However, from there, I do not understand how to use the why3gospel plugin to generate the Why3 module, and how to give use the Why3 module to provide a verified implementation of the interface.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/vocal-project/vocal/issues/9?email_source=notifications&email_token=AA2YXNWPRLMQPJS3ETQ5KKTRDVRNNA5CNFSM4KX5HLM2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IOWPWQQ, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA2YXNUGZVOUFPRGE3AQPTTRDVRNNANCNFSM4KX5HLMQ.
Hi, I had not noticed that VOCaL was not yet released, that explains it. Thanks for your detailed explanation.
Would it be possible to provide a small tutorial or enhance the README? I manage to:
However, from there, I do not understand how to use the why3gospel plugin to generate the Why3 module, and how to give use the Why3 module to provide a verified implementation of the interface.