The logical quantifiers "for all" and "there exists" are written
in Larch/C++ as \A (or \forall)
and \E (or \exists).
See section 5.2.3.1 Simple Type Names for the syntax of built-in-type-name.
See section 5.2.3.2 Class and Namespace Names for the syntax of class-name.
See section 8.3 Instantiation of Templates for the syntax of type-id.
quantifier ::= quantifier-sym quantified-list quantifier-sym ::=\A|\forall|\E|\existsquantified-list ::= varId:sort-name [,varId:sort-name ] ... varId ::= identifier sort-name ::= identifier [ sort-instance-actuals ] | class-name | built-in-type-name | typedef-non-class-or-enum-name | typedef-enum-name sort-instance-actuals ::=[sort-or-type [,sort-or-type ] ...]sort-or-type ::= identifier [ sort-instance-actuals ] | type-id
The sort of a term with quantifiers is Bool.
The term within the parentheses following the quantifiers must
also have sort Bool, assuming that the identifiers introduced by
the quantifiers have the declared sorts.
An identifier used as a sort-name should be the name of a sort
from one of the used traits.
Such a name may be parameterized as in LSL, with the sort name's parameters
following it in square brackets, such as String[char].
Note that a class-name is also considered a sort-name,
and it may be an instance of a template, such as Set<int>.
The grammar does not allow the two forms to be mixed:
if Set is known in the specification as a template-class-name,
then one must write Set<int>, or ident(Set)[int]
(as Set[int] will give a parse error, see section 4.6 Identifiers for the
syntax ident()).
The meaning of a term with quantifiers is the usual one from first-order logic. For example, the following is true.
\A i: int (i < INT_MAX \implies (i < (i + 1)))
The following is also true.
\A i: int (i > INT_MIN \implies (\E j: int (j < i)))
A quantifier introduces a scope (see section 2.6 Scope Rules).
For example, in the following,
the scope of the i declared in \E i:int
extends through (legalIndex(a,i) /\ (a[i])^ = i)
and so the function present
looks for an element of a that has a value (in the pre-state)
equal to its own index.
// @(#)$Id: present_bad.lh,v 1.9 1997/06/03 20:30:18 leavens Exp $
extern int present_bad(const int a[], int siz, int i) throw();
//@ behavior {
//@ requires 0 <= siz /\ assignedUpTo(a,siz);
//@ ensures result = (if (\E i:int (0 <= i /\ i < siz /\ (a[i])^ = i))
//@ then i else -1);
//@ }
However, if it finds such, it then returns the argument i,
rather than this index.
(See section 11.8 Pointer Types for the definitions
of the trait functions validUpTo,
which defines validUpTo(a,siz) to mean that the indexes 0
through siz-1 (inclusive) are valid indexes into the array
into which a points.)
If the intent was to search for i in a,
then the specification should have been written as follows.
// @(#)$Id: present_good.lh,v 1.8 1997/06/03 20:30:19 leavens Exp $
extern int present(const int a[], int siz, int i) throw();
//@ behavior {
//@ requires 0 <= siz /\ assignedUpTo(a,siz);
//@ ensures if (\E j:int (0 <= j /\ j < siz /\ (a[j])^ = i))
//@ then 0 <= result /\ result < siz /\ (a[result])^ = i
//@ else result = -1;
//@ }
Often the use of quantifiers can be avoided by writing a trait
which has an appropriate trait function.
For example, when a has sort Ptr[ConstObj[int]],
as in the above specifications, then the following predicate
can be written more succinctly as validUpTo(a,siz),
because the trait function validUpTo is defined in the
trait PointerWithNull,
which Larch/C++ automatically uses when the specification deals
with such pointer types
(see section 11.8 Pointer Types for details).
\A j: int ((0 <= j /\ j < siz) => legalIndex(a,j))
Most other cases where quantifiers are used to iterate over a collection of abstract values can also be made into trait functions; you can write them yourself if they are not standard.
Go to the first, previous, next, last section, table of contents.