Specware 4.0 User Manual

Copyright © 2001, 2002 by Kestrel Development Corporation

Copyright © 2001, 2002 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. Processing Units
Overview
Resolution of Unit Identifiers
SWPATH-Based Unit Identifier
Relative Unit Identifiers
Processing Commands
Processing a Unit
Processing a Multiple-Unit File
Unit-Specific Processing
Typechecking Specs
Proving Properties in Specs
Generating Lisp Code
Auxiliary Commands
Displaying Unit Values
Inspecting and Clearing the Cache
Inspecting and Setting SWPATH
Generating Lisp Code
Miscellaneous Commands
6. Lisp Code Generated from Specs
Translation of Specware Names to Lisp Names
Arity and Currying Normalization
Representation of Other Sorts
7. Debugging Generated Lisp Files
Tracing
Breaking
Timing
Interrupting
8. Emacs Usage in Specware
Specware Mode Commands
Specware Interaction Commands
Other Useful Emacs Commands
  Next
  Installing Specware