TransClass (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.jmlrac
Class TransClass

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.jmlrac.TransUtils
          org.jmlspecs.jmlrac.TransType
              org.jmlspecs.jmlrac.TransClass

All Implemented Interfaces:: Cloneable, Constants, Constants, Constants, RacConstants

public class TransClass
extends TransType

A class for translating JML class declarations. The translation produces a set of assertion check methods for the class and any necessary fields, e.g., to hold old values. This class implements the Template Method Pattern layed out by the abstract superclass TransType.

Version:: $Revision: 1.74 $
Author:: Yoonsik Cheon

Field Detail

classDecl

private final JmlClassDeclaration classDecl

Target class declaration to be translated.


 private invariant classDecl == (JmlClassDeclaration)typeDecl;

surrogateCacheNeeded

private boolean surrogateCacheNeeded

True if a cache for interface surrogates need be generated for the current class being translated.


 private invariant dynamicInvocationMethodNeeded 
                     ==> surrogateCacheNeeded;

See Also:: dynamicInvocationMethod(), surrogateCacheDeclaration()

Constructor Detail

TransClass

public TransClass(JmlClassDeclaration classDecl)

Constructs a TransClass object.

Parameters:: classDecl - target class declaration to be translated

Method Detail

translateField

protected JmlFieldDeclaration translateField(JmlFieldDeclaration fieldDecl)

Translates a JML field declaration, fieldDecl, e.g., handling final, model, spec_public, and spec_protected.

If this is a model field and it has no accessor method generated by represents clauses, generate the following form of default model accessor method:

 [[... model T m ...;]] ==
   protected T m() {
     throw new JMLNonExecutableException();
   }

The generated method declaration is added to the current class, classDecl and its name is added to the field modelMethods.

If the given declaration is a ghost field declaration, generates a pair of ghost field accessor methods (getter and setter), a private field for storing ghost values, and possibly an initialization block. The generated code has the following structure:

  private [static] T v;
  [static] {
     v = initializer;
  }
  public [static] T ghost$v$C() {
     return v;
  } 
  public [static] void ghost$v$C(T x) {
     v = x;
  }

The generated accessors are added to the current class declaration, and the new field declaration (with its initialization block) is stored into the input field declaration for later pretty-printing in the proper order.


 also
   requires fieldDecl != null;
   modifies modelMethods, classDecl.*;

Overrides:: translateField in class TransType

See Also:: #translateRepresents(JmlRepresentsDecl[]), #modelMethods

translateInvariant

protected void translateInvariant()

Translates invariant clauses of this class declaration. This method produces a couple of invariant check methods, one for the static invariants and the other for instance invariants.


 also
   modifies classDecl.*;

translateConstraint

protected void translateConstraint()

Translates constraint clauses of the target class. This method produces constraint check methods, old expression evaluation methods, and old expression fields, to be added to the translated class.


 also
   assignable classDecl.*;

See Also:: TransConstraint

translateBody

protected void translateBody(ArrayList inners,
                             ArrayList methods,
                             JPhylum[] fieldsAndInits)

Translates a class body of the target class declaration. This method is overridden here to generate a default constructor with assertion checking capability if the class has no constructor.

Overrides:: translateBody in class TransType

Parameters:

inners - inner classes

methods - mthod declarations

fieldsAndInits - field declarations


 also
   requires inners != null && methods != null && fieldsAndInits != null;

translateMethod

protected void translateMethod(JmlMethodDeclaration mdecl)

Translates a JML method declaration. A translation of JML method declaration produces four new methods, and the original method is renamed and made private-accessible:

Precondition checking method. A protected method to check the precondition of the original method (refer to the class PreconditionMethod).

Normal and exceptional postcondition checking methods. A couple of protected methods to check the normal and exceptional postconditions of the original method (refer to the classes PostconditionMethod and ExceptionalPostconditionMethod).

Wrapper method. A wrapper method that wraps the original method with pre and postcondition checking (refer to the class WappersMethod).
The translation also generate several new instance fields to store temporally values used by the assertion checking methods. There are three kinds of variables that are generated and declared as instance fields.
- Precondition variables.
- Pre (\pre) expression variables.
- Old (\old) expression variables.
- Specification variables.

Similarly, translation of JML constructor declaration also produces four new methods, and the original constructor becomes a wrapper method (refer to the class TransConstructor).

createMethodTranslator

protected TransMethod createMethodTranslator(JmlMethodDeclaration mdecl)

Creates a method translator for the given method declaration.

translateModelMethod

protected void translateModelMethod(JmlMethodDeclaration mdecl)

Translates the given model method (or constructor), mdecl. !FIXME!describe translation rules.

Overrides:: translateModelMethod in class TransType

specPublicMethodAccessor

private JmlMethodDeclaration specPublicMethodAccessor(JmlMethodDeclaration mdecl)

Returns an access method for the given spec_public (or spec_protected) method declaration, mdecl. The returned method has the following code structure.

 public [static] T specPublic$m(x1, ..., xn) {
   [return] m(x1, ..., xn);
 }


 requires mdecl.isSpecPublic() || mdecl.isSpecPublic();

specPublicConstructorAccessor

private JmlMethodDeclaration specPublicConstructorAccessor(JmlConstructorDeclaration mdecl)

Returns an access method for the given spec_public (or spec_protected) constructor declaration. The returned method has the following code structure.

 public static T specPublic$$init$(x1, ..., xn) {
   return new T(x1, ..., xn);
 }

where T is the name of type currently being translated.


 requires mdecl.isSpecPublic() || mdecl.isSpecPublic();

finalizeTranslation

protected void finalizeTranslation()

Performs a finialization of translation, e.g., generation of spec inheritance mechanism.

Overrides:: finalizeTranslation in class TransType

staticInvariantCheckInitializer

protected JmlMethodDeclaration staticInvariantCheckInitializer()

Returns a static initializer that checks whether static invariants are established by the initialization of this class. The returned static initializer simply calls the static invariant check method of this class.

constructionStatusAccessor

protected JmlMethodDeclaration constructionStatusAccessor()

Returns declarations of a private instance field and a protected access method for storing and accessing the status of an instance construction. The returned field and method are used to disable assertion checks while the "this" object is being constructed by the constructor.

generateAccessorsForInterfaceModelFields

private boolean generateAccessorsForInterfaceModelFields()

Generates access methods for all the model fields inherited from the interfaces of this class. The generated access method is either a default access method or a dynamic delegation method. If the inherited model field has no represents clauses in the interface hiearchy, a default access method is generated; otherwise, a dynamic delegation method is generated which makes a dynamic call to the corresponding access method of the interfeace's surrogate class.

See Also:: defaultModelFieldAccessor(CField), modelFieldDelegationMethod(CField, JmlTypeDeclaration)

interfaceModelFields

private JFieldDeclarationType[] interfaceModelFields()

Returns all model fields inherited from the interfaces of this class, but excluding those also inherited from the superclass chain.

toSet

private Set toSet(JFieldDeclarationType[] fdecls)

Returns a set containing elements from the given array.

defaultModelFieldAccessor

private JmlMethodDeclaration defaultModelFieldAccessor(CField field)

Returns a default accessor method for a model field. The returned method has the following form:

  public [static] T model$n() {
    throw new JMLNonExecutableException();
  }

modelFieldDelegationMethod

private JmlMethodDeclaration modelFieldDelegationMethod(CField field,
                                                        JmlTypeDeclaration tdecl)

Returns a model field delegation method for model field, field, whose represents clause is found in type tdecl. The returned method has the following form:

  public [static] T model$n() {
    Object obj = dynamic_delegation_to_accessor_method_in_tdecl();
    return unwrapped_obj;
  }

specPublicAccessor

protected JmlMethodDeclaration specPublicAccessor(CField field)

Returns a default access method for a spec_public field. The returned method has the following form:

  public [static] T spec$n() {
    return x;
  }

where x is the name of the given field.

addNewMethod

protected void addNewMethod(JmlMethodDeclaration mdecl)

Adds a new method declaration, mdecl, to the instrumented class.

defaultConstructor

private JmlConstructorDeclaration defaultConstructor()

Returns a default constructor for the target class declaration.

assertionInheritanceMethod

protected JmlMethodDeclaration assertionInheritanceMethod()

Returns a method declaration implementing dynamic inheritance using the Java's reflection facility. The returned method is often called an inheritance method. The inheritance method makes dynamic invocations to assertion check methods, given an assertion check method's class name, method name, formal parameter types, and actual arguments. If the target assertion check method returns a boolean value, that value is returned; otherwise, true is returned. An exception thrown by the targe method is transparently propagated to the caller.


 ensures \result != null;

surrogateCacheDeclaration

protected JmlMethodDeclaration surrogateCacheDeclaration()

Returns a field declaration for an interface surroagte cache with a cache lookup method and a cache update method. The returned value is of type JmlMethodDeclaration so that it can be added to the current type declaration by using addMember method.

dynamicInvocationMethod

protected JmlMethodDeclaration dynamicInvocationMethod()

Returns a method declaration that makes a dynamic call to the given method using the Java's reflection facility. The inheritance method makes dynamic invocations to a target method to is specified by its name, its owner's class name, formal parameter types, and actual arguments. The target method is typically an access method generated by the runtime assertion checker, such as an accessor for a model, ghost, spec_public, or spec_protected field, a setter for a ghost field, and an accessor for a spec_public or spec_protected method. The return value is that of the target method, if necessary, wrapped in an object. If the target method is not found, a instance of JMLNonExecutableException is thrown. If the target method throws a RuntimeException, including JMLNonExecutableException, the exception is rethrown; for other types of exceptions, an instanceof RuntimeException is thrown.

Overrides:: dynamicInvocationMethod in class TransType

receiver

protected String receiver(String clsName,
                          String clazz,
                          String receiver)

Returns a string form of code that, if executed, returns the receiver of for a dynamic call. This method is used by the method dynamicInvocationMethod to define a subclass-specific dynamic invocation method.


 also
 ensures \result.equals("rac$receiver(" +clsName+ ", " +receiver+ ")");

See Also:: TransType.dynamicInvocationMethod()