INCITS/ISO/IEC 13817-1 : 1996 : R2007

Foreword
Introduction
1 Scope
2 Normative references
3 Definitions
   3.1 Structure of Formal Definition
   3.2 Conventions
4 Conformity
   4.1 Specifications
5 Basic Mathematical Notation
   5.1 Logic Notation
   5.2 Basic Set Theory
   5.3 Cartesian Products
   5.4 Binary Relations and Functions
   5.5 Finite Sequences
   5.7 Finite Mappings
   5.7 Ordinal Numbers
   5.8 Definition by Transfinite Induction
   5.9 Cardinality and Cardinal Numbers
   5.10 Structured expressions
   5.11 Semantic Function and Predicate Definitions
   5.12 Use of Recursion
6 Core Abstract Syntax
   6.1 Document
   6.2 Definitions
   6.3 Expressions
   6.4 State Designators
   6.5 Statements
   6.6 Patterns and Bindings
7 Dynamic Semantic Domains
   7.1 The Domain Universe
   7.2 The Semantic Domains
8 The Dynamic Semantics
   8.1 Document
   8.2 Definitions
   8.3 Expressions
   8.4 State Designators
   8.5 Statements
   8.6 Patterns and Bindings
   8.7 Auxiliary Functions and Predicates
9 The Mathematical Concrete Syntax
   9.1 Document
   9.2 Definitions
   9.3 Expressions
   9.4 State Designators
   9.5 Statements
   9.6 Patterns and bindings
   9.7 Lexical Specification
   9.8 Operator Precedence
10 The Interchange Concrete Syntax
   10.1 Introduction
   10.2 Lexis
   10.3 Symbols
11 The Outer Abstract Syntax
   11.1 Document
   11.2 Definitions
   11.3 Expressions
   11.4 State Designators
   11.5 Statements
   11.6 Patterns and bindings
   11.7 Lexical Specification
12 The Syntax Mapping
   12.1 Structure and Style of the Definition
   12.2 Syntaxes and Auxiliary Functions
   12.3 The Syntax Mapping Functions
13 The Static Semantic Domains
   13.1 Type Representations
   13.2 Accessing Environments
   13.3 Well-formedness Classifications
   13.4 Type Relations
   13.5 Extended Abstract Syntax
14 The Static Semantics
   14.1 Documents
   14.2 Definitions
   14.3 Expressions
   14.4 State Designators
   14.5 Statements
   14.6 Patterns and Bindings
   14.7 Auxiliary Functions
Annex A (informative) - Extensions
Annex B (informative) - Tool conformity
      B.1 Semantic conformity of tools
Annex C (informative) - Modules
      C.1 Overview
      C.2 Requirements of Modularization
      C.3 Extant Approaches to Structuring Specifications
Annex D (informative) - Cross-references
      D.1 Cross References for the Dynamic Semantics
      D.2 Cross References for the Concrete Syntax
      D.3 Cross References for the Abstract Syntax
      D.4 Cross References for the Syntax Mapping
      D.5 Cross References for the Static Semantics
Annex E (informative) - Bibliography

Describes the model based specification language VDM SL (Vienna Development Method - Specification Language).