ASML REFERENCE

AsmL: The Abstract State Machine Language

October 7, 2002 (revised September 2, 2006)

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.

1 Introduction 1

1.1 Executable specifications 1

1.8 Comments 6

2 Lexical Structure 6

1.9 AsmL source 6

1.10 Handling of control characters6

1.11 Tokens 6

1.12 Comments 7

1.13 Identifiers 7

1.14 Literals 8

1.15 Keywords 10

3 Declarations11

4 Values, Constructors and Patterns 17

1.22 Values 17

1.23 Constructors 18

1.24 Literal constructors 18

1.25 Datatype constructors 18

i

1.26 Collection constructors 20

1.27 Patterns 22

1.28 Binders 27

5 Types 29

1.29 Type expressions 29

1.35 Methods 48

1.36 Constraints 56

7 Statements and Expressions 58

1.37 Statement blocks 58

1.38 Local fields 60

1.39 Assertion statements 61

1.40 Nondeterministic choice statements 63

1.41 Return statements 64

1.42 Conditional expressions 64

1.43 Try/catch expressions 66

1.49 Enumerated types 73

1.50 The do expression 76

ii

1.51 Update statements 77

1.52 Parallel update blocks 80

1.53 Sequential blocks 81

9 Namespaces 84

1.59 Namespaces 84

1.60 Qualified names 85

1.61 Import directives 85

1.62 Linkage 87

1.63 Literate programming environment 88

10 .NET Extensions 89

1.64 Modifiers 89

1.65 Attributes 90

1.66 Delegates 90

1.67 Properties 91

11 Library 92

1.74 String operations 93

12 Grammar 95

iii