ISO/IEC 13817-1:1996

lSO/IEC
INTERNATIONAL
13817-l
STANDARD
First edition
1996-12-15
Information technology - Programming
languages, their environments and system
software interfaces - Vienna Development
- Specification Language -
Method
Part 1:
Base language
- Langages de programmation, leurs
Technologies de /‘information
environnemen ts et interfaces logiciel sys t&me - Mkthode de
- Langage de spkification -
d&eloppemen t de Vienne
Partie 1: Langage de base
Reference number
ISO/lEC 13817-I :1996(E)
ISO/IEC 1381’71: 1996(E)
Contents
Page
xi
...........................................................................
Foreword
xii
Introduction .
...........................................................................
Scope
.............................................................
Normative References
.....................................................................
Definitions.
.....................................................
3.1 Structure of Formal Definition
3.2 Conventions .
.........................................................
3.2.1 Informative text
Conformity .
Specifications .
4.1
....................................................... 6
Basic Mathematical Notation
Logic Notation .
5.1
Basic Set Theory .
5.2
Cartesian Products .
5.3
.................................................... 8
5.4 Binary Relations and Functions
............................................................... 9
5.5 Finite Sequences
............................................................... 10
5.6 Finite Mappings
5.7 OrdinalNumbers .
................................................. 12
5.8 Definition by Transfinite Induction
................................................. 12
5.9 Cardinality and Cardinal Numbers
5.10 Structured Expressions .
.......................................... 15
5.11 Semantic Function and Predicate Definitions
5.12 UseofRecursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Core Abstract Syntax .
6.1 Document .
6.2 Definitions .
6.2.1 Type Definitions .
6.2.2 State Definition .
6.2.3 Value Definitions .
6.2.4 Function Definitions .
6.2.5 Operation Definitions .
0 ISO/IEC 1996
All rights reserved. Unless otherwise specified, no part of this publication may be reproduced or
utilized in any form or by any means, electronic or mechanical, including photocopying and micro-
film, without permission in writing from the publisher.
ISO/IEC Copyright Office l Case postale 56 l CH-1211 Geneve 20 l Switzerland
Printed in Switzerland
ii
ISO/IEC 13817-1 : 1996(E)
6.3 Expressions 21
...................................................................
6.3.1 Local Binding Expressions 22
.................................................
Conditional Expressions 22
6.3.2
...................................................
6.3.3 Unary Expressions
.......................................................
6.3.4 Binary Expressions 23
.......................................................
6.3.5 Quantified Expressions 23
....................................................
........................................................
6.3.6 IotaExpression. 24
6.3.7 Set Expressions 24
.........................................................
6.3.8 Sequence Expressions 24
.....................................................
6.3.9 Map Expressions
........................................................
6.3.10 Tuple Constructor 25
.......................................................
6.3.11 Record Expressions.
......................................................
6.3.12 Apply Expressions
......................................................
6.3.13 Lambda Expression 26
......................................................
6.3.14 Is Expression 26
...........................................................
6.3.15 Literals
...............................................................
6.3.16 Identifiers 27
..............................................................
6.4 State Designators 28
..............................................................
6.5 Statements 28
...................................................................
6.5.1 Local Binding Statements 28
..................................................
6.5.2 Block and Assignment Statements.
........................................... 29
6.5.3 Conditional Statements. 29
...................................................
6.5.4 Loop Statements 29
........................................................
6.5.5 Non-Deterministic Sequences 30
...............................................
6.5.6 Call and Return Statements
................................................ 30
6.5.7 Exception Handling Statements
............................................. 31
6.6 Patterns and Bindings. 31
..........................................................
7 Dynamic Semantic Domains 34
........................................................
7.1 The Domain Universe 34
...........................................................
7.1.1 Basic Definitions. 34
........................................................
7.1.1.1 Complete Partial Orders and Fixed Point Definitions
...................... 34
7.1.1.2 Operators on Complete Partial Orders. 35
................................
7.1.2 A Universe of Complete Partial Orders 37
........................................
7.1.3 A Universe of Domains
....................................................
7.2 The Semantic Domains 40
..........................................................
7.2.1 Basic Semantic Domains
...................................................
7.2.2 Extended Semantic Domains.
............................................... 42
7.2.3 Semantic Domains for Evaluation Functions 43
....................................
7.2.4 Auxiliary Semantic Domains 45
................................................
8 The Dynamic Semantics 46
...........................................................
8.1 Document . 46
8.2 Definitions . 48
8.2.1 Type Definitions. 48
........................................................
8.2.1.1 The Verification Predicate for Types 49
..................................
8.2.1.2 Evaluation Functions for Types 50
......................................
8.2.2 State Definition 57
.........................................................
8.2.3 Value Definitions 57
........................................................
8.2.3.1 The Verification Predicate for Value Definitions
.......................... 58
8.2.3.2 The Evaluation Function for Value Definitions 61
...........................
8.2.4 Function Definitions 63
......................................................
8.2.4.1 Verification Predicates for Function Definitions 63
..........................
8.2.4.2 Evaluation Functions for Polymorphic Functions . 67
8.2.5 Operation Definitions 69
.....................................................
8.2.5.1 Verification Predicates for Operation Definitions . 69
8.2.5.2 Evaluation Functions for Operation Definitions . 70
. . .
ISO/IEC 13817-1: 1996(E)
8.3 Expressions .
8.3.1 Local Binding Expressions .
8.3.2 Conditional Expressions .
8.3.3 Unary Expressions .
8.3.3.1 Numeric Operations .
8.3.3.2 Logical Operation .
8.3.3.3 Set Operations .
8.3.3.4 Sequence Operations .
8.3.3.5 Map Operations .
8.3.4 Binary Expressions .
8.3.4.1 Numeric Operations .
..................................... 85
8.3.4.2 Numeric Comparison Operators.
8.3.4.3 Equality Operations .
............................................... 86
8.3.4.4 Logical Operations
............................................ 87
8.3.4.5 Logical Set Operations
8.3.4.6 Set Operations .
.............................................. 88
8.3.4.7 Sequence Operation
............................. 89
8.3.4.8 Sequence and Map Modification Operation
8.3.4.9 Map Operations .
.............................................. 90
8.3.4.10 Compose and Iterate
8.3.5 Quantified Expressions .
......................................................... 98
8.3.6 Iota Expression.
......................................................... 99
8.3.7 Set Expressions
8.3.8 Sequence Expressions .
........................................................ 106
8.3.9 Map Expressions
8.3.10 Tuple Constructor .
8.3.11 Record Expressions. .
8.3.12 Apply Expressions .
8.3.13 LambdaExpression .
8.3.14 Is Expression .
8.4 State Designators .
8.5 Statements .
8.5.1 Underlying Theory For Statements .
8.5.2 The Statement Evaluation Functions .
8.5.3 Local Binding Statements .
8.5.4 Block and Assignment Statements. .
8.5.5 Conditional Statements. .
........................................................ 126
8.5.6 Loop Statements
............................................... 129
8.5.7 Non-Deterministic Sequences
................................................ 130
8.5.8 Call and Return Statements
............................................. 131
8.5.9 Exception Handling Statements
8.6 Patterns and Bindings. .
8.61 Patterns .
.............................................. 141
8.6.1.1 Auxiliary Functions.
8.62 Bindings. .
................................................. 144
8.7 Auxiliarv Functions and Predicates
d
8.7.1 Expansion Functions. .
8.7.2 Functions for Extending the Environment .
8.7.3 Functions and Predicates to deal with the State .
8.7.4 Functions and Predicates to deal with Curried Functions .
8.7.5 Compute Functions. .
Generate Functions. . 156
8.7.6
M&e Functions . 157
8.7.7
GetFunctions . 159
8.7.8
Collector Functions. . 163
8.7.9
Selector Functions . 166
8.7.10
8.7.11 Tag-processing Functions . 169
iv
ISO/IEC 13817-1: 1996(E)
8.7.12 General Functions and Predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171
9 The Mathematical Concrete Syntax
.................................................
9.1 Document.l7 8
9.2 Definitions .
9.2.1 Type Definitions.
........................................................
9.2.2 State Definition
.........................................................
9.2.3 Value Definitions
........................................................
9.2.4 Function Definitions
......................................................
9.2.5 Operation Definitions
.....................................................
9.3 Expressions .
9.3.1 Bracketed Expressions
....................................................
9.3.2 Local Binding Expressions
.................................................
9.3.3 Conditional Expressions
...................................................
9.3.4 Unary Expressions
.......................................................
9.3.5 Binary Expressions
.......................................................
9.3.6 Quantified Expressions
....................................................
9.3.7 Iota Expression.
.........................................................
9.3.8 Set Expressions
.........................................................
9.3.9 Sequence Expressions
.....................................................
9.3.10 Map Expressions
........................................................
9.3.11 Tuple Constructor Expression
...............................................
9.3.12 Record Expressions.
......................................................
9.3.13 Apply Expressions
.......................................................
9.3.14 Lambda Expression
......................................................
9.3.15 Is Expressions.
..........................................................
9.3.16 Names .
9.4 State Designators
..............................................................
9.5 Statements
...................................................................
9.5.1 Local Binding Statements
..................................................
9.5.2 Block and Assignment Statements.
...........................................
9.5.3 Conditional Statements.
...................................................
9.5.4 Loop Statements
........................................................
9.5.5 Nondeterministic Statement
................................................
9.5.6 Call and Return Statements
................................................
9.5.7 Exception Handling Statements
.............................................
9.5.8 Identity Statement
.......................................................
9.6 Patterns and Bindings.
..........................................................
9.61 Patterns
...............................................................
9.6.2 Bindings.
..............................................................
9.7 Lexical Specification
............................................................
9.7.1 General .
9.7.2 Characters
.............................................................
9.7.3 Symbols. .
9.8 Operator Precedence
............................................................
9.8.1 The Family of Combinators
.................................................
9.8.2 The Family of Applicators
.................................................
9.8.3 The Family of Evaluators
..................................................
9.8.4 The Family of Relations
NO
...................................................
9.8.5 The Family of Connectives
.................................................
9.8.6 The Family of Constructors
................................................
9.8.7 Grouping
..........................................................
9.8.8 The Type Operators.
.....................................................
10 The Interchange Concrete Syntax 192
...................................................
10.1 Introduction .
10.2 Lexis .
V
ISO/IEC 13817-1 : 1996(E)
10.3 Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192
I196
........................................................
I.1 The Quter J&stract Syntax
....................................................................
11.1 Document
..19 6
11.2 Definitions .
........................................................ 196
11.2.1 Type Definitions.
......................................................... 197
~1.2.2 State Definition
........................................................ 198
11~2.3 Value Definitions
...................................................... 198
j-1.2.4 Function Definitions
..................................................... 198
11.2.5 Operation Definitions
....... 199
...........................................................
II.3 Expressions
....................................................
11.3.1 Bracketed Expressions
.................................................
11.32 Local Binding Expressions
...................................................
11.3.3 Conditional Expressions
.......................................................
11.3.4 IJnary Expressions
....................................................... 201
11.3.5 Binary Expressions
.................................................... 202
~Kl.3~6 Quantified Expressions
11.3.7 IotaExpression. .
......................................................... 202
1‘1.3.8 Set Expressions
..................................................... 203
l-1.3.9 Sequence Expressions
........................................................ 203
11.3.10MapExpressions
............................................... 203
lB.3.PP Tuple Constructor Expression
...................................................... 203
11.3.12 Record Expressions.
....................................................... 203
PP.3.13ApplyExpressions
...................................................... 204
Bl.3.14Lambda Expression
..........................................................
lP.3.P5 Is Expressions.
..2Q 4
11.3.16Names. .
..............................................................
Il.4 State Designators
................................................................... 204
11.5 Statements
..................................................
11.5.1 Local Binding Statements
........................................... 205
11.5.2 Block and Assignment Statements.
...................................................
11.5.3 Conditional Statements.
........................................................
11.5.4 Loop Statements
................................................ 206
11.5.5 Nondeterministic Sta,tement
................................................
l-1.5.6 Call and Return Statements
.............................................
81.5.7 Exception Handling Statements
.......................................................
11.5.8 Identity Statement
..........................................................
11.6 Patterns and Bindings.
20’7
...............................................................
11.6.1 Patterns
11.6.2 Bindings .
............................................................
11.7 Lexical Specification
12 The Syntax Mapping .
................................................ 210
12.1 Structure and Style of the Definition
.................................................... 210
12.1.1 Division into Modules.
.............................................. 210
12.P.l.J Module “OASZAS”
.................................................. 210
12.1.1.2 Module “OAS”
.................................................. 218
12.1.1.3 Module “CAY
............................................ 210
12.1.1.4 Module “GetUnusedId”
.................... 211
l-2.1.2 Pre-conditions in the VDM-SL Definition of the Syntax Mapping.
................................ 211
12.1.3 Transformation of a Document to CAS.Definitions
.............................. 211
12.1.3.1 The Introduction of Additional Identifiers
............ 212
12.1.3.2 The Generation of Quoted Pre- and Post-conditions for Functions
........... 212
12.1.3.3 The Generation of Quoted Pre- and Post-conditions for Operations
................................... 213
12.1.3.4 The Transformation of Expressions
........................................
12.1.3.5 Pre-conditions of Operations
.......................................... 214
112.1.3.6 Guards of Error Handlers
Vi
ISO/IEC 13817-1: 1996(E)
12.1.3.7 Quoted Post-conditions of Implicit Operations
...........................
12.1.3.8 The Transformation of Type Definitions
............................... 214
12.1.3.9 The Transformation of Value Definitions
............................... 214
12.1.3.10 The Transformation of the State
.....................................
12.1.4 Notational Conventions.
................................................... 215
12.2 Syntaxes and Auxiliary Functions
.................................................. 215
12.2.1 Module ‘LOAS”
.......................................................... 215
12.2.2 Module “CAS”
..........................................................
12.2.3 Module “GetUnusedId”
................................................... 216
12.3 The Syntax Mapping Functions
.................................................... 216
12.3.1 Document
............................................................. 217
12.3.2 Definitions
.............................................................
12.3.2.1 Type Definitions
................................................. 220
12.3.2.2 State Definition
................................................. 224
12.3.2.3 Value Definitions.
................................................ 225
12.3.2.4 Function Definitions
.............................................. 225
12.3.2.5 Operation Definitions
............................................. 232
12.3.3 Expressions
............................................................ 237
12.3.3.1 Bracketed Expressions
............................................. 239
12.X3.2 Local Binding Expressions
.......................................... 239
12.3.3.3 Conditional Expressions
........................................... 240
12.3.3.4 Unary Expressions
............................................... 241
12.3.3.5 Binary Expressions
............................................... 241
12.3.3.6 Quantified Expressions
............................................ 241
12.3.3.7 Iota Expression.
................................................. 241
12.3.3.8 Set Expressions
.................................................. 242
12.3.3.9 Sequence Expressions
............................................. 242
1X3.3.10 Map Expressions
.................................................
1X3.3.11 Tuple Constructor Expression
....................................... 243
12.3.3.12 Record Expressions
...............................................
12.3.3.13 Apply Expressions
............................................... 244
12.3.3.14 Lambda Expression.
.............................................. 244
12.3.3.151s Expressions
................................................... 245
12.3.3.16Names
........................................................
12.3.4 State Designators
........................................................ 246
12.3.5 Statements
............................................................. 246
12.3.5.1 Local Binding Statements
.......................................... 247
12.3.5.2 Block and Assignment Statements
.................................... 248
12.3.5.3 Conditional Statements
............................................ 248
12.3.5.4 Loop Statements
................................................. 249
12.3.5.5 NonDeterministic Statement
........................................ 250
12.3.5.6 Call and Return Statements
........................................ 250
12.3.5.7 Exception Handling Statements
...................................... 250
12.3.5.8 Identity Statement
............................................... 251
12.3.6 Patterns and Bindings
.................................................... 251
12.3.6.1 Patterns
.......................................................
12.3.6.2 Bindings
.......................................................
12.3.7 Lexical Specification
...................................................... 253
12.3.7.1 General
.......................................................
12.3.7.2 Characters
.....................................................
12.3.7.3 Symbols
.......................................................
13 The Static Semantic Domains
.......................................................
13.1 Type Representations
...........................................................
13.1.1 Special Subclasses of Type Representations
.....................................
13.2 Environments
.................................................................
13.2.1 Accessing Environments
...................................................
vii
ISO/IEC 13817-1 : 1996(E)
13.2.2 Upda,ting Environments . 258
13o3 WeII-formedness Classifications . 258
13.4 Type Relations . 259
13.4.1 Subtypes . 259
....................... 264
1X4.2 Overlapping Subtypes, Disjoint ‘Types and Overlapping Types
....................................... 267
13.4.3 Auxiliary Tvpe Relations and Functions
........................................................ 273
13.5 Extended Abstract &Max
d
.............................................................. 273
14 The Static Semantics
................................................................... 274
14.1 Documents
....................................... 275
14.1 0 1 Auxiliary Web-formedness Requirements
84.2 Definitions .
................................................. 276
14.2.1 Type and State Definitions
..... Ij ...................................... 277
14.2l,l Types and Type maps.
................................... 279
P4.2A. .2 Extraction of Type R,epresentations
..................................... 280
14.2.2 Value, Function, and Operation Definitions
........................................... 280
14.2.2.1 Simultaneous Definitions
...................... 281
14.2.2.2 Ordered Definition Groups and Definition Sequences
..................................................... 282
14.2.2.3 Definitions
................................. 285
14.2.2.4 Definition Groups and their Ordering
............................................ 286
14.22.5 Ordering of Definitions
...................................... 287
14.2.2.6 Asserted Visible Environments
.................................................. 289
14.2.2.7 Pre-Conditions
14*3 Expressions .
.......................................... 290
14.3J Expression Characteristic Predicates
......................................
14.3.2 Relaxations and Restriction of Predicates
............................................ 291
14.3.2.1 The Subsumption Rule
................................................ 291
14,3.2.2 The InType Rule
.................................................... 292
14.3@2.3 Union Close
..................................... 292
14.3.2.4 Sub-Environment Based Checks.
............................................. 294
14.3.3 Well-Formedness of Expressions
..................................................... 295
14.3.4 Bracketed Expression
................................................. 295
14.3.5 Local Binding Expressions
..................................................
14.3.5.1 Let Expression
.............................................
14.3.5.2 Let Be ST Expression
.................................................. 296
14.3.503 Def Expression
................................................... 296
14.3.6 Conditional Expressions
................................................... 296
14.3.6-l If Expression.
................................................ 297
14.3.6.2 Cases Expression
....................................................... 298
14.3.7 Unary Expressions
.............................................. 299
14.3.7.1 Numeric Operations
................................................ 300
14.3.7.2 Logical Operation
.................................................. 301
14.3.7.3 Set Operations
.............................................. 302
14.3.7.4 Sequence Operations
................................................. 303
14.3.7.5 Map Operations
........................................... 304
14.3.7.6 Map Inverse Expression.
....................................................... 304
14.3.8 Binary Expressions
.............................................. 305
14.3.8.1 Numeric Operations
..................................... 387
14.3.8.2 Numeric Comparison Operators.
............................................... 308
14.3.8.3 Equality operations
............................................... 308
14.30804 Logical Operations
............................................ 310
l-4.3.8.5 Logical Set Operations
.................................................. 311
14.3.8.6 Set Operations
.............................................. 311
14.3.8.7 Sequence Operation
............................. 312
14.3.8.8 Sequence and Map Modification Operation
................................................. 313
14.3.8.9 Map Operations
............................................. 315
14.3.8.10 Compose and Iterate.
..m
Vlll
ISO/IEC 13817-1 : 1996(E)
14.3.9 Quantified Expressions
....................................................
14.3.10 Iota Expression.
.........................................................
14.3.1lSet Expressions
.........................................................
14.3.12 Sequence Expressions
.....................................................
14.3.13 MapExpressions
.........................................................
14.3.14 Tuple Constructor
.......................................................
143.15 Record Expressions.
......................................................
14.3.16 Apply Expressions
.......................................................
14.3.17 Lambda Expressions
......................................................
14.3.18 Is Expressions.
..........................................................
14.3.19Names.
..32 6
............................................................
14.3.20Literals
...............................................................
14.3.21 Auxiliary Well-formedness Predicates
......................................... 327
14.4 State Designators
..............................................................
14.5 Statements
...................................................................
14.5.1 Local Binding Statements
.................................................. 329
14.5.2 Block and Assignment Statements.
...........................................
14.5.3 Conditional Statements.
...................................................
14.5.4 Loop Statements
........................................................
14.5.5 Non-Deterministic Statement
...............................................
14.5.6 Call and Return Statements
................................................
14.5.7 Exception Handling Statements
.............................................
14.5.8 Identity Statements
......................................................
14.6 Patterns and Bindings.
..........................................................
14.6.1 Patterns
...............................................................
14.6.1.1 Pattern Characteristic Predicates
.................................... 338
14.6.1.2 Relaxation of Pattern Characteristic Predicates
.......................... 340
14.6.1.3 Well-formedness of Patterns
........................................
14.6.2 Bindings .
14.6.3 Value Environment
.......................................................
14.7 Auxiliary Functions.
............................................................
14.7.1 Dependency Relations.
....................................................
14.7.1.1 Free and Defined Names
........................................... 348
14.7.1.2 Syntactical Sub-Components
........................................ 356
14.7.1.3 The Definitional Basis of Types
...................................... 361
14.7.2 Syntax Transformations
...................................................
14.7.3 Substitutions
...........................................................
14.7.4 Indirectly Defined Functions
................................................
14.7.5 Classification Functions
...................................................
A Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 372
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 2 Approach
.........................................................
ix
ISO/IEC 13817-1 : 1996(E)
................................. 376
C.3.3 The Manchester Approach (Fitzgeralc’l & Jones)
........................................... 377
C.3.4 The VVSL Approach (Middelburg)
.................................................... 377
C.3.5 The RAISE Approach.
..................................................................
D Cross-references
.......................................... 379
D.1 Cross References for the Dynamic Semantics
..................................... 379
D.1.1 Naming and Typesetting Conventions Used
...............................
D.I.2 Listing of Functions/Predicates: Alphabetic (uses) 380
............................................
D.2 Cross References for the Concrete Syntax 385
............................................
14.3 Cross References for the Abstract Syntax.
............................................ 390
D.4 Cross References for the Syntax Mapping.
............................................ 393
ID.5 Cross References for the Static Semantics
E Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 397
Figures
1 Structure of the syntax mapping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 210
1 Character set. 187
2 Interchange syntax: representation of symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192
X
ISO/IEC 13817-l: 1996(E)
Foreword
IS0 (the International Organization for Standardization) and IEC (the International Electrotechnical Commission)
form the specialized system for worldwide standardization. National bodies that are members of IS0 or IEC participate
in the development of International Standards through technical committees established by the respective organization
to deal with particular fields of technical activity. IS0 and IEC technical committees collaborate in fields of mutual
interest. Other international organizations, governmental and non-governmental, in liaison with IS0 and IEC, also
take part in the work.
In the field of information technology, IS0 and IEC have established a joint technical committee, ISO/IEC JTCl.
Draft International Standards adopted by the joint technical committee are circulated to national bodies for voting.
Publication as an International Standard requires approval by at least 75% of the national bodies casting a vote.
International Standard ISOLIEC 13817-1 was prepared by Joint Technical Committee, ISO/IEC JTC 1, Information
technology, Subcommittee SC 22, Programming languages, their environments and system software interfaces.
ISO/IEC 13817 consists of the following parts, under the general title Information technology - Programming
languages, their environments and system software interfaces - Vienna Development Method - Specification
Language:
- Part 1: Base language
Additional parts will specify modules and the development method.
Annexes A to E of this part of ISO/IEC 13817 are for information only.
xi
ISO/IEC 13817-1 : 1996(E)
Introduction
Historical background of the Vienna Development Method (VDM)
The Laboratory came into existence in 1961 when Professor
VDM was developed at the IBM Laboratory in Vienna.
Heinz Zemanek of the Technical University in Vienna decided to move his whole group to an industrial home.‘) They
had previously developed a computer called Mailufterl at the Technical University. From 1958 the group had been
(r the construction of one of the early compilers for the ALGOL 60
increasingly involved in software projects in&din,
programming language. As time went on they found it difficult to get adequate support for their projects and eventually
joined IBM. In the mid-1960s IBM decided to develop a new programming language for which the ambition was to
replace both FORTRAN and COBOL. The language, which was at first called New Programming Language (until
the National Physical Laboratories in the UK objected to the acronym - the language became known as PL/I), was
clearly going to be large and it was decided that it would be useful to try to apply formal techniques to its description.
Based on their own work __ and influenced by research work by Cal Elgot, Peter Landin and John McCarthy __ the
Vienna group developed an operational semantics definition of PL/I which they called ULD-3 (YJniversal Language
Description’; ULD-2 was the name applied to the IBM Hursley contribution to this effort - the language itself
was being developed mainly from Hursley along with the early compilers; ULD-1 was a term applied to the natural
language description of the language). The description of PL/I in ULD-3 style ran through three versions. These are
very large documents. Operational semantics is now seen as unnecessarily complicated as compared to denotational
semantics. However, to make the principles of denotational semantics applicable to a language like PL/I with arbitrary
transfer of control, procedures as arguments, complicated tasking, etc. required major theoretical break-throughs and
a considerable mathematical apparatus not available at the time. The effort of the formal definition uncovered many
language problems early and had a substantial influence on the shape of the language.
Towards the end of the 1960s serious attempts were made to use the ULD-3 description as the basis of compiler
designs. Many problems were uncovered: in general, one could say that the over-detailed mechanistic features of the
operational semantics definition considerably complicated the task of proving that compiling algorithms were correct.
But again one should be clear that the work was a technical achievement:
a series of papers was published that
0 language concept’s could be mapped into implementations which could be proved
described how various programmin,
correct from the description (e.g. in JL71). In addition, a series of proposals was made which could simplify t,he
task of developing compilers from a semantic description. One of these was an early form of an exit construct (HJ70)
which led to an interesting difference between the Vienna flavour 01 c c lenotational semantics and that used in Oxford.
Another VDM-like idea that, arose at this time was Peter Lucas’ twin rnuchine proof
...