This is the command gwhy that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
why - A multi-language multi-prover verification tool
why [ options ] files
why is a verification tool. It takes annotated programs as input (in ML or C syntax) and
outputs verification conditions for several proof assistants (Coq, PVS, HOL Light, Mizar)
and decision procedures (haRVey, Simplify).
-h Help. Will give you the full list of command line options.
Jean-Christophe Filliatre <[email protected]>
Use gwhy online using onworks.net services