3 Preliminary design of Larch/Java

The Larch family of specification languages consists of the Larch Shared Language (LSL) and a collection of Larch Interface Languages (LIL), each tailored for a particular programming language [GHW85]. The peculiarity of Larch with respect to design specifications is the ``two tiers'' (or layers) approach it uses. The lower tier is the Larch Shared Language, an algebraic specification language which defines the mathematical abstractions used in the other tier, which is the behavior interface language in which predicate on pre and post condition over the execution of the operations are defined [GH93,Win87].

LSL traits are the units of LSL specifications introducing sorts and operators to represent terms and values and a set of equations to define some relevant properties. For common data structures like integers, sets, etc, Larch provides a collection of library traits, which can be reused to specify new objects or abstract values of some data type. The interface specification module describes the behavior of the operations by defining the relation between the state in which an operation is invoked and the state after the execution of the operation, through the definition of requires-modifies-ensures clauses.

Several LIL have been developed for the most common programming languages such as C [GH91], ADA [GHW85], and Modula-3 [BGHL91]. The most recent LIL are all object-oriented: Smalltalk [CL94b] and C++ [CL94a]. Interestingly, a Generic Interface Language has been proposed as a generic basis for the definition of new languages, which has been extended for the specification of concurrent objects with the definition of a generic concurrent interface language (GCIL) in [Ler91]. Finally, a preliminary proposal for Larch/CORBA-IDL has been recently published in [Siv95].

Larch/Java has been developed starting from the design of Larch/C++ with the modifications necessary to support concurrency features of Java. Leaving out most design details, in Larch/Java an additional when clause provides a mechanism for synchronization. A when clause states the condition for scheduling the corresponding operation once that the preconditions have been met. The identifier myId identifies the client which has invoked the operation; each object has a lock and a waiting set to represent Java mechanisms for thread support and mutual exclusion. In particular, the scheduler is responsible for the assignment of the lock to a waiting thread, while the client may release the lock and modify the set of threads waiting for a condition to be met. The following example shows a Larch/Java specification for a simple concurrent counter which uses the BCounterTrait LSL trait:

BCounterTrait: trait
  includes Natural(Nat)
  introduces
    newCounter: -> Counter
    inc: Counter -> Counter
    dec: Counter -> Counter
    value: Counter -> Nat
    isZero: Counter -> bool
    MAX: -> Nat
  asserts
    Counter generated by newCounter, inc
    Counter partitioned by value
    \forall c: Counter
      value(newCounter) ==0;
      value(inc(c)) == value(c) + 1;
      isZero(newCounter);
      0 < MAX;

This trait defines a bounded counter abstract data structure. Such an abstract definition is used to specify a CCounter class as follows:

public class CCounter { 
uses BCounterTrait;
invariant value(self) <= MAX  $\land$ value(self) > 0;
public int CCounter() {
		 modifies self;
		 ensures  self' = newCounter; }
public synchronized int value() {
		  requires lock=myId;
		  modifies lock;
		  ensures result = value(self $\hat{}$) $\land$ lock=nil; }
public synchronized void inc() {
		  when lock=myId $\land$ value(self$\hat{}$) < MAX;
		  modifies self,lock;
		  ensures  self' = inc(self $\hat{}$) $\land$ lock=nil; }
public void synchronized dec() {
		  when lock=myId $\land$ $\lnot$ isZero(self);
		  modifies self,lock;
		  ensures  self' = dec(self $\hat{}$) $\land$ lock=nil; }
}

The CCounter class defines a bounded counter which can be shared among several threads. The class specification includes the specification of three synchronized methods; namely these methods operate in mutual exclusion.