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)

---------------------- Page: 1 ----------------------
ISO/IEC 1381’71: 1996(E)
Contents
Page
xi
...........................................................................
Foreword
xii
Introduction .
1
...........................................................................
Scope
2
.............................................................
Normative References
.....................................................................
Definitions.
.....................................................
3.1 Structure of Formal Definition
3.2 Conventions .
.........................................................
3.2.1 Informative text
5
Conformity .
5
Specifications .
4.1
....................................................... 6
Basic Mathematical Notation
6
Logic Notation .
5.1
6
Basic Set Theory .
5.2
7
Cartesian Products .
5.3
.................................................... 8
5.4 Binary Relations and Functions
............................................................... 9
5.5 Finite Sequences
............................................................... 10
5.6 Finite Mappings
11
5.7 OrdinalNumbers .
................................................. 12
5.8 Definition by Transfinite Induction
................................................. 12
5.9 Cardinality and Cardinal Numbers
13
5.10 Structured Expressions .
.......................................... 15
5.11 Semantic Function and Predicate Definitions
16
5.12 UseofRecursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
17
Core Abstract Syntax .
17
6.1 Document .
17
6.2 Definitions .
17
6.2.1 Type Definitions .
19
6.2.2 State Definition .
19
6.2.3 Value Definitions .
19
6.2.4 Function Definitions .
20
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

---------------------- Page: 2 ----------------------
ISO/IEC 13817-1 : 1996(E)
6.3 Expressions 21
...................................................................
6.3.1 Local Binding Expressions 22
.................................................
Conditional Expressions 22
6.3.2
...................................................
22
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
25
........................................................
6.3.10 Tuple Constructor 25
.......................................................
6.3.11 Record Expressions.
25
......................................................
6.3.12 Apply Expressions
25
......................................................
6.3.13 Lambda Expression 26
......................................................
6.3.14 Is Expression 26
...........................................................
6.3.15 Literals
26
...............................................................
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
38
....................................................
7.2 The Semantic Domains 40
..........................................................
7.2.1 Basic Semantic Domains
40
...................................................
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
. . .
111

---------------------- Page: 3 ----------------------
ISO/IEC 13817-1: 1996(E)
72
8.3 Expressions .
74
8.3.1 Local Binding Expressions .
76
8.3.2 Conditional Expressions .
78
8.3.3 Unary Expressions .
78
8.3.3.1 Numeric Operations .
79
8.3.3.2 Logical Operation .
79
8.3.3.3 Set Operations .
80
8.3.3.4 Sequence Operations .
81
8.3.3.5 Map Operations .
82
8.3.4 Binary Expressions .
82
8.3.4.1 Numeric Operations .
..................................... 85
8.3.4.2 Numeric Comparison Operators.
85
8.3.4.3 Equality Operations .
............................................... 86
8.3.4.4 Logical Operations
............................................ 87
8.3.4.5 Logical Set Operations
88
8.3.4.6 Set Operations .
.............................................. 88
8.3.4.7 Sequence Operation
............................. 89
8.3.4.8 Sequence and Map Modification Operation
89
8.3.4.9 Map Operations .
.............................................. 90
8.3.4.10 Compose and Iterate
93
8.3.5 Quantified Expressions .
......................................................... 98
8.3.6 Iota Expression.
......................................................... 99
8.3.7 Set Expressions
104
8.3.8 Sequence Expressions .
........................................................ 106
8.3.9 Map Expressions
108
8.3.10 Tuple Constructor .
108
8.3.11 Record Expressions. .
110
8.3.12 Apply Expressions .
111
8.3.13 LambdaExpression .
112
8.3.14 Is Expression .
113
8.4 State Designators .
117
8.5 Statements .
117
8.5.1 Underlying Theory For Statements .
119
8.5.2 The Statement Evaluation Functions .
120
8.5.3 Local Binding Statements .
122
8.5.4 Block and Assignment Statements. .
124
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
135
8.6 Patterns and Bindings. .
136
8.61 Patterns .
.............................................. 141
8.6.1.1 Auxiliary Functions.
144
8.62 Bindings. .
................................................. 144
8.7 Auxiliarv Functions and Predicates
d
144
8.7.1 Expansion Functions. .
147
8.7.2 Functions for Extending the Environment .
151
8.7.3 Functions and Predicates to deal with the State .
8.7.4 Functions and Predicates to deal with Curried Functions .
153
154
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

---------------------- Page: 4 ----------------------
ISO/IEC 13817-1: 1996(E)
8.7.12 General Functions and Predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171
9 The Mathematical Concrete Syntax
178
.................................................
9.1 Document.l7 8
9.2 Definitions .
178
9.2.1 Type Definitions.
178
........................................................
9.2.2 State Definition
179
.........................................................
9.2.3 Value Definitions
179
........................................................
9.2.4 Function Definitions
179
......................................................
9.2.5 Operation Definitions
179
.....................................................
9.3 Expressions .
180
9.3.1 Bracketed Expressions
180
....................................................
9.3.2 Local Binding Expressions
180
.................................................
9.3.3 Conditional Expressions
180
...................................................
9.3.4 Unary Expressions
181
.......................................................
9.3.5 Binary Expressions
181
.......................................................
9.3.6 Quantified Expressions
182
....................................................
9.3.7 Iota Expression.
183
.........................................................
9.3.8 Set Expressions
183
.........................................................
9.3.9 Sequence Expressions
183
.....................................................
9.3.10 Map Expressions
183
........................................................
9.3.11 Tuple Constructor Expression
183
...............................................
9.3.12 Record Expressions.
183
......................................................
9.3.13 Apply Expressions
183
.......................................................
9.3.14 Lambda Expression
183
......................................................
9.3.15 Is Expressions.
183
..........................................................
9.3.16 Names .
183
9.4 State Designators
183
..............................................................
9.5 Statements
184
...................................................................
9.5.1 Local Binding Statements
184
..................................................
9.5.2 Block and Assignment Statements.
184
...........................................
9.5.3 Conditional Statements.
184
...................................................
9.5.4 Loop Statements
184
........................................................
9.5.5 Nondeterministic Statement
184
................................................
9.5.6 Call and Return Statements
185
................................................
9.5.7 Exception Handling Statements
185
.............................................
9.5.8 Identity Statement
185
.......................................................
9.6 Patterns and Bindings.
185
..........................................................
9.61 Patterns
185
...............................................................
9.6.2 Bindings.
185
..............................................................
9.7 Lexical Specification
185
............................................................
9.7.1 General .
185
9.7.2 Characters
186
.............................................................
9.7.3 Symbols. .
188
9.8 Operator Precedence
188
............................................................
9.8.1 The Family of Combinators
189
.................................................
9.8.2 The Family of Applicators
189
.................................................
9.8.3 The Family of Evaluators
189
..................................................
9.8.4 The Family of Relations
NO
...................................................
9.8.5 The Family of Connectives
190
.................................................
9.8.6 The Family of Constructors
190
................................................
9.8.7 Grouping
190
..........................................................
9.8.8 The Type Operators.
191
.....................................................
10 The Interchange Concrete Syntax 192
...................................................
10.1 Introduction .
192
10.2 Lexis .
192
V

---------------------- Page: 5 ----------------------
ISO/IEC 13817-1 : 1996(E)
10.3 Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192
I196
........................................................
I.1 The Quter J&stract Syntax
196
....................................................................
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
200
....................................................
11.3.1 Bracketed Expressions
208
.................................................
11.32 Local Binding Expressions
200
...................................................
11.3.3 Conditional Expressions
201
.......................................................
11.3.4 IJnary Expressions
....................................................... 201
11.3.5 Binary Expressions
.................................................... 202
~Kl.3~6 Quantified Expressions
202
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
204
..........................................................
lP.3.P5 Is Expressions.
..2Q 4
11.3.16Names. .
284
..............................................................
Il.4 State Designators
................................................................... 204
11.5 Statements
205
..................................................
11.5.1 Local Binding Statements
........................................... 205
11.5.2 Block and Assignment Statements.
285
...................................................
11.5.3 Conditional Statements.
206
........................................................
11.5.4 Loop Statements
................................................ 206
11.5.5 Nondeterministic Sta,tement
206
................................................
l-1.5.6 Call and Return Statements
206
.............................................
81.5.7 Exception Handling Statements
206
.......................................................
11.5.8 Identity Statement
207
..........................................................
11.6 Patterns and Bindings.
20’7
...............................................................
11.6.1 Patterns
207
11.6.2 Bindings .
208
............................................................
11.7 Lexical Specification
210
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
213
........................................
12.1.3.5 Pre-conditions of Operations
.......................................... 214
112.1.3.6 Guards of Error Handlers
Vi

---------------------- Page: 6 ----------------------
ISO/IEC 13817-1: 1996(E)
12.1.3.7 Quoted Post-conditions of Implicit Operations
...........................
214
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
214
.....................................
12.1.4 Notational Conventions.
................................................... 215
12.2 Syntaxes and Auxiliary Functions
.................................................. 215
12.2.1 Module ‘LOAS”
.......................................................... 215
12.2.2 Module “CAS”
215
..........................................................
12.2.3 Module “GetUnusedId”
................................................... 216
12.3 The Syntax Mapping Functions
.................................................... 216
12.3.1 Document
............................................................. 217
12.3.2 Definitions
.............................................................
220
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
242
.................................................
1X3.3.11 Tuple Constructor Expression
....................................... 243
12.3.3.12 Record Expressions
243
...............................................
12.3.3.13 Apply Expressions
............................................... 244
12.3.3.14 Lambda Expression.
.............................................. 244
12.3.3.151s Expressions
................................................... 245
12.3.3.16Names
245
........................................................
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
251
.......................................................
12.3.6.2 Bindings
252
.......................................................
12.3.7 Lexical Specification
...................................................... 253
12.3.7.1 General
253
.......................................................
12.3.7.2 Characters
253
.....................................................
12.3.7.3 Symbols
253
.......................................................
13 The Static Semantic Domains
.......................................................
255
13.1 Type Representations
255
...........................................................
13.1.1 Special Subclasses of Type Representations
256
.....................................
13.2 Environments
257
.................................................................
13.2.1 Accessing Environments
257
...................................................
vii

---------------------- Page: 7 ----------------------
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
276
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
..............................
...