org.jmlspecs.jml4.rac
Class ExceptionalPostconditionMethod

java.lang.Object
  org.jmlspecs.jml4.rac.AssertionMethod
      org.jmlspecs.jml4.rac.PrePostconditionMethod
          org.jmlspecs.jml4.rac.PostconditionMethod
              org.jmlspecs.jml4.rac.ExceptionalPostconditionMethod

public class ExceptionalPostconditionMethod
extends PostconditionMethod

Generate exceptional postcondition check methods. This class takes code that checks an exceptional postcondition of a method and wraps it with code that checks inherited exceptional postconditions and, if violated, throws an exceptional postcondition error.

Author:

Yoonsik Cheon and Amritam Sarcar

Constructor Summary

ExceptionalPostconditionMethod(JmlTypeDeclaration typeDecl, AbstractMethodDeclaration mdecl, java.lang.String restoreMethod)
Creates a new postconidition method generator for the given method of the given type.

Method Summary

MethodDeclaration

generate(java.lang.StringBuffer stmt, java.util.Set<ASTNode> terms, RacResult result) Returns an exceptional postcondition checking method.

Methods inherited from class java.lang.Object

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

Constructor Detail

ExceptionalPostconditionMethod

public ExceptionalPostconditionMethod(JmlTypeDeclaration typeDecl,
                                      AbstractMethodDeclaration mdecl,
                                      java.lang.String restoreMethod)

Creates a new postconidition method generator for the given method of the given type.

Parameters:

typeDecl - Type of which a RAC methodis to be generated

mdecl - Method for which a precondition method is to be generated

restoreMethod - Method to be used to restore pre-state values

Method Detail

generate

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

Returns an exceptional postcondition checking method. This method appends to the body, stmt, (1) code to check the inherited exceptional postconditions if any, and (2) code to throw an appropriate exception to notify a violation if the condition is violated at runtime.

Overrides:

generate in class PostconditionMethod

Parameters:

stmt - code to evaluate the exceptional postcondition; the result is supposed to be stored in the variable VN_ASSERTION. A null value means that no exceptional postcondition is specified or it is not executable.

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

result - TODO