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

1.37Statement blocks

A number of contexts in the grammar expect statement blocks to provide the meaning of operations. Statement blocks occur inside:

• 
  a method declaration (see section above), as the method body, or operation performed when the method is invoked during the run of the program;
  
• 
  a parallel update statement (see section below), to effect the individual updates of each parallel binding;
  
• 
  a step of a sequential block (see section below), to configure an abstract state machine's variables in the following step;
  
• 
  a nondeterministic choice expression (see below), to operate on the value chosen;
  
• 
  each branch of an if-then-else expression (see section below), to indicate the operation performed if the conditions given in the conditional guard expression are satisfied;
  
• 
  each case of match expression (see section below), as the operation performed when the case's pattern matches a given value;
  
• 
  a try block (see section below), as the protected operation;
  
• 
  each case of exception handler (see section below), as the operation performed when an exception matches the selection criteria of the handler.
  

An optional return clause terminates the statement block. The expression given after the return keyword becomes the value of the statement block. If no return clause is used, the block does not return a value.

In general, AsmL statements execute in parallel. Updates to state do not take effect immediately. As a consequence, AsmL imposes only partial order on the evaluation of the expressions given in a statement block:

• 
  The expressions that give the initial values of the local fields are evaluated prior to any precondition assertions. Currently, local field instances are initialized in the order of their appearance in the block. (In a future version of AsmL, local fields will be initialized using a partial order given by resolving any field-to-field value dependencies.)
  
• 
  Preconditions will be evaluated prior to statement-level expressions in the block.
  
• 
  Statement-level expressions will be evaluated prior to providing the return value to the calling context. If there is no return value, then the evaluation of statement-level expressions in the invocation of the block is not considered to be synchronous (that is the caller need not wait for completion). The order of evaluation of each expression in block is not constrained. This includes the evaluation of the expression that provides the return value.
  
• 
  Postcondition assertions will be evaluated after the block's statement. An AsmL implementation must delay the evaluation of postconditions until all updates of the current step have been performed. In this sense, postconditions can be seen as constraints on the application of updates. There is no guarantee that the postcondition will be evaluated prior to the delivery of the statement block's return value in its invocation context.
  

1.38Local fields

local ::= letBinding
| { localVariableModifier } localVar
letBinding ::= [ let ] pat "=" exp
localVar ::= ( var | initially ) id
( as typeExp ["=" exp ] | "=" exp )

Statements that are similar to field declarations (see section above) in form and meaning may occur within statement blocks as a means of introducing local fields, either constants or variables.

Local fields have one field instance (see section above) for each invocation of their enclosing statement block. Local fields are both locally scoped and ephemeral; that is, they are visible in their scope during the lifetime of the runtime context associated with the particular invocation of the statement block.

The scope of local fields is the region of their statement block that follows their declaration. (There is one exception to this; see the "step" statement in section below.)

Local constants are introduced as the result of pattern-based bindings in the form let pattern "=" exp (see above). A pattern-based binding may establish more than one name/value association.

Note to users

The let keyword is optional when introducing local constants; however, its use is recommended as a matter of style to avoid confusion with the Boolean expression for equality testing, x = y.

As a way to introduce local variables the keyword "var" is interchangeable with the keyword "initially." The latter emphasizes the role of a local variable within the algorithm given in a method body.

Statements that introduce local variables have the same form as variables given by field declarations.

44. 
    Local fields
    

class Identifier
Main()

var x = new Identifier()

let (a, b) = (“abc”, “def”)

let c as String = a

let y = x

step

x := new Identifier()
step

WriteLine(x = y) // prints false

Note to users

The expression that provides the initial value of a local field is evaluated only once in any invocation of a statement block.

This means that any local fields initialized by nondeterministic expressions (including expressions that return a different value every time they are invoked, such as the class construction operator "new"), can be relied upon to contain just one value for the duration of the invocation context.

Download 0.93 Mb.

Share with your friends: