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.44Quantifying expressions

Quantifying expressions return true or false depending on whether a condition (given by exp) has been met universally over some collection of bindings or existentially by at least one example.

The universal quantifier consists the keyword forall followed by one or more binders for which a given condition must hold (given by the holds clause) if the quantifier is true. If the binders produce no bindings (for instance, if they iterate over an empty set), then the expression given by the holds clause is not evaluated, but the value of the forall expression is true.

The bindings produced by the forall expression may be referenced within the expression given by the holds clause.

The existential quantifier consists the keyword exists followed by one or more binders. If all of the names given in the binders may be bound to values, then the existential quantifier is true. If the binders produce no bindings (for instance, if they iterate over an empty set), then the value of the exists expression is false.

48. 
    Quantifying expressions
    

return (1 = i mod 2)

v1 = forall i in S holds odd(i) // false

v2 = exists i in S where i > 4 // true

v3 = forall i in S where i > 4 holds odd(i) // false

v4 = forall i in S where i > 100 holds odd(i) // true

v5 = forall i in S holds exists j in S where i < j // false

v6 = exists i in S where exists j in S where i < j // true

v7 = exists i in S, j in S where i < j // true

v8 = exists i in S, j in S where i + 1 = j // true

v9 = forall i in S, j in S holds i mod j < 6 // true

WriteLine([v1, v2, v3, v4, v5, v6, v7, v8, v9])

1.45Selection expressions

A selection expression is used to query for values from a domain given by a comprehension clause. (Recall from above that comprehensions are in the form exp | binder1, binder2, ...)

The value of a selection expression depends upon the selector keyword.

• 
  For "any," the value of exp for any one of the bindings produced by the binders clause. The selection is nondeterministic.
  
• 
  The keyword "the" adds a constraint: there must be exactly one possible binding, or an error occurs.
  
• 
  The keywords "min" and "max" are used to select the smallest and largest values possible. (The operations ">" and "<" must be defined for the data type in question.)
  
• 
  The keyword "sum" causes the value returned to be the arithmetic sum of all values given by exp. (The operator "+" must be defined for the data type in question.)
  

49. 
    Value-level nondeterministic choice
    

let S = {1, 2, 3, 4, 5}

step

let y = any i | i in S where i < 4

step

WriteLine(z) // prints 1

step

let w = sum i + 1 | i in S

The selectors min, max and sum are deterministic and return the minimum element, maximum element and the sum of all elements described by the comprehension.

50. 
    Selection expressions
    

const T = {-1, 2, 3, 5, 7}

return (x mod 2 = 1)

let v1 = (any x | x in T where IsOdd(x) and x > 0)

let v2 = (the val | val in T where val notin S)

let v3 = (max x + y | x in S, y in T)

let v4 = (min x | x in S + T)
WriteLine([v1, v2, v3, v4])

// v1 is one of {3, 5, 7}

// v2 is -1

// v3 is 17

// v4 is -1
Although parsing without parentheses works, it is considered to be good style to put parentheses around every selection expression.

1.46Primary Expressions

Primary expressions consist of logical operations, arithmetic operations, and the invocation of methods.

The meaning of the logical operators is given above in 1.43.

The arithmetic and relational expressions are defined in the AsmL library. They appear in this reference only by virtue of their special syntactic form.

To be written: Give a precedence table.

1.46.1Logical operations

Alternate forms are provided for the case of "sequential and" and "sequential or" where the order of evaluation is significant. The meaning of the logical operators and then, or else and implies are given by the following table.

1.46.2Type query expressions

Type queries are Boolean expressions that return true if a value is of a given type. Type queries are in the form applyExpr is type. See section above for more about types.

1.46.3Type coercion expressions

AsmL allows the user to convert types using expressions in the form addExpr
as type. The type coercion operator invokes the converter method that applies to the type being converted.

Conversions among built-in types are provided in the runtime library. See the accompanying document: “AsmL Standard Library Reference”.

51. 
    Type conversions of built-in types
    

Main()
//conversions using convertors

step WriteLine(1b as Short) // prints 1

step WriteLine(1 as Double) // prints 1

// conversions using functions

step WriteLine(ToInteger(1.9)) // prints 2

step WriteLine(ToChar("a")) // prints 'a'

step WriteLine(ToSet([1,2,1])) // prints {1, 2} or {2, 1}

Download 0.93 Mb.

Share with your friends: