ConstructorWrapper (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 ConstructorWrapper

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.jmlrac.TransUtils
          org.jmlspecs.jmlrac.WrapperMethod
              org.jmlspecs.jmlrac.ConstructorWrapper

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

public class ConstructorWrapper
extends WrapperMethod

A class for generating constructor wrappers. A constructor wrapper is a constructor that wraps a constructor with assertion check methods such as pre and postcondition check methods. The constructor under wrapping becomes a private method and called by the wrapper.

Version:: $Revision: 1.24 $
Author:: Yoonsik Cheon
See Also:: TransConstructor

Constructor Detail

ConstructorWrapper

public ConstructorWrapper(String typeName,
                          JmlConstructorDeclaration mdecl)

Construct a new instance.


 requires typeName != null && mdecl != null;

Parameters:: mdecl - constructor to be wrapped

Method Detail

generate

public JMethodDeclarationType generate()

Returns a constructor wrapper for the given constructor declaration. The constructor body is replaced by a new block of code that forwards constructor calls to the orginal constructor (which now becomes a private method) and performs appropriate assertion checks (such as pre- and postoncodition checks) before and after forwarding. The new body looks something like the following:

 C(T1 x1, ..., Tn xn) {
   checkPre(x1, ..., xn);
   try {
     internal(x1, ..., xn);
     checkPost(x1, ..., xn);
   }
   catch (JMLEntryPreconditionError e) {
     throw new JMLInternalPreconditionError(e); 
   }
   catch (JMLAssertionError e) {
     throw e;
   }
   catch (Throwable e) {
     checkXPost(x1, ..., xn, e);
   }
   finally {
     checkInv(x1, ..., xn);
 }


 also
   modifies methodDecl.*;
   accessible methodDecl;
   ensures \result != null;

Overrides:: generate in class WrapperMethod

buildWrapperBody

private JBlock buildWrapperBody(JExpression explicitSuper)

Returns a body for the constructor wrapper being built. Refers to the method generate() for the structure of the constructor body.


 assignable args, postArgs, xpostArgs;
 accessible methodDecl;
 ensures \result != null;

Parameters:: explicitSuper - explicit super/this call to be added as the first statement of the body to be built; if null, no such call is added.
See Also:: generate(), WrapperMethod.buildWrapperBody()

nocheckDuringInit

protected String nocheckDuringInit()

Returns code for bypassing assertion checks during the class and instance initialization. The returned code has the following structure.

  if (!VN_CLASS_INIT || !VN_INIT) {
     T(x1, ..., xn);
     return;
  }

Overrides:: nocheckDuringInit in class WrapperMethod

checkPrecondition

protected String checkPrecondition()

Returns code for checking precondition. The precondition is always checked. The returned code has the following structure.

  // check precondition
  if (JMLChecker.isActive(JMLChecker.PRECONDITION)) {
    JMLChecker.enter();
    checkPre$$init$$T(x1,...,xn);
    JMLChecker.exit();
  }

where T is the name of target type.

Overrides:: checkPrecondition in class WrapperMethod

See Also:: WrapperMethod.checkPrecondition()

checkPreInvariant

protected String checkPreInvariant()

Returns code for checking invariant in the pre-state. Constructors should preserve static invariants, and have to establish non-static invariants. However, helpers are exempted from the obligation. Thus, for helpers, an empty string is returned, and for non-helpers, the following form of code is returned.

  // check static invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT) && rac$constructed()) {
    JMLChecker.enter();
    checkInv$static();
    JMLChecker.exit();
  }

where T is the name of type being translated.

Overrides:: checkPreInvariant in class WrapperMethod

checkPostInvariant

protected String checkPostInvariant()

Returns code for checking invariant in the post-state. Constructors should preserve static invariants, and have to establish non-static invariants. However, helpers are exempted from the obligation. Thus, for helpers, an empty string is returned, and for non-helpers, the following form of code is returned.

  // check static invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT) && rac$constructed()) {
    JMLChecker.enter();
    checkInv$static();
    JMLChecker.exit();
  }
  // check instance invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT) && rac$constructed()) {
    JMLChecker.enter();
    checkInv$instance$T();
    JMLChecker.exit();
  }

where T is the name of type being translated.

Overrides:: checkPostInvariant in class WrapperMethod

checkPostInstanceInvariant

protected String checkPostInstanceInvariant()

Returns code for checking instance invariant in the post-state. Constructors have to establish non-static invariants. However, helpers are exempted from this obligation. Thus, for helpers, an empty string is returned, and for non-helpers, the following form of code is returned.

  // check instance invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT) && rac$constructed()) {
    JMLChecker.enter();
    checkInv$instance$T();
    JMLChecker.exit();
  }

where T is the name of type being translated.

checkPostStaticInvariant

protected String checkPostStaticInvariant()

Returns code for checking static invariant in the post-state. Constructors should preserve static invariants. However, helpers are exempted from this obligation. Thus, for helpers, an empty string isq returned, and for non-helpers, the following form of code is returned.

  // check static invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT) && rac$constructed()) {
    JMLChecker.enter();
    checkInv$static();
    JMLChecker.exit();
  }

evalOldInConstraint

protected String evalOldInConstraint()

Returns code for evaluating old expressions in static constraint. All non-helper constructors must preserve static constraints, but not instance constraints. Thus, an empty string is returned for helpers, and the following form of code for non-helpers.

  // eval old exprs in static constraint
  if (JMLChecker.isActive(JMLChecker.CONSTRAINT)) {
    JMLChecker.enter();
    evalOldExprInHC$satic(); 
    JMLChecker.exit();
  }

where T is the name of type being translated.

Overrides:: evalOldInConstraint in class WrapperMethod

checkConstraint

protected String checkConstraint()

Returns code for checking history constraints. All non-helper constructors must preserve static constraints, but not instance constraints. Thus, an empty string is returned for helpers, and the following form of code for non-helpers.

  // check static constraint
  if (JMLChecker.isActive(JMLChecker.CONSTRAINT)) {
    JMLChecker.enter();
    checkHC$static();
    JMLChecker.exit();
  }

where T is the name of type being translated.

Overrides:: checkConstraint in class WrapperMethod

callOriginalMethod

protected String callOriginalMethod()

Returns code for invoking the now-renamed original constructor. I.e., internal$m(x1,...,xn);.

Overrides:: callOriginalMethod in class WrapperMethod

checkPostcondition

protected String checkPostcondition()

Returns code for checking normal postcondition. The postcondition is checked only if the object is not being constructed. The returned code has the following structure.

  // check normal postcondition
  if (JMLChecker.isActive(JMLChecker.POSTCONDITION) 
      && rac$constructed()) {
    JMLChecker.enter();
    checkPost$$init$$T(x1,...,xn);
    JMLChecker.exit();
  }

where T is the name of the target type.

Overrides:: checkPostcondition in class WrapperMethod

checkXPostcondition

protected String checkXPostcondition()

Returns code for checking exceptional postcondition. The exceptional postcondition is checked only if the object is not being constructed. The returned code has the following structure.

  // check exceptional postcondition
  if (JMLChecker.isActive(JMLChecker.POSTCONDITION)
      && rac$constructed()) {
    JMLChecker.enter();
    checkXPost$$init$T(x1,...,xn,e);
    JMLChecker.exit();
  }

where T is the name of the target type.

Overrides:: checkXPostcondition in class WrapperMethod

isActive

protected String isActive(String type)

Returns a string representation of the condition that tests if the given type of assertion is active. Assertion checking is active only when the instance has completed its construction.

Overrides:: isActive in class WrapperMethod

identification

protected String identification(String state)

Returns a string that identifies the method being translated.

Overrides:: identification in class WrapperMethod

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

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.

Constructor Summary
`ConstructorWrapper(String typeName, JmlConstructorDeclaration mdecl)` Construct a new instance.

Method Summary
`private JBlock`	`buildWrapperBody(JExpression explicitSuper)` Returns a body for the constructor wrapper being built.
`protected String`	`callOriginalMethod()` Returns code for invoking the now-renamed original constructor.
`protected String`	`checkConstraint()` Returns code for checking history constraints.
`protected String`	`checkPostcondition()` Returns code for checking normal postcondition.
`protected String`	`checkPostInstanceInvariant()` Returns code for checking instance invariant in the post-state.
`protected String`	`checkPostInvariant()` Returns code for checking invariant in the post-state.
`protected String`	`checkPostStaticInvariant()` Returns code for checking static invariant in the post-state.
`protected String`	`checkPrecondition()` Returns code for checking precondition.
`protected String`	`checkPreInvariant()` Returns code for checking invariant in the pre-state.
`protected String`	`checkXPostcondition()` Returns code for checking exceptional postcondition.
`protected String`	`evalOldInConstraint()` Returns code for evaluating old expressions in static constraint.
`JMethodDeclarationType`	`generate()` Returns a constructor wrapper for the given constructor declaration.
`protected String`	`identification(String state)` Returns a string that identifies the method being translated.
`protected String`	`isActive(String type)` Returns a string representation of the condition that tests if the given type of assertion is active.
`protected String`	`nocheckDuringInit()` Returns code for bypassing assertion checks during the class and instance initialization.

org.jmlspecs.jmlrac Class ConstructorWrapper

ConstructorWrapper

generate

buildWrapperBody

nocheckDuringInit

checkPrecondition

checkPreInvariant

checkPostInvariant

checkPostInstanceInvariant

checkPostStaticInvariant

evalOldInConstraint

checkConstraint

callOriginalMethod

checkPostcondition

checkXPostcondition

isActive

identification

org.jmlspecs.jmlrac
Class ConstructorWrapper