6.8 Let Clauses

A let-clause can be used in a function specification to avoid repeating the same term several times within a spec-case. That is, a let-clause allows abbreviation within the rest of a spec-case. If a specification has more than one spec-case the scope of the abbreviations does not extend to subsequent spec-cases. However, the scope of the abbreviations introduced by a let-clause can be extended to several spec-cases by enclosing them in a pair of curly brackets ({ }). See section 6 Function Specifications, for the details of the syntax. See section 6.10 Case Analysis, for the meaning of a specification with multiple or nested spec-cases.

The syntax of the let-clause itself is as follows. See section 6.1.3.2 Quantifiers for the syntax of varId and sort-name.

let-clause ::= let be-list ;
be-list ::= varId : sort-name be term [ , varId : sort-name be term ] ...

As an example, the following specification uses a let-clause to avoid the use of ^ in the postcondition [Jonkers91]. Informally, it says that a call to transfer moves the prescribed amount of money from the source account to the sink account.

// @(#)$Id: transfer.lh,v 1.12 1997/07/24 21:14:36 leavens Exp $

#include "BankAccount.lh"

extern void transfer(BankAccount& source, BankAccount& sink, Money amt)
            throw();
//@ behavior {
//@   let presrc:BankAccount be source^, presink:BankAccount be sink^,
//@      src:Obj[Money] be presrc.credit, snk:Obj[Money] be presink.credit;
//@   requires source ~= sink /\ assigned(source, pre) /\ assigned(sink, pre)
//@            /\ src^ >= amt /\ amt >= 0;
//@   modifies src, snk;
//@   ensures snk' = snk^ + amt /\ src' = src^ - amt;
//@ }

A specification using a let-clause is syntactic sugar for a specification written without it. The meaning of such a specification is given by textually replacing the free occurrences of the defined variables with their definitions. Bindings are allowed to depend on previous bindings, so technically this replacement process starts by substituting the term which is bound to the last name. The last name's definition is substituted for that name, and then this desugaring recurses by processing the next to last name, and so on. In the example above, one would replace oldsink by presink.credit first, then continue backwards working on oldsrc, then presink, and finally presrc.

For example, the specification of transfer given above is equivalent to the following.

// @(#)$Id: transfer2.lh,v 1.12 1997/07/24 21:14:49 leavens Exp $

#include "BankAccount.lh"

extern void transfer(BankAccount& source, BankAccount& sink, Money amt)
            throw();
//@ behavior {
//@  requires source ~= sink /\ assigned(sink, pre) /\ assigned(source, pre)
//@           /\ source^.credit^ >= amt /\ amt >= 0;
//@  modifies source^.credit, sink^.credit;
//@  ensures sink'.credit' = sink^.credit^ + amt
//@     /\ source'.credit' = souce^.credit^ - amt;
//@ }

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