org.jmlspecs.jml4.rac
Class PreconditionMethod

java.lang.Object
  org.jmlspecs.jml4.rac.AssertionMethod
      org.jmlspecs.jml4.rac.PrePostconditionMethod
          org.jmlspecs.jml4.rac.PreconditionMethod

public class PreconditionMethod
extends PrePostconditionMethod

Generates precondition check methods. Given precondition check code, this class wraps it with code that checks inherited preconditions from superclass and interfaces and throws a precondition violation error upon a violation of the precondition.

Author:

Yoonsik Cheon and Amritam Sarcar

See Also:

PrePostconditionMethod

Method Summary

MethodDeclaration	generate(java.lang.StringBuffer stmt, java.util.Collection<RacOldExpression> preExprs, java.util.Set<ASTNode> terms, RacResult result) Generates and returns a precondition checking method.
RacMethodDeclaration	generate(java.lang.StringBuffer stmt, java.util.Set<ASTNode> terms, RacResult result) Overridden here to throw an exception, as this method is not supported by this class.

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)

Overridden here to throw an exception, as this method is not supported by this class. Instead, the following method should be used for generating a precondition method.

Specified by:

generate in class AssertionMethod

Parameters:

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.

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

result - TODO

See Also:

generate(StringBuffer, Collection, Set, RacResult)

generate

public MethodDeclaration generate(java.lang.StringBuffer stmt,
                                  java.util.Collection<RacOldExpression> preExprs,
                                  java.util.Set<ASTNode> terms,
                                  RacResult result)

Generates and returns a precondition checking method. Append to the body (stmt) (1) code to check the inherited precondition if any, and (2) code to throw an appropriate exception to notify a violation if the precondition is violated.

Parameters:

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

preExprs - List of code for be executed in the pre-sate; this includes old variables and old expressions.

result - TODO