SpecL:
A Formal Modeling and
Specification Language

Contents

1.  Introduction
     1.1. The Overall Structure of a Requirements Specification
     1.2. Underlying Principles
     1.3. Defining User-Level Specifications
     1.4. Relationship between an SpecL Specification and a Concrete User Interface
     1.5. Defining Specifications for Embedded Systems

2.  Syntactic and Lexical Elements of SpecL
     2.1. Identifiers
     2.2. Literal Values
     2.3. Punctuation Symbols and Expression Operators
     2.4. Comments
     2.5. Scoping
         2.5.1. Declaration Scopes
             2.5.1.1. Module Scopes
             2.5.1.2. Object and Operation Scopes
         2.5.2. Expression Scopes
         2.5.3. Scope Visibilty
     2.6. Specification Files
     2.7. Includes
     2.8. The Top-Level Interactive Scope
     2.9. SpecL Keywords and Standard Identifiers
     2.10. Naming Conventions

3.  Objects and Operations
     3.1. Defining Objects
     3.2. Defining Operations
     3.3. Component Expressions
         3.3.1. And Composition
         3.3.2. Or Composition
         3.3.3. Repetitive Composition
         3.3.4. Functional Composition
         3.3.5. Recursive Composition
         3.3.6. Common Uses of SpecL Composition Forms
         3.3.7. Composition Expressions in Operations
     3.4. Operation Typing and Functionality
     3.5. Names and Types
     3.6. Composite versus Atomic Objects
     3.7. Concrete Values
     3.8. The Representational Base of Object Hierarchies
     3.9. Default Operation Parameters
     3.10. Definition Short Forms

4.  Inheritance
     4.1. Precise Semantics of Inheritance
     4.2. Multiple Inheritance
     4.3. Parent Objects as Types
     4.4. Inheriting from Non-Tuples

5.  Modules

6.  User-Defined Attributes

7.  Formal Specifications
     7.1. Variable names
     7.2. Functional, Arithmetic, and Boolean Expressions
     7.3. List Operations
     7.4. Composite Object Selector Operations
     7.5. Logical Implication
     7.6. Quantifiers
     7.7. Let Expressions
     7.8. Pre/Postconditions, Equations, and Axioms
     7.9. Auxiliary Functions

8.  Formal Specification Examples
     8.1. Equational Specification
     8.2. Some Additional Equational Definitions
         8.2.1. A Bag-Like Object
         8.2.2. A LIFO-Structured Database
         8.2.3. A FIFO-Structured Database
         8.2.4. A Keyed Database
     8.3. Testing Equational Specifications
     8.4. Predicative Specification
         8.4.1. Quantification
         8.4.2. Combining Predicative and Equational Specification
         8.4.3. More on Auxiliary Functions
     8.5. Inheritance of Formal Specifications

References

A.  Summary of Entity Definition Forms
     A.1. Object Definition Forms
     A.2. Operation and Function Definition Forms

B.  Keyword Synonyms

C.  Functional Definition of Relational Attributes

D.  Complete SpecL Syntax