org.jmlspecs.jml4.rac
Class WrapperConstructorGenerator

java.lang.Object
  org.jmlspecs.jml4.rac.WrapperMethodGenerator
      org.jmlspecs.jml4.rac.WrapperConstructorGenerator

public class WrapperConstructorGenerator
extends WrapperMethodGenerator

Generates a wrapper constructor. A wrapper constructor is a constructor with the same signature as the constructor under translation, thus replacing it the constructor under translation is turned into a private internal method. A wrapper constructor forwards an incoming call to the internal method but wrapped with various assertion checks before and after the call forwarding, and it has the following general structure:

  S(T1 x1, ..., Tn xn) throws E1, ..., En {
    checkInv$static();
    checkPre$init$S(x1, ..., xn);
    evalOldExprInHC$static();
    boolean rac$ok = true;
    boolean rac$inv = true;
    try {
      [rac$result =] internal$init$S(x1, ..., xn);
      checkPost$init$S(x1, ..., xn);
    } catch (JMLPreconditionError e) {
      rac$ok = false;
      throw new JMLInternalPreconditionError(e);
    } catch (JMLNormalPostconditionError e) {
        rac$ok = false;
        throw new JMLInternalNormalPostconditionError(e);
    } catch (JMLExceptionalPostconditionError e) {
        rac$ok = false;
      throw new JMLInternalExceptionalPostconditionError(e);
    } catch (JMLAssertionError rac$er) {
        rac$ok = false;
      throw e;
    } catch (Throwable e) {
      rac$inv = false;
      try {
        checkXPost$init$S(x1, ..., xn, e);
      } catch (JMLAssertionError rac$er) {
        rac$ok = false;
        throw e;
      }
    } finally {
        if (rac$ok && rac$inv) {
           checkInv$instance$S();
      }
      if (rac$ok) {
           checkInv$static();
           checkHC$static();    
      }
    }
  }
 

Author:

Yoonsik Cheon and Amritam Sarcar

Constructor Summary

WrapperConstructorGenerator()
Creates a new wrapper generator.

Method Summary

ConstructorDeclaration

createConstructor(ConstructorDeclaration cons)

Methods inherited from class org.jmlspecs.jml4.rac.WrapperMethodGenerator

generate, headerToString, isHelperMethod

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

WrapperConstructorGenerator

public WrapperConstructorGenerator()

Creates a new wrapper generator.

Method Detail

createConstructor

public ConstructorDeclaration createConstructor(ConstructorDeclaration cons)