Generating Proof Units

Two Specware Shell commands facilitate the creation of proof units. The first is:

punits [unit-identifier [filename] ]

in which the unit identifier must be that of a single spec term. Executing the command then generates proof units for all the conjectures, theorems and proof obligations of the spec resulting from elaborating that spec term.

These proof units are written to a file that can then be processed to attempt proving all the conjectures in the spec. The proof file can also be edited to add usings and options to the proof units. By default, the proof units are written in a file obtained from the unit identifier given to the punits command. For example, if the unit identifier is /dir1/dir2/foo, then the proof units are written to /dir1/dir2/foo_Proofs.sw. Optionally, the file for the proof units to be written to can be given as the second argument to the punits command.

Using punits, proof units are generated not just for the conjectures explicitly present in the spec, but also for all non-local conjectures for the spec. The user can use the command:

lpunits [unit-identifier [filename] ]

to generate a proof-unit file with only the "local" conjectures.