Go backward to 2.3 Terms Go up to 2 Language Go 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, #));