Go backward to 2.3 TermsGo up to 2 LanguageGo forward to 2.5 Values |

[

=*Formulas**Formula*`,`

*Formula*A (possibly empty) sequence of formulas separated by commas.

pred areOrdered(a, b, c, d) <=> and(

__<=(a, b), <=(b, c), <=(c, d)__); > predicate areOrdered/4.[

=*Terms**Term*`,`

*Term*A (possibly empty) sequence of formulas separated by commas.

fun sumSquares(a, b) = +(

__*(a, a), *(b, b)__). > function sumSquares/2.[

=*IteratorVariables**IteratorVariable*`,`

*IteratorVariable*A (possibly empty) sequence of iterator variables separated by commas.

option universe = nat(1,10); > universe of discourse set. formula forall(

__x, y in nat(1, x), z = y__: <=(y, z)); > true.[

=*ConstrainedVariables**ConstrainedVariable*`,`

*ConstrainedVariable*A (possibly empty) sequence of constrained variables separated by commas.

fun minus(

__x: Nat, y in nat(1, x)__) = -(x, y); > function minus/2.[

=*BoundVariables**BoundVariable*`,`

*BoundVariable*A (possibly empty) sequence of bound variables separated by commas.

term let(

__x = 1, y = 2__: +(x, y)); > 3.

=*IteratorVariable*

|*Variable*

|*TypedVariable**BoundVariable*An

*iterator variable*is a variable that iterates over a sequence of values: a plain variable (iterating over the universe of discourse), a typed variable (iterating over some domain), or a bound variable (iterating over a single value).option universe = nat(1, 3); > universe of discourse set. term set(

__x__,__y in nat(1, x)__,__p = tuple(x, y)__: true, p); > > <1, 1>, <2, 1>, <2, 2>, <3, 1>, <3, 2>, <3, 3>.

=*ConstrainedVariable*

|*Variable*

|*TypedVariable**CheckedVariable*A

*constrained variable*is a variable whose domain may be restricted: a plain variable (not constrained), a typed variable (constrained by a domain), or a checked variable (constrained by a predicate).pred isMultiple(

__x: Nat__,__y in nat(1, x)__) <=> exists(z in nat(1, x): =(x, *(y, z))); > predicate isMultiple/2.

=*Variable**Name*A name represents a variable if it occurs in the scope of a corresponding variable declaration of some quantifier or if it is declared as a parameter in a predicate/function definition.

fun a = 0; > function a/0. formula forall(

__x__in nat(2,10): not(=(a, -(__x__, 1)))); > true. fun f(__x__) =__x__; > fun f/1.

=*TypedVariable**Name*`in`

*Term*A typed variable is a name whose value range is constrained by a

*domain*(an interval or a set). It is an error to attempt to bind to the variable a value that is not from the specified domain (such an attempt is detected if parameter checking is switched on).fun -1(

__x in nat(1, 100)__) = -(x, 1); > function -1/1.

=*BoundVariable**Name*`=`

*Term*A

*bound variable*receives its value from the denoted term. The token ``=`

' should be surrounded by whitespace because it can be also part of a a name.term let(

__x = 7__: *(2, x)); > 14. term let(x=7: *(2, x)); > ERROR: unexpected ':'.

=*CheckedVariable**Name*`:`

*Name*A checked variable is a name whose value range is constrained by a predicate. The second name must denote a unary predicate; it is an error to attempt to bind a value to the variable that is not satisfy the predicate (such an attempt is detected if parameter checking is switched on).

pred isEven(

__n: Nat__) <=> exists(m in nat(0, n): =(n, *(2, m))); > predicate isEven/2. fun half(__n: isEven__) = such(m in nat(0, n): =(n, *(2, m))); > function half/2.*Name*A name is any sequence of non-whitespace characters that does not start with a decimal digit and that does not include any of the characters `

`(`

', ``)`

', ``,`

', ``:`

', ``;`

'.term

__+3__(__xVal__,__f_0__(__y__,));__#__

Maintained by: Wolfgang Schreiner

Last Modification: September 16, 2004