AS/NZS ISO/IEC 15437:2003 (R2014)

Table of Contents

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

Abstract

Defines the syntax and semantics of the enhanced LOTOS language, named E-LOTOS. E-LOTOS is used for the formal descritpion of the behavioural aspects of distributed and concurrent systems in general and in the area of open distributed processing in particular.

RECONFIRMATION NOTICE
Technical Committee IT-015 has reviewed the content of this publication and in accordance
with Standards Australia procedures for reconfirmation, it has been determined that the
publication is still valid and does not require change.
Certain documents referenced in the publication may have been amended since the original
date of publication. Users are advised to ensure that they are using the latest versions of
such documents as appropriate, unless advised otherwise in this Reconfirmation Notice.
Approved for reconfirmation in accordance with Standards Australia procedures for
reconfirmation on 17 March 2014.
The following are represented on Technical Committee IT-015:
Australian Computer Society
Australian Society for Technical Communication (NSW)
Charles Sturt University
Department of Defence (Australia)
Griffith University
La Trobe University
National Association of Testing Authorities Australia
National ICT Australia
NSW Business Chamber
Quantitative Enterprise Software Performance
Systems Engineering Society of Australia
University of Technology, Sydney

Scope

This International Standard defines the syntax and semantics of the enhanced LOTOS language (ISO 8807), named E-LOTOS. E-LOTOS is used for the formal description of the behavioural aspects of distributed and concurrent systems in general and in the area of open distributed processing in particular.

General Product Information

Published
Document Type	Standard
Status	Current
Publisher	Standards Australia
ProductNote	Reconfirmed 20/05/2014. This standard has been reconfirmed in Australia in 2014 and remains current in New Zealand. Reconfirmation Notice 20/05/2014
Pages
ISBN
Committee	IT-015
Supersedes	DR 03092 CP