Contents
1 Introduction 6
1.1 Executable specifications 6
1.2 Other Approaches 8
1.3 Applications 9
1.4 Features 9
1.5 Design goals 10
1.6 Audience 10
1.7 Notation 10
1.7.1 Conventions for terminology 10
1.7.2 Syntax 11
1.7.3 Language version 11
1.8 Comments 11
2 Lexical Structure 11
1.9 AsmL source 11
1.10 Handling of control characters 12
1.11 Tokens 12
1.12 Comments 12
1.13 Identifiers 13
1.14 Literals 14
1.14.1 Null 14
1.14.2 Boolean literals 14
1.14.3 Integer literals 14
1.14.4 Literals for real numbers 15
1.14.5 String literals 15
1.14.6 Character literals 16
1.15 Keywords 16
3 Declarations 17
1.16 Block structure 18
1.17 Kinds of declarations 19
1.18 The Main() method 20
1.19 Names 20
1.20 Declaration Scope 20
1.20.1 Unique declarations required per scope 21
1.20.2 Shadowing of identifiers 21
1.20.3 Order unimportant within a scope 21
1.20.4 Closure of scope 22
1.21 Continuation of declarations 22
4 Values, Constructors and Patterns 23
1.22 Values 23
1.23 Constructors 23
1.24 Literal constructors 24
1.25 Datatype constructors 24
1.25.1 Instance constructors 24
1.25.2 Compound value constructors 25
1.25.3 Enum constructors 25
1.26 Collection constructors 26
1.26.1 Tuple construction 26
1.26.2 Set construction 26
1.26.3 Sequence construction 27
1.26.4 Map construction 27
1.27 Patterns 28
1.27.1 Universal patterns 29
1.27.2 Literal patterns 29
1.27.3 Identifier patterns 29
1.27.4 The type pattern 30
1.27.5 Tuple pattern 30
1.27.6 Datatype pattern 31
1.27.7 The maplet pattern 31
1.28 Binders 32
1.28.1 Parallel binding semantics 34
1.28.2 Order of bindings 34
5 Types 34
1.29 Type expressions 34
1.29.1 Disjunctive types 35
1.29.2 Option types 36
1.29.3 Product types 36
1.29.4 Named types 36
1.29.5 Instantiated types 36
1.30 Operations on types 37
1.31 Built-in types 38
1.32 Subtypes 39
1.33 Type Declarations 40
1.33.1 User-declared subtypes 40
1.33.2 Interface declarations 41
1.33.3 Datatype declarations 42
1.33.4 Datatype variants 42
1.33.5 Enumerations 44
1.33.6 Constrained types 45
1.33.7 Constraints on type parameters 47
6 Members 48
1.34 Fields 48
1.34.1 Type constraints on values of field instances 49
1.34.2 Constants 49
1.34.3 Variables 49
1.34.4 Initialization of field instances 50
1.34.5 Kinds of fields 50
1.34.6 Indexing field names 51
1.34.7 Indexing parameters 52
1.35 Methods 53
1.35.1 Kinds of methods 53
1.35.2 Functions and procedures 54
1.35.3 Operators 54
1.35.4 Conversion methods 55
1.35.5 Method parameters 55
1.35.6 Static method selection 56
1.35.7 Dynamic method selection 58
1.35.8 Return values 59
1.35.9 Recursive methods 59
1.35.10 Type-parameterized, generic methods 59
1.35.11 Constructor methods 59
1.35.12 Disambiguation of method names 60
1.36 Constraints 61
7 Statements and Expressions 61
1.37 Statement blocks 62
1.38 Local fields 63
1.39 Assertion statements 65
1.40 Nondeterministic choice statements 67
1.41 Return statements 67
1.42 Conditional expressions 68
1.42.1 If-then-else expressions 68
1.42.2 Match expressions 68
1.42.3 Defaults for conditionals 69
1.43 Try/catch expressions 70
1.44 Quantifying expressions 71
1.45 Selection expressions 72
1.46 Primary Expressions 74
1.46.1 Logical operations 74
1.46.2 Type query expressions 74
1.46.3 Type coercion expressions 74
1.47 Apply expressions 75
1.48 Atomic expression 76
1.49 Enumerated types 77
1.50 The do expression 79
8 State Operations 79
1.51 Update statements 80
1.51.1 Consistency of update statements 82
1.51.2 Locations 82
1.51.3 Partial and total updates 83
1.52 Parallel update blocks 83
1.53 Sequential blocks 84
1.53.1 Effect of recursion on sequential steps 85
1.53.2 Scope of constants and variables 85
1.53.3 Iterated steps 85
1.54 The skip statement 86
1.55 Processes 86
1.56 Agents 86
1.57 Exploration expressions 86
9 Namespaces 87
1.58 Unit of compilation (assembly) 87
1.59 Namespaces 87
1.60 Qualified names 88
1.61 Import directives 89
1.61.1 Units of compilation 90
1.62 Linkage 90
1.63 Literate programming environment 91
10 .NET Extensions 92
1.64 Modifiers 92
1.65 Attributes 93
1.66 Delegates 94
1.67 Properties 94
1.68 Events 94
1.69 Type integration 95
1.70 Reflection 95
11 Library 95
1.71 Set operations 95
1.72 Sequence operations 96
1.73 Map operations 96
1.74 String operations 96
12 List of Examples 97
2 Grammar 1
2.1 Lexical level 1
2.1.1 Identifiers 1
2.1.2 Literals 1
2.1.3 Boolean literals 1
2.1.4 Integer literals 1
2.1.5 Literals for real numbers 2
2.1.6 String literals 2
2.1.7 Character literals 2
2.1.8 Keywords 2
2.2 Unit of compilation (assembly) 3
2.3 Values, constructors and patterns 3
2.3.1 Constructors 3
2.3.2 Patterns 3
2.3.3 Binders 4
2.4 Type expressions 4
2.5 Type declarations 4
2.5.1 Type Parameters 4
2.5.2 Type Relations 4
2.5.3 Interface 5
2.5.4 Datatype declaration 5
2.5.5 Enumerations 5
2.5.6 Constrained Types 5
2.6 Members 5
2.6.1 Fields 5
2.6.2 Methods 6
2.6.3 Constraints 6
2.7 Statements and expressions 6
2.7.1 Local fields 6
2.7.2 Assertion statements 7
2.7.3 Nondeterministic choice statements 7
2.7.4 Return statements 7
2.7.5 Conditional expressions 7
2.7.6 Try/catch expressions 7
2.7.7 Quantifying expressions 7
2.7.8 Selection expressions 7
2.7.9 Primary Expressions 8
2.7.10 Apply expressions 8
2.7.11 Atomic expression 8
2.8 Runtime states 8
2.8.1 Update statements 8
2.8.2 Parallel update blocks 8
2.8.3 Sequential blocks 9
2.8.4 Exploration expressions 9
2.9 .NET Compatibility 9
2.9.1 Modifiers 9
2.9.2 Attributes 9
2.9.3 Delegates 9
2.9.4 Properties 10
2.9.5 Events 10
