[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] #3143: Use of PVS as a manual prover?

Hi Ben,
To use PVS with why3, you need a fairly recent version of why3, along with
PVS version >= 6.0.  pvs must also be in your path.

I got the latest why3 using the git version; for details see
Building it requires ocaml, but is pretty easy, at least on Linux.
It found PVS (6.1, in my case) without any problem, and I was able to
start it on a why spec.
Let me know if you have any problems with this,

Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

> In looking how to do manual proofs, I found this page: http://docs.adacore.com/spark2014-docs/html/ug/
> appendix.html#alternative-provers
> It mentions coq, so I installed coq using homebrew, and then from the instructions on that page, I ran
> `why3config --detect-provers`, but when I did so, I got the following result:
> ====
> ▶ why3config --detect-provers
> Found prover Coq version 8.4pl5, but Why3 wasn't compiled with support for it
> Found prover PVS version 6.0, but Why3 wasn't compiled with support for it
> warning: Warning: prover CVC4 version 1.5-prerelease is not known to be supported.
> warning: Warning: prover Alt-Ergo version 0.96 is not known to be supported.
> warning: Warning: prover Yices version 1.0.39 is not known to be supported.
> 0 provers detected and 3 provers detected with unsupported version
> Save config to /Users/benjaminhocking/.why3.conf
> ====
> I was surprised by the line about finding prover PVS (a theorem prover which I really like), so I tried
> to see how to configure Why3 to use it. I did not see any reference to PVS in appendix.html, nor did
> this search result return any hits: https://www.google.com/webhp?sourceid=chrome-instant&ion=1&espv=2&ie
> =UTF-8#q=pvs%20site%3Adocs.adacore.com
> Can one use PVS as an alternative prover (manual, of course) for SPARK Ada?
> Best Regards,
> Ben Hocking
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx