Specware 4.0 Language 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
Disclaimer
1. Introduction to Specware
What Is Specware?
What Is Specware For?
The Design Process in Specware
Stages of Application Building
Building a Specification
Refining your specifications to constructive specifications
Reasoning About Your Code
Abstractness in Specware
Logical Inference in Specware
2. Metaslang
Preliminaries
The grammar description formalism
Models
Sort-correctness
Constructive
Lexical conventions
Symbols and Names
Comments
Units
Unit Identifiers
Specs
Morphisms
Diagrams
Generate Terms
Proof Terms
Declarations
Import-declarations
Sort-declarations
Sort-definitions
Op-declarations
Op-definitions
Claim-definitions
Sorts
Sort-sums
Sort-arrows
Sort-products
Sort-instantiations
Sort-names
Sort-records
Sort-restrictions
Sort-comprehensions
Sort-quotients
Expressions
Lambda-forms
Case-expressions
Let-expressions
If-expressions
Quantifications
Applications
Annotated-expressions
Op-names
Literals
Field-selections
Tuple-displays
Record-displays
Sequential-expressions
List-displays
Structors
Matches and Patterns
Matches
Patterns
A. Metaslang Grammar
B. Base Libraries
Boolean
Integer
Nat
Char
String
List
Compare
Option
Functions
  Next
  Disclaimer