Specware provides a mechanism for verifying the correctness of properties either specified in Metaslang specs or automatically generated as proof obligations arising from refinements or typechecking. Currently Specware comes packaged with the Snark first-order theorem prover. Interaction with Snark is through the proof unit described below.
The user invokes the Snark theorem prover by constructing and processing a proof term. A typical proof term is of the form:
prove f_stable in Stability
using stable_charn, f_defn
options "(use-paramodulation t)
(use-resolution nil)
(use-hyperresolution t)" |
In this proof term, Stability must be a spec-valued unit term, and f_stable, stable_charn, and f_defn must all be names of claims (i.e. axioms, conjectures, or theorems) that appear in the spec resulting from elaborating that unit term. If this proof term is in the single-unit file pruf.sw, then issuing the command proc pruf will result in first translating stable_charn, f_defn and f_stable to Snark formulas, and then invoking the Snark prover to try to prove f_stable from the hypotheses stable_charn and f_defn, using the options in the options list. To avoid circular proofs, the claims used as hypotheses -- stable_charn and f_defn in the example -- are required to appear earlier in that spec than the claim to be proved -- f_stable in the example. Most users will omit the options part. Additionally, the using part can be omitted as well. In that case all the claims that appear in the spec term before the claim to be proved will be used as hypotheses in the proof.
After Snark completes, Specware will report on the success or failure of the Snark proof.