LM3: a Larch Interface Language for Modula-3 A Denition and Introduction

Procedure parameters
Modula-3 allows the programmer to pass procedures as parameters to other procedures. This feature is well understood at the program level since one can just call the passed procedure just like any other procedure. However, at the speci cation level, it is the procedure’s speci cation that is of interest, not its implementation. \Calling » a speci cation has no meaning. The speci cation of a procedure is a predicate de ning a relation over states, so passing p as a parameter, to a procedure R, actually means providing a predicate representing p. This predicate can then be used (with renaming of p’s parameters) within the speci cation of R.
In order to be able to restrict the possible values of a procedure argument, we need to be able to talk about the speci cation of a formal procedure parameter in the REQUIRES clause. There is already a notation for giving the predicate specifying a procedure, that is REQUIRES MODIFIES ENSURES, which we can use. We extend the notion of a predicate to permit this form. This also allows us to place restrictions on a procedure type by using a REQUIRES MODIFIES ENSURES predicate in the type invariant.
Such a speci cation in the REQUIRES clause represents the weakest spec-i cation that any actual parameter has to meet. In reasoning about client code, the client uses the speci cation of the actual argument in place of the speci cation of the formal parameter.
We allow a speci er to refer to the components of a procedure P’s speci cation, using P.MODIFIES, P.REQUIRES and P.ENSURES. Alternatively, the predicate representing the full speci cation is accessible as P.SPEC. In either case, renaming is permitted.
As an example, consider the speci cation of a `parameterized’ sorting routine, where the actual ordering function is given as a parameter.
We could specify this as:
<* USING TotalOrder(R for <) *>
PROCEDURE
Sort(VAR data: ARRAY OF INTEGER;
ord: PROCEDURE(a, b:INTEGER): BOOLEAN); <* REQUIRES ord.SPEC IMPLIES
(MODIFIES NOTHING ENSURES RESULT\post = R(a, b))
AND size(data\pre) > 1
MODIFIES data
ENSURES FORALL i,j \in inds(data\pre)
ord.SPEC(data\post[i] for a,
data\post[j] for b,
i < j for RESULT\post)
AND permutation(data\pre, data\post) *>
This speci cation tells us that we are free to pass any function parameter whose speci cation is stronger than or equal to
(MODIFIES NOTHING ENSURES RESULTnpost = R(a; b))
or, in other words, has no side e ects and implements some total order.
Intermediate states
In some circumstances, particularly if procedure parameters are involved (see Section 2.3.1), it is necessary to be able to refer to states that are not visible to the outside world, even in atomic procedures. To facilitate this, LM3 allows predicates that are explicitly quanti ed over states.
In such predicates, a state is bound by a quanti er, such as s is below. This state may be used in any place that either of the distinguished states, pre and post, may occur. The operator, \eval, which takes a state and a variable to a value. So, v\pre and v\post are equivalent to \eval(pre, v) and \eval(post, v) respectively. For convenience, \eval(s, v) may be written as v\s.
For example, if we have a speci cation of a procedure:
PROCEDURE double(n : INTEGER) : INTEGER;
<* REQUIRES n > 0
ENSURES RESULT\post = 2 * n
*>
and a second procedure speci ed as :
PROCEDURE
twice(p: PROCEDURE(n: INTEGER): INTEGER,
i: INTEGER): INTEGER;
<* REQUIRES p.REQUIRES(i for n) AND
FORALL s: State
(p.SPEC(s for post, i for n, j for RESULT\post)
IMPLIES p.REQUIRES(s for pre, j for n))
ENSURES EXISTS s: State
(p.SPEC(s for post, i for n)
AND p.SPEC(s for pre, RESULT\s for n)
*>
then we know that a call of twice with double as an actual value for p is allowed, since the speci cation of double satis es the requirement on p. If we wanted to perform any reasoning about this call, then p.REQUIRES, for example, would be instantiated to the actual value of double.REQUIRES.
If we expand the predicates in such a call, we see for:
twice(double; 3)
the expanded predicate is:
9s : State
(3>0)
RESULTns = 2 3 ^
RESULTns > 0 ) RESULTnpost = 2 RESULTns
which indeed simpli es to RESULT\post = 12.
This example shows the need for quanti cation over states since we would be unable to refer to the intermediate result without such a mechanism.
Object types and methods
One of the ways in which Modula-3 di ers from its predecessors in the Modula family is that it has subtyping with inheritance. LM3 has to support these features, which have not been addressed in previous Larch interface languages.
There is a problem. There are two distinct uses of inheritance within the Object Oriented community, only one of which represents true subtyping. It is reasonable to assume that if a type T1 is a subtype of T, then any properties we specify of T would still be required of T1. Unfortunately, Modula-3 can not enforce this semantic restriction, and it is often the case that programmers use inheritance simply to avoid rewriting some code, without really preserving subtyping. This would make it impossible to specify anything meaningful about the subtype relationship. LM3 supports only disciplined use of inheritance. Anything that is speci ed about a type must also be true for all subtypes (modulo appropriate rebinding of rede ned operators). This will in certain cases require a programmer to perform actions (such as providing a new default method) that are not required by the programming language, per se, and certainly restricts the programmer’s freedom to override methods arbitrarily.
An object value can be regarded as a record with an associated suite of procedures, called methods, giving operations bound to that record. An object type has a supertype and inherits both the structure and the default operations of this supertype. The LM3 keyword, SELF, refers to the current instantiation of the object.
The INITIALLY clause of an object type is a post-condition on any use of the function NEW with this type. Since this is not syntactically checkable, it is a proof obligation. The invariant on the type must be true on instance creation, and preserved by methods.
The speci cation of a subtype inherits the speci cations of its supertype with its default methods and extends these speci cations with specializa-tions. Following the pattern of the Larch Shared Language, this inheritance is treated syntactically. Semantic interpretation is on the fully expanded form.
The Syntax of LM3
This section gives a complete description of the syntax of the LM3 language. Whilst much of this is paraphrased directly from the Modula-3 Report, it should be possible to follow the de nition without knowledge of the grammar given there. The LM3 grammar is a superset of the Modula-3 interface grammar.
The grammar presented here is a collection of the components presented previously; it does not go down to the token level. A complete parsing grammar is given in Appendix B.

1 Introduction 
1.1 Background
1.2 The relationship between Modula-3 and LM3
2 The LM3 specication language 
2.1 Interfaces
2.2 Declarations
2.3 Other Modula-3 features
3 The Syntax of LM3 
3.1 The LM3 reference grammar
4 The semantics and checking of LM3 
4.1 The translation functions
4.2 The LM3Trait
4.2.1 The interfaces
4.2.2 The trait
5 Examples 
5.1 The Threads interface
5.1.1 Mutex, Acquire, Release
5.1.2 Semaphore, P, V
5.1.3 Blocking and unblocking on condition variables
5.1.4 Alerts
5.2 The IO Streams interface
5.2.1 An IOStreams package
5.2.2 The Rd interface
5.2.3 The RdClass interface
Bibliography