Specware 4.1 User Manual

Copyright © 2001-2004 by Kestrel Development Corporation

Copyright © 2001-2004 by Kestrel Technology LLC

All rights reserved

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

The name Allegro Common Lisp® is a registered trademark of Franz Inc.

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
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
  Next
  Installing Specware