Abstract This document describes AsmL, a specification language based on abstract state machines. Foundations of Software Engineering Microsoft Research (c) Microsoft Corporation. All rights reserved. Contents 1 Introduction 6

12List of Examples

Example 1 In-place sorting 7

Example 2 Indentation as block structure 18

Example 3 Indentation as block structure 19

Example 4 Declarations 19

Example 5 Continuation of declarations 22

Example 6 Literal constructors 24

Example 7 Constructing instances 24

Example 8 Constructing compound values 25

Example 9 Constructing enumerated values 25

Example 10 Constructing tuples 26

Example 11 Constructing sets 27

Example 12 Constructing sequences 27

Example 13 Constructing maps 28

Example 14 Symmetry of construction and pattern matching 28

Example 15 Pattern matching without binding 29

Example 16 Single-name patterns 29

Example 17 Type patterns 30

Example 18 Tuple pattern 30

Example 19 Destructing patterns for structures 31

Example 20 Maplet patterns 32

Example 21 Simple, iterated and nondeterministic bindings 33

Example 22 Type expressions 34

Example 23 Disjunctive type 35

Example 24 Type families 37

Example 25 Type operations 38

Example 26 Interface declaration 41

Example 27 Datatype variants 43

Example 28 Structure case as subtypes 43

Example 29 Enumeration with user-provided values 44

Example 30 Enum Ranges 44

Example 31 Constrained type 46

Example 32 Constraints on type parameters 47

Example 33 Field containing a compound value 51

Example 34 Indexing parameters vs. indexing field names 52

Example 35 Kinds of methods 53

Example 36 Example: Operator declaration 54

Example 37 Example: Conversion methods 55

Example 38 Static method selection 57

Example 39 Dynamic method selection 58

Example 40 User-provided constructor 59

Example 41 User-provided constructor with inheritance 60

Example 42 Disambiguation of method names 60

Example 43 Constraint declaration 61

Example 44 Local fields 64

Example 45 Runtime assertion checking 65

Example 46 Use of a resulting expression 66

Example 47 Statement-level nondetermism 67

Example 48 Quantifying expressions 72

Example 49 Value-level nondeterministic choice 73

Example 50 Selection expressions 73

Example 51 Type conversions of built-in types 75

Example 52 Invocation syntax 76

Example 53 Enumerated types 77

Example 54 Enumerable disjunctive types 77

Example 55 Enumerable structure type 78

Example 56 Enumerated class 78

Example 57 Enumeration of enum values 78

Example 58 Enumeration of constrained type 79

Example 59 Update statement 81

Example 60 Update statements 81

Example 61 Parallel update 83

Example 62 Sequential and parallel steps 85

Example 63 Skip statement 86

Example 64 Select expressions 87

Example 65 Namespaces 88

Example 66 Use of qualified names 88

Example 67 Import Directives 89

Example 68 Explicit qualification required 89

Example 69 Delegate 94