Download Specware 4.2 User Manual

Table of Contents
1. Installing Specware ....................................................................................................1
1.1. Contents of Distribution Package .....................................................................1
1.2. System Requirements........................................................................................1
1.2.1. Hardware................................................................................................2
1.2.2. Operating system ...................................................................................2
1.3. Installation Instructions.....................................................................................2
1.4. Uninstalling.......................................................................................................3
2. Getting Started ...........................................................................................................5
2.1. Starting Specware .............................................................................................5
2.2. Exiting Specware ..............................................................................................5
3. Usage Model ...............................................................................................................7
3.1. Units..................................................................................................................7
3.2. Interaction .........................................................................................................7
4. Defining Units .............................................................................................................9
4.1. Conceptual Model.............................................................................................9
4.1.1. Unit Identifiers .......................................................................................9
4.1.2. Unit Terms .............................................................................................9
4.2. Realization via the File System.........................................................................9
4.2.1. The SWPATH Environment Variable .....................................................10
4.2.2. Single Unit in a File .............................................................................10
4.2.3. Multiple Units in a File ........................................................................11
4.3. Unit Definitions Are Managed Outside of Specware .....................................12
5. The Specware Shell ..................................................................................................13
5.1. Overview.........................................................................................................13
5.2. Typechecking Specs........................................................................................14
5.3. Resolution of Unit Identifiers..........................................................................15
5.3.1. SWPATH-Based Unit Identifier..............................................................15
5.3.2. Relative Unit Identifiers .......................................................................17
5.4. Command Format ...........................................................................................19
5.5. Miscellaneous Commands ..............................................................................19
5.6. Processing a Unit ............................................................................................20
5.7. Showing a Unit ...............................................................................................22
5.8. Generating Proof Units ...................................................................................23
5.9. Evaluating Expressions ...................................................................................24
5.10. Generating Lisp Code ...................................................................................25
5.11. Generating Java Code ...................................................................................26
iii