org.jmlspecs.jml4.rac
Class ConstraintMethod

java.lang.Object
  org.jmlspecs.jml4.rac.AssertionMethod
      org.jmlspecs.jml4.rac.InvariantLikeMethod
          org.jmlspecs.jml4.rac.ConstraintMethod

public class ConstraintMethod
extends InvariantLikeMethod

Generates assertion check methods for history constraints.

Author:

Amritam Sarcar, Yoonsik Cheon

Method Summary

RacMethodDeclaration

generate(java.lang.StringBuffer stmt, java.util.Set<ASTNode> terms, RacResult result, boolean inherit, boolean isTopLevelInstance, java.lang.String methodPrefix) Overridden method to generate a type-level constraint check method.

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

generate

Methods inherited from class java.lang.Object

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

Method Detail

generate

public RacMethodDeclaration generate(java.lang.StringBuffer stmt,
                                     java.util.Set<ASTNode> terms,
                                     RacResult result,
                                     boolean inherit,
                                     boolean isTopLevelInstance,
                                     java.lang.String methodPrefix)

Overridden method to generate a type-level constraint check method. This method adds a method header and wraps the given constraint checking code (stmt) with code for inheriting assertions and to reporting an constraint violation.

Parameters:

terms - Nodes whose values are to be printed upon an assertion violation.

stmt - Code to evaluate the assertion under translation. The result is assumed to be stored in variable VN_ASSERTION. A null value means that no assertion is specified or the assertion is not executable.

result - RacResult associated with this type

inherit - Can this method inherit from super class/interface. Not all methods of history constraint contains code to support inherited or implemented constraints.

isTopLevelInstance - Whether the method that is currently being generated is a top-level instance history constraint method. This method has the following pattern: checkHC$instance$

methodPrefix - The prefix for the method name (0,S,W ...) for generation of of different methods for HC. When isEvaluation is true, methodPrefix denotes the method name of the method to be generated and the method name of the super class/interface.