Parameterized Schemes

use id1 for id2, . . . , idm for idn in class expression

In Java, there is no concept of renaming identifiers, therefore the renaming must be done before the specification is translated. In RSL a renaming class expression can be expanded into a basic class expression simply by renaming all the identifiers in the class expression according to the list of renaming pairs as shown in Example 2.7. In the translation into Java this expansion should be used.

Example 2.7 Renaming class expression.

schemeSTACK SCHEME = use stack for list in

LIST STATE Is equivalent to:

schemeSTACK SCHEME = class

variable stack : Int^∗ end

Example 2.8 Parameterized list in RSL.

schemePARAM LIST(E: class typeElem end) = class

variable

list : E.Elem^∗ ...

end

Example 2.9 Translation of a parameterized list in Java.

public c l a s s PARAM LIST<E> { public RSLList<E> l i s t ;

. . . }

in Example 2.8 could in Java be translated to the generic class shown in Example 2.9.

Generic methods must be dynamic in Java. The reason for this is that at the time of invocation of the method, the generic type must be known. In Java, the only way to declare the type of a generic class is to instantiate an object of the class with the generic type as type–parameter. A static method in Java does not require an instantiation of an object and the generic type can therefore not be determined. This is the reason that only dynamic methods are allowed to be generic.

Parameterization in RSL may be done with other kinds of declarations than type declarations since the parameterization is based on objects, which may be instances of class expressions containing any kind of declarations.

The scheme parameterization in RSL is a way of writing a more general specification, when a parameterized scheme is used either in an instantiation of an object or in a class expression of another scheme, it must be instantiated with an object. A parameterized scheme instantiated with an object can be expanded to a basic class expression.

This gives two possibilities for translation of an instantiation of a param-eterized scheme:

1. Rewrite parameterized schemes as basic class expressions and translate the basic class expressions.

2. Define a number of translations depending on the kind of parameteri-zation.

The first suggestion is obiviously the most simple solution, but it has the drawback that it creates one large class rather than dividing the proper-ties between several entiproper-ties which is the point of the parameterized scheme.

An example of an instantiated parameterized scheme and the equivalent ex-panded class expression is shown in Example 2.10 and Example 2.11.

Example 2.10 Instantiation of parameterized scheme.

schemeSIZE = class

value

size : Nat end

schemeSIZED INTLIST(S : SIZE) = class

variable list : Int^∗ value

empty : Unit →write list Unit empty() ≡ list := hi,

add : Int → write list Unit add(e) ≡ list :=hei b list

pre len list < S.size end

object S : class

value

size : Nat = 7 end

object USESIZEDLIST : SIZED INTLIST(S)

The second suggestion is much more complex to translate, but also pro-vides a solution which is more in line with the idea of the specification. First of all, this project only considers explicit specifications, therefore the use of

Example 2.11 Expanded instantiated parameterized scheme equivalent.

object USESIZEDLISTEXPANDED : class

variable list : Int^∗ value

empty : Unit → write list Unit empty() ≡ list := hi,

add : Int →write list Unit add(e) ≡list := hei b list

pre len list <7 end

parameterization to combine axioms are not considered. Only parameteriza-tion with variables, values and types are considered, parameterizaparameteriza-tion with channels are part of specification of parallel systems and is not considered.

However, the channel concept has some similarities with channels in Java, which may be placed as a field in a class, a discussion of possible transla-tion of channels can be found in Sectransla-tion 7.3.2. Therefore, the translatransla-tion of parameterization with variables and values could also be considered for channels.

As shown later, type definitions are translated as one or more classes, the translation of a parameterized scheme using types as a parameter could therefore be translated using generics classes in Java as presented in Example 2.9.

Parameterization with variables and values presents some other chal-lenges. Example 2.10 shows a scheme SIZED INTLIST which is a speci-fication of a list of limited size. The size of the list is put as a parameter to the scheme to allow different sizes of lists. The challenge of the translation of these schemes and objects is to ensure that it is possible to create lists of different sizes which may be referenced from other modules. It should noted that a value in RSL is constant, i.e., it cannot be changed, therefore, the translation should ensure that this is also the case. The translation of a value in the parameter of a scheme could be translated as an argument to the constructor of the class created and kept in the class as a private finalized field to ensure that it cannot be changed. The same translation could be used for variables except that the field in Java should not be declared ^final so that methods could manipulate the translation of the variable. Objects

used in the instantiation of a parameterized are not translated as objects are elsewhere. An example of the translation of the parameterized scheme in Example 2.10 is presented in Example 2.12.

Example 2.12 Translation of parameterized scheme presented in Example 2.10.

public c l a s s SIZED INTLIST { private f i n a l i n t s i z e ;

public RSLList<I n t e g e r> l i s t ; public SIZED INTLIST (i n t s i z e ) {

t h i s. s i z e = s i z e ; }

public void empty ( ) {

l i s t = new RSLListDefault<I n t e g e r>() ; }

public void add (i n t e ) { a s s e r t l i s t . l e n ( ) < s i z e ;

l i s t = (new RSLListDefault<I n t e g e r>(e ) ) . c o n c a t ( l i s t ) ;

} }