Specware 4.1 Language 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

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
Type-correctness
Constructive
Lexical conventions
Symbols and Names
Comments
Units
Unit Identifiers
Specs
Morphisms
Diagrams
Target Code Terms
Proof Terms
Declarations
Import-declarations
Type-declarations
Type-definitions
Op-declarations
Op-definitions
Claim-definitions
Type-descriptors
Type-sums
Type-arrows
Type-products
Type-instantiations
Type-names
Type-records
Type-restrictions
Type-comprehensions
Type-quotients
Expressions
Lambda-forms
Case-expressions
Let-expressions
If-expressions
Quantifications
Annotated-expressions
Applications
Restrict-expressions
Op-names
Literals
Field-selections
Tuple-displays
Record-displays
Sequential-expressions
List-displays
Structors
Matches and Patterns
Matches
Patterns
A. Metaslang Grammar
B. Inbuilts and Base Libraries
Inbuilts
Boolean
Integer
Nat
Char
String
List
Compare
Option
Functions
  Next
  Disclaimer