4 Larch/Java for design pattern

 The technique of design patterns aims to classify ``best practice'' solutions to problems recurring in the development of applications, in order to help and guide software builders. They can successfully exploit prior experience in the solution of a given design problem by applying the right pattern of design [MKMG97,GHJV95]. The usual notation used to describe design patterns is a mixture of informal and formal notations with annotated examples written in a particular programming language or in pseudocode. In [GHJV95] a catalog of most important design patterns is provided, each classified with a text template, which illustrates the motivation, the condition for the applicability, the structure and other information, and with class and object diagrams based on the OMT technique.

The use a formal notation as Larch/Java to describe design patterns has the usual advantages coming from the application effective formal techniques. Unlike other too abstract formal notations, the two tiered approach of Larch provides the designer with an effective guide for the concrete implementation of program modules.

Design patterns such as those described in [Lea97a] which deal with constructs and techniques to solve common concurrent design problem, can be formally studied in our framework. For example, let us consider the design pattern in which pairs of actions cannot co-occur, referred to as conflict sets in [Lea97a]. Suppose that $\{(op1,op2), (op2,op2)\}$ is the conflict set for the two operations $\{op1,op2\}$, i.e two op1 operations can execute concurrently, while an op2 should not run concurrently with an op1 or another op2 operation. A Larch/Java specification for such pattern is the following:

public class ConflictOperations {
uses oper1, oper2;
protected int op1=0;
protected int op2=0;
public void op1(...){
		composed of s1,do,s2;
		action s1{
		when op2=0 $\land$ lock=myId;
		modifies op1,lock;
		ensures op1=op1+1 $\land$ lock=nil;}
		action do {
		modifies self;
		ensures result=doaction(self);}
		actions s2 {
		when lock=myId;
		modifies op1,lock,ws;
		ensures op1'=op1-1 $\land$ (if op1'=0 then ws'={}) $\land$ lock=nil}
		}
 
public void op2(...){
		composed of r1,make,r2;
		action r1 {
		when op1=0 $\land$ op2=0 $\land$ lock=myId;
		modifies op2;
		ensures op2=op2+1;}
		action make {
		modifies self;
		ensures result=makeaction(self);}
		action r2{
		when lock=myId;
		modifies op1,ws;
		ensures op2'=op2-1 $\land$ (if op2'=0 then ws'={}) $\land$ lock=nil}
		}
}

Each operation is composed of several atomic actions. The scheduler may arbitrarily interleave actions of one operation with the actions of another one, provided that the execution order is maintained and the conditions of the when-clause are satisfied. The first operation, when invoked, waits for being executed, until it gets the lock and the variable op2 is zero, meaning that no other op2 operation is running. At this point the counter on op1 operations is incremented, the lock can be released and the second action do can be executed as soon as the scheduler gives it the control. The next action must instead wait to get the lock in order to properly modify the variable op1 after the execution of the operation and to awake the other threads in the waiting set if no other op1 operation is running. The specification for the other operation op2 is similar apart from the condition in the when clause, stating that no other operation can be executing concurrently as desired.

Note that in Larch/Java the synchronization constraints among the different methods are clearly specified and the pairs of pre/post conditions for the execution of each method define the modification of the state of the object as computation goes on.