Go to the first, previous, next, last section, table of contents. Quantifiers

The logical quantifiers "for all" and "there exists" are written in Larch/C++ as \A (or \forall) and \E (or \exists). See section Simple Type Names for the syntax of built-in-type-name. See section 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 | \exists
quantified-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.