Specware 4.2 User Manual

Copyright © 2001-2009 by Kestrel Development Corporation

Copyright © 2001-2009 by Kestrel Technology LLC

All rights reserved

The name Specware® is a registered trademark of Kestrel Development Corporation

Table of Contents
1. Installing Specware
Contents of Distribution Package
System Requirements
Hardware
Operating system
Installation Instructions
Uninstalling
2. Getting Started
Starting Specware
Exiting Specware
3. Usage Model
Units
Interaction
4. Defining Units
Conceptual Model
Unit Identifiers
Unit Terms
Realization via the File System
The SWPATH Environment Variable
Single Unit in a File
Multiple Units in a File
Unit Definitions Are Managed Outside of Specware
5. The Specware Shell
Overview
Typechecking Specs
Resolution of Unit Identifiers
SWPATH-Based Unit Identifier
Relative Unit Identifiers
Command Format
Miscellaneous Commands
Processing a Unit
Showing a Unit
Generating Proof Units
Evaluating Expressions
Generating Lisp Code
Generating Java Code
The Option Spec
Translation of Inbuilt Ops
Metaslang/Java Interface
Type Conversion between Java and Metaslang
Generating C Code
Generating, Compiling and Running the generated C code using "make"
Compiling and Running the generated C code without using "make"
Garbage Collector
Supplying a C "main" function
Auxiliary Commands for Lisp
Finally
6. Proving Properties in Specs
The Proof Unit
Implicit Axioms
Proof Errors
Proof Log Files
Multiple Proofs
Interrupting Snark
The Prover Base Library
The Experimental Nature of the Prover
7. Lisp Code Generated from Specs
Translation of Specware Names to Lisp Names
Arity and Currying Normalization
Representation of Other Types
8. Debugging Generated Lisp Files
Tracing
Breaking
Timing
Interrupting
9. Emacs Usage in Specware
Specware Mode Commands
Specware Interaction Commands
Other Useful Emacs Commands
X-Symbol Mode
Hide/Show Commands
  Next
  Installing Specware