This section describes what happens when specific kinds of units are processed.
The user can construct specs by explicitly listing the sorts, ops, and axioms comprising the spec, possibly after importing one or more spec. When these spec definitions are processed, Specware typechecks all the expressions that appear in the spec. Typechecking means checking that the expressions are type-correct, according to the rules of the Metaslang language.
In general, only some of the ops and variables that appear in an expression have explicit type (i.e., sort) information. Typechecking also involves reconstructing the types of those ops and variables that lack explicit type information.
Typechecking is an integrated process that checks the type correctness of expressions while reconstructing the missing type information. This is done by deriving and solving type constraints from the expression. For instance, if it is known that an op f has sort A -> B then the type of the variable x in the expression f(x) must be A, and the type of the whole expression must be B.
If the missing type information cannot be uniquely reconstructed and/or if certain constraints are violated, Specware signals an error, indicating the textual position of the problematic expression.
Since the Metaslang type system features subsorts defined by arbitrary predicates, it is in general undecidable whether an expression involving subsorts is type-correct or not. When Specware processes a spec, it assumes that the type constraints arising from subsorts are satisfied, thus making typechecking decidable.
The proof obligations associated with a spec, which are extracted via the Metaslang obligations operation, include conjectures derived from the type constraints arising from subsorts. If all of these conjectures are discharged (using a theorem prover) then all the expressions in the spec are type-correct.
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 a proof term. A typical proof term is of the form:
prove property in spec_term
using hypothesis1, hypothesis2
options "(use-paramodulation t)
(use-resolution nil)
(use-hyperresolution t)" |
If this term is in file proof.sw then issuing the command :sw proof will result in translating hypothesis1, hypothesis2 and property to Snark and then invoking the Snark prover to try to prove property from hypothesis1 and hypothesis2 using the options in the options list. Note that the properties property, hypothesis1, and hypothesis2 must all be names of claims (i.e. axioms, conjectures, or theorems) that appear in the spec resulting from elaborating spec_term. Note also that hypothesis1 and hypothesis2 are required to appear earlier in that spec than property. Most users will omit the options list. Additionally, the using part can be omitted as well. In this case all the properties that appear in spec_term prior to property will be used to prove property.
After Snark completes Specware will report on the success or failure of the Snark proof.
Specware will report an error if property does not occur in spec_term or if one of the axioms do not occur in spec_term prior to property.
Snark will likely break into Lisp if the user inputs an incorrect option.
In the course of its execution Snark typically outputs a lot of information as well as a proof when it finds one. All this output can be overwhelming to the user, yet invaluable in understanding why his proofs succeeded or failed. To deal with all this output Specware redirects all the Snark output to log files. In our example above, which executed a proof in the file proof.sw, Specware will create a subdirectory called snark at the same level as proof.sw. In that directory a log file called proof.log will be created that contains all the Snark output.
Just as there can be multiple units per file, there can be multiple proofs in single file. For example, in file proof.sw we could include more than one proof as follows:
p1 = prove prop1 using ax1, ax2 p1a = prove prop1 using ax3 p2 = prove prop2 |
In this case Snark will be invoked three separate times, writing three different log files. In this case an additional subdirectory will be created under snark, called proof. The three log files will then be: snark/proof/p1.log, snark/proof/p1a.log, and snark/proof/p2.log.
As is the case with any first-order prover, Snark is likely to either loop forever or run for a longer time than the user can wait. The user can provide a time limit for Snark by using an appropriate option. However, there are likely to be times when the user wants to stop Snark in the middle of execution. He can do this by typing Cntrl-C Cntrl-C in the *common-lisp* buffer. This will then interrupt Snark and place the user in the Lisp debugger. He can exit the debugger by issuing the :pop command. A log file will still be written that he can look at if he needs to.
Specware has a base library that is implicitly imported by every spec. Unfortunately, the axioms in this library are not necessarily written to be useful by Snark. Instead of having Snark use these libraries we have created a separate base library for Snark. This library is located at /Library/Base/ProverBase.sw. The axioms in this spec are automatically sent to Snark as part of any proof.
Our experience with the current prover interface is very new and as such we are still very much experimenting with it and don't expect it to be perfect at this point in time. Many simple theorems will be provable. Some that the user thinks should be might not, and the user will be required to add further hypothesis and lemmas that may seem unnecessary. We are currently working on making this interface as robust and predictable as possible, and welcome any feedback the user can offer.
One area where the user can directly experiment is with the axioms that make up the ProverBase. The axioms that make up an effective prover library are best determined by an experimental evolutionary process. The user is welcome to play with the axioms in the ProverBase, by adding new ones or changing or deleting old ones. Keep in mind the goal is to have a single library that is useful for a wide range of proofs. Axioms that are specific to different proofs should be created in separate specs and imported where needed.
The user generates Lisp code from a spec by constructing a Lisp program unit via the Metaslang generate operation. The optional string given as argument must be an absolute file path in the file system. The generated Lisp code is deposited into that file. The .lisp file extension can be omitted.
The string argument can be omitted if the spec term given as argument is a unit identifier. In this case, Specware deposits the generated code into the file A.lisp, where A is the rightmost path element comprising the unit identifier. The A.lisp file is deposited in a lisp subdirectory immediately under the directory of the file containing the unit term of the spec identified by the unit identifier given as argument to generate.
For example, suppose that the first directory in SWPATH is c:\tmp and that a spec is defined in the single-unit file c:\tmp\one\two\A.sw. Suppose that the Lisp program unit is defined by:
generate lisp /one/two/A |
Then the code is deposited into the file c:\tmp\one\two\lisp\A.lisp.
As another example, suppose that SWPATH is as before and that a spec is defined in the multiple-unit file c:\tmp\one\two\f.sw, and that B is the path element associated with the spec. Suppose that the Lisp program unit is defined by:
generate lisp /one/two/f#B |
Then the code is deposited into the file c:\tmp\one\two\lisp\B.lisp.