Abstract This paper is an introduction to specifying robust software components using AsmL, the Abstract State Machine Language. Foundations of Software Engineering Microsoft Research (c) Microsoft Corporation

Download 443.18 Kb.

Page	1/16
Date	28.01.2017
Size	443.18 Kb.
	#9777

1 2 3 4 5 6 7 8 9 ... 16

Introducing AsmL:

A Tutorial for the Abstract State Machine Language

December 19, 2001

Revised May 23, 2002

Abstract

This paper is an introduction to specifying robust software components using AsmL, the Abstract State Machine Language.

Foundations of Software Engineering -- Microsoft Research

(c) Microsoft Corporation. All rights reserved.

1 Introduction 1

1.1 Audience 1

1.2 Organization of the document 1

1.3 Notation 1

2 Models 2

1.4 Abstract state 2

1.5 Distinct operational steps 3

1.6 The evolution of state variables 3

3 Programs 6

1.7 Hello, world 7

1.8 Reading a file 7

4 Sequential Processes 10

1.9 Stopping conditions 10

1.9.1 Stopping for fixed points 10

1.9.2 Stopping for conditions 11

1.10 Sequences of steps 12

1.11 Iteration over collections 12

1.12 Guidelines for using steps 13

5 Updates 14

1.13 The update statement 14

1.14 When updates occur 15

1.15 Consistency of updates 16

1.16 Total and partial updates 17

6 Methods 18

1.17 Functions and update procedures 19

1.18 Local names for values 20

1.19 Method overloading 21

7 Values 22

1.20 What are values? 22

1.21 Structured values 22

1.22 Built-in values 23

8 Constraints 24

1.23 Assertions 24

1.24 Type constraints 25

9 Constants 25

10 Variables 26

11 Classes 28

1.25 Fields defined in a class 29

1.26 New instances of a class 29

1.27 Updates to instance variables 29

1.28 Instances as "references" 30

1.29 Derived classes 31

12 Structured Values 32

1.30 Structure cases 34

13 Sets 35

1.31 Sets as enumerated values 35

1.32 Sets given by value range 36

1.33 Sets described algorithmically 36

1.34 Set Operations 37

1.34.1 Union 37

1.34.2 Intersect 37

1.34.3 Size 38

14 Sequences 38

15 Parallel evaluation 40

1.35 Sequential iteration 41

16 Maps 42

1.36 Map Comprehensions 43

1.37 Maps with multiple arguments 44

1.38 Map Operations 44

1.38.1 Indices 44

1.38.2 Values 45

1.38.3 Union 45

1.38.4 Override (+) 45

1.39 Partial updates of maps 46

17 Nondeterminism 47

1.40 Nondeterministic choice 47

1.41 External nondeterminism 48

1.42 The nondeterminism of "new" 49

18 Enumerations 49

19 Conditionals 50

1.43 The If Statement 51

1.44 Logical Operators 52

1.44.1 The and operator 53

1.44.2 The not operator 53

1.44.3 The not operator 53

1.44.4 The implies operator 54

20 Patterns 54

21 Predicate Logic 54

1.45 forall..holds 55

1.46 The exists Quantifier 56

22 Table of examples 1

1Introduction

This paper is a basic introduction to AsmL (Abstract State Machine Language) and contains enough information so that, once you've read it, you should be able to write simple models. In addition to this manual, you may also want to read the paper called "Vending Machine Case Study," which uses many of these basic techniques. For a complete description of the AsmL language, see the reference manual, "AsmL: The Abstract State Machine Language."

1.1Audience

We assume no prior knowledge of the modeling approach used in this paper or any understanding of the mathematical underpinnings that make the language such a precise modeling tool. Even though this paper describes a language based on rigorous mathematical semantics, it is intended for a broad audience. The mathematics is there, but you don't need to concern yourself with it.

AsmL was designed to be accessible to anyone with a basic understanding of programming. A familiarity with one other programming language, such as Visual Basic, is enough to understand this paper.

Readers interested in the details of AsmL, and especially the technical features that provide its mathematical foundations, should refer to http://research.micosoft.com/foundations/AsmL. This Web site includes documentation and a publicly downloadable implementation of the AsmL tool.

1.2Organization of the document

Section 2 gives the overview. Subsequent sections provide more detail.

1.3Notation

The document consists of text and lines of AsmL source. AsmL source is formatted using a special style:

// This is AsmL source.

It is important to use this style when writing AsmL because this is how the AsmL tool knows what to extract from a document. Within the text, we format AsmL literals using a fixed-width font.

We use special text colors for terminology that is defined in the document. Such terms are printed in blue when they are defined and dark red when referenced. For example, we define a term as a phrase with special meaning. A term may appear anywhere in the document.

Notes to the reader use a faded color to distinguish them from the rest of the text:

This is a note.

Download 443.18 Kb.

Share with your friends:

1 2 3 4 5 6 7 8 9 ... 16