AS/NZS ISO/IEC 15437:2003

1 - AS/NZS ISO/IEC 15437:2003 INFORMATION TECHNOLOGY-OPEN DISTRIBUTED PROCESSING-ENHANCEMENTS TO LOTOS (E-LOTOS)
4 - PREFACE
5 - CONTENTS
11 - 1 Scope
11 - 2 Conformance
11 - 3 Normative reference
11 - 4 Terms, definitions and notation
12 - 5 E-LOTOS grammar
12 - 5.1 Lexical Structure
12 - 5.1.1 Character set
13 - 5.1.2 Comments and separators
13 - 5.1.3 Identifiers
13 - 5.1.4 Reserved words
14 - 5.1.5 Identifiers classes
14 - 5.1.6 Non-terminals classes
15 - 5.2 Syntax of the language
15 - 5.2.1 Specification
16 - 5.2.2 Top-level declaration
16 - 5.2.3 Module body
16 - 5.2.4 Module expression
16 - 5.2.5 Module formal parameters
16 - 5.2.6 Interface expressions
16 - 5.2.7 Record module expression
17 - 5.2.8 Interface body
17 - 5.2.9 Formal parameter list
17 - 5.2.10 Renaming/Instantiation
17 - 5.2.11 Equations declaration
18 - 5.2.12 Simple equations declaration
18 - 5.2.13 Declarations
18 - 5.2.14 Expressions
18 - 5.2.15 Expression Atoms
19 - 5.2.16 Behaviour expressions
20 - 5.2.17 Disabling behaviour expression
20 - 5.2.18 Synchronization behaviour expression
20 - 5.2.19 Concurrency behaviour expression
20 - 5.2.20 Selection behaviour expression
20 - 5.2.21 Suspend/Resume behaviour expression
20 - 5.2.22 Interleaving behaviour expression
20 - 5.2.23 Behaviour term
21 - 5.2.24 Behaviour atom
22 - 5.2.25 Type expressions
22 - 5.2.26 Record type expressions
22 - 5.2.27 Value expressions
23 - 5.2.28 Record value expressions
23 - 5.2.29 Patterns
23 - 5.2.30 Gate parameter list
23 - 5.2.31 Actual parameter list
23 - 5.2.32 Exception parameter list
24 - 5.2.33 Record patterns
24 - 5.2.34 Behaviour pattern matching
24 - 5.2.35 Expression pattern matching
24 - 5.2.36 In parameter list
24 - 5.2.37 In parameter
24 - 6 E-LOTOS abstract syntax
24 - 6.1 Overview
25 - 6.1.1 Syntactic sugar
25 - 6.1.2 Abstract syntax
26 - 6.2 Concrete to abstract syntactic translation
26 - 6.2.1 Interface body
28 - 6.2.2 Formal parameter list
28 - 6.2.3 Declarations
31 - 6.2.4 Expressions
31 - 6.2.5 Expression atoms
34 - 6.2.6 Behaviour expressions
34 - 6.2.7 Interleaving behaviour expression
35 - 6.2.8 Behaviour atom
41 - 6.2.9 Type expressions
42 - 6.2.10 Record type expressions
42 - 6.2.11 Record value expressions
43 - 6.2.12 Gate parameter list
43 - 6.2.13 Actual parameter list
43 - 6.2.14 Exception parameter list
43 - 6.2.15 Record patterns
44 - 6.2.16 In parameter list
44 - 6.2.17 In parameter
45 - 7 E-LOTOS semantics
45 - 7.1 Overview
46 - 7.2 Static Semantics
46 - 7.2.1 Static semantic objects for Base
47 - 7.2.2 Judgements on static semantics for Base
48 - 7.2.3 Extended identifiers
49 - 7.2.4 Static semantic objects for Modules
49 - 7.2.5 Judgements on static semantics for Modules
50 - 7.2.6 Cycle freedom
50 - 7.2.7 Context morphism
50 - 7.2.8 Realization
50 - 7.2.9 Interface Instantiation
51 - 7.2.10 Interface Matching
51 - 7.2.11 Renaming/Instantiation
54 - 7.3 Untimed dynamic semantics
54 - 7.3.1 Untimed dynamic semantic objects for Base
55 - 7.3.2 Judgements on untimed dynamic semantics for Base
56 - 7.3.3 Dynamic semantic objects for Modules
57 - 7.3.4 Judgements on untimed dynamic semantics for Modules
58 - 7.3.5 Environment morphism
58 - 7.3.6 Signature Instantiation
58 - 7.3.7 Renaming/Instantiation
58 - 7.4 Timed dynamic semantics
59 - 7.4.1 Judgements on timed dynamic semantics
59 - 7.5 Write-many variables: the value substitution operator
62 - 8 The E-LOTOS modules
62 - 8.1 Specification
62 - 8.1.1 Specification
63 - 8.2 Top-level declaration
63 - 8.2.1 Module not constrained by an interface
63 - 8.2.2 Module constrained by an interface
64 - 8.2.3 Generic module not constrained by an interface
65 - 8.2.4 Generic module constrained by an interface
65 - 8.2.5 Interface declaration
66 - 8.2.6 Sequential top declaration
66 - 8.3 Module body
66 - 8.3.1 Block declaration
67 - 8.3.2 Module Expression
67 - 8.4 Module expression
67 - 8.4.1 Module aliasing not constrained by an interface
68 - 8.4.2 Module aliasing constrained by an interface
68 - 8.4.3 Generic module actualization not constrained by an interface
69 - 8.4.4 Generic module actualization constrained by an interface
69 - 8.4.5 Generic module renaming/instantiation
70 - 8.5 Module formal parameters
70 - 8.5.1 Single
70 - 8.5.2 Disjoint union
71 - 8.6 Interface expressions
71 - 8.6.1 Interface identifier
71 - 8.6.2 Simple renaming
71 - 8.6.3 Explicit body
72 - 8.7 Interface body
72 - 8.7.1 Type hiding the implementation
72 - 8.7.2 Type synonym
72 - 8.7.3 Constructed type
73 - 8.7.4 Named record type
73 - 8.7.5 Process declaration
74 - 8.7.6 Equations
74 - 8.7.7 Sequential declaration
74 - 8.8 Record module expression
74 - 8.8.1 Single
75 - 8.8.2 Disjoint union
75 - 8.8.3 Renaming tuple
75 - 8.9 Equation declarations
75 - 8.9.1 Equations declaration
76 - 8.9.2 Sequential
76 - 8.10 Simple equation declaration
76 - 8.11 Declarations
76 - 8.11.1 Type synonym
76 - 8.11.2 Type declaration
77 - 8.11.3 Named record type
77 - 8.11.4 Process declaration
78 - 8.11.5 Sequential declarations
79 - 9 The E-LOTOS base language
79 - 9.1 Introduction
79 - 9.2 Behaviours
79 - 9.2.1 Disabling behaviour expression
80 - 9.2.2 Synchronization behaviour expression
81 - 9.2.3 Concurrency behaviour expression
83 - 9.2.4 Selection behaviour expression
83 - 9.2.5 Suspend/Resume behaviour expression
84 - 9.2.6 Sequential composition
85 - 9.2.7 Action
86 - 9.2.8 Internal action
86 - 9.2.9 Succesful termination without values
86 - 9.2.10 Succesful termination
87 - 9.2.11 Inaction
87 - 9.2.12 Time block
87 - 9.2.13 Delay
88 - 9.2.14 Assignment
88 - 9.2.15 Nondeterministic Assignment
89 - 9.2.16 Choice over values
90 - 9.2.17 Trap
91 - 9.2.18 General parallel
93 - 9.2.19 Parallel over values
94 - 9.2.20 Variable declaration
94 - 9.2.21 Gate hiding
95 - 9.2.22 Renaming
97 - 9.2.23 Process instantiation
97 - 9.2.24 loop iteration
98 - 9.2.25 Case
98 - 9.2.26 Case with tuples
99 - 9.2.27 Signalling
100 - 9.3 Type expressions
100 - 9.3.1 Type identifier
100 - 9.3.2 Empty type
100 - 9.3.3 Universal type
100 - 9.3.4 Record type
101 - 9.4 Record type expressions
101 - 9.4.1 Singleton record
101 - 9.4.2 Universal record
101 - 9.4.3 Record disjoint union
102 - 9.4.4 Empty record
102 - 9.5 Value expressions
102 - 9.5.1 Primitive constants
102 - 9.5.2 Variables
102 - 9.5.3 Record values
103 - 9.5.4 Constructor application
103 - 9.6 Record value expressions
103 - 9.6.1 Singleton record
103 - 9.6.2 Record disjoint union
103 - 9.6.3 Empty record
104 - 9.7 Patterns
104 - 9.7.1 Record pattern
104 - 9.7.2 Wildcard
104 - 9.7.3 Variable binding
105 - 9.7.4 Expression pattern
105 - 9.7.5 Constructor application
106 - 9.7.6 Explicit typing
106 - 9.8 Record patterns
107 - 9.8.1 Singleton record pattern
107 - 9.8.2 Record wildcard
107 - 9.8.3 Record match
108 - 9.8.4 Record disjoint union
108 - 9.8.5 Empty record pattern
108 - 9.9 Record of variables
108 - 9.9.1 Singleton record variable
108 - 9.9.2 Record disjoint union
109 - 9.10 Behaviour pattern-matching
109 - 9.10.1 Single match
110 - 9.10.2 Multiple match
110 - 10 Predefined library
111 - 10.1 Booleans
113 - 10.2 Natural Numbers
116 - 10.3 Integral Numbers
119 - 10.4 Rational Numbers
122 - 10.5 Floating Point Numbers
123 - 10.6 Characters
124 - 10.7 Strings
124 - 10.8 Enumerated Type Scheme
126 - 10.9 Record Type Scheme
127 - 10.10 Set Type Scheme
130 - 10.11 List Type Scheme
132 - Annex A - Tutorial
132 - A.1 The base language
155 - A.2 The module language
166 - A.3 An E-LOTOS specification of the ODP trader
189 - Annex B - Guidelines for LOTOS to E-LOTOS translation
189 - B.1 Introduction
196 - Bibliography