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.39Assertion statements

An assertion constrains the behavior of the running program for the purposes of error checking. An AsmL implementation may optionally halt the program’s run if an assertion’s constraint has not been met, but assertions do not otherwise affect the meaning the program's run. In particular, a precondition or postcondition may not cause an update statement to be evaluated. If it does, an error will occur.

There are three forms of assertions: preconditions, postconditions and data-oriented constraints. These are introduced by the keywords require, ensure and constraint, respectively.

The expression given by a precondition is a predicate that must evaluate to true if the constraint is to be satisfied. The predicate is evaluated in a context that includes the statement block's local field instances.

The expression given by a postcondition is a predicate that must evaluate to true if the constraint is to be satisfied. The predicate is evaluated in a context that includes statement block's local field instances and, if the statement block includes a return statement, a binding of the identifier result to the statement block's return value.

Constraints introduced within statement blocks are have the same syntax as constraints declared as members. See section above for the syntax. Like preconditions, constraints check that a Boolean condition is true. However, constraints offer the additional feature of checking that the condition is true even when updates to variables occur.

45. 
    Runtime assertion checking
    

require x >= 0

ensure result = x + 1

return ((((x + 1) * 2) - 2) / 2) + 1

step WriteLine(Incr(1))

step WriteLine(Incr(99))
The special form resulting selectExpr may be used within a postcondition to constrain the update set of the current step . The resulting expression returns the value that the variable designated by the selectExpr (see section 1.51.2) will have in the following sequential step of the current abstract state machine. This value is only known after the update set has been completly determined (that is, just prior to beginning of the subsequent sequential step).

Thus, the checking of a postcondition constraint that includes a "resulting expression" is not synchronized with the statement block in which it occurs. Instead, the constraint will be checked later, after all (parallel) updates have been calculated for the current step.

46. 
    Use of a resulting expression
    

require Counter >= 0

ensure resulting Counter = Counter + 1

Counter := ((((Counter + 1) * 2) - 2) / 2) + 1

step Increment()

step WriteLine(Counter)

step Increment()

step WriteLine(Counter)
Compatibility Note

The behavior of the resulting expression may differ from this description in the current AsmL2 implementation.

The current AsmL2 implementation does not take into consideration all of the updates. The resulting expression queries the statement block's contribution to the current update set of the expressions with respect to a given location (see 7.5.1). In other words, it yields the value of a location after any updates created within the block will have been applied.

Since the order of expression evaluation is not given, the values returned by "resulting expressions" in AsmL 2 cannot be predicted in every case without introducing substeps at a lower level of abstraction than given in the model. (The value will be predictable in cases where a "total" update has occurred.)

1.40Nondeterministic choice statements

A statement-level choose-expression begins with the keyword choose and includes a statement block. In this form, all of the bindings established by the binders clause will be available for reference within the statement block.

A statement-level choose-expression may optionally provide an ifnone clause. If the choose-expression provides no bindings (for instance, when choosing from the empty set), the ifnone statement block will be evaluated. In that case, the value of the choose-expression is the return value of the ifnone statement block. Otherwise, the return value is that of the statement block following the binders clause.

If no ifnone clause is provided for a statement-level choose-expression then it defaults to "ifnone skip".

47. 
    Statement-level nondetermism
    

S = {"a", "b", "c"}

choose i in S

WriteLine(i + " was chosen.")

1.41Return statements

return   ::= return exp

A return statement is used as the last statement of a block to indicate the return value of that block.

AsmL does not issue an error if the return value of a statement block (or method) is ignored in the calling context.

Note to users

Unlike many other languages, AsmL uses "return" to indicate the value returned from a statement block, not from a method. The return statement has no effect on control flow.

Download 0.93 Mb.

Share with your friends: