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
with Snark
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. As of this release claim names are qualified. If the user does not explicitly use a qualifier then all properties that have that name will be used, regardless of their qualification. Note also that Specware does not require property names to be unique. If there are more than one property that has the same name as a claim in the using clause then they will all be sent to Snark.
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.
The with clause is used to specify which prover to be used. If the with clause is omitted which is typically the case, then before invoking Snark, the claim will be sent to a simple integer linear inequality decision procedure based on the Fourier Motzkin method. If this fails then Snark will be invoked. Optionally the user can specify either, Snark or FourierM to explicitly state which prover he wants used. Note that the inequality decision procedure does not make use the properties specified in the using clause.
After Snark completes, Specware will report on the success or failure of the Snark proof.