BS ISO/IEC 13817-1:1996

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
A Extensions
B Tool conformity
    B.1 Semantic conformity of tools
C Modules
    C.1 Overview
    C.2 Requirements of Modularization
          C.2.1 Language Facilities
                 C.2.1.0.1 Syntactic Separation
                 C.2.1.0.2 Explicit Import
                 C.2.1.0.3 Explicit Export
                 C.2.1.0.4 Parameterization
          C.2.2 Semantics
    C.3 Extant Approaches to Structuring Specifications
          C.3.1 The Syntactic Approach
          C.3.2 The Z Approach
          C.3.3 The Manchester Approach (Fitzgerald & Jones)
          C.3.4 The VVSL Approach (Middelburg)
          C.3.5 The RAISE Approach
D Cross-references
    D.1 Cross References for the Dynamic Semantics
          D.1.1 Naming and Typesetting Conventions Used
          D.1.2 Listing of Functions/Predicates:
                  Alphabetic (uses)
    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
E Bibliography
Figures
1 Structure of the syntax mapping
Tables
1 Character set
2 Interchange syntax: representation of symbols

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

This part of ISO/IEC13817 specifies the model based specification language VDM-SL (Vienna Development Method— Specification Language). It specifies:

• two representations: the mathematical and interchange;

• the syntax;

• the static semantics;

• the dynamic semantics;

• conformity for specifications and tools.

It does not specify:

• the proof obligations;

• the reification rules;

• the size or complexity of a specification that will exceed the capacity of any specific data processing system or the capacity of a particular tool, nor the actions to be taken when the corresponding limits are exceeded;

• the minimal requirements of a data processing system that is capable of supporting an implementation of a tool;

• the method that tools use for reporting errors.