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

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



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,