org.jmlspecs.jml4.rac
Class PostconditionMethod

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

Direct Known Subclasses:

ExceptionalPostconditionMethod

public class PostconditionMethod
extends PrePostconditionMethod

A class for generating postcondition check methods. The postcondition check code is wrapped with code to check the inherited postconditions if any, and to throw an appropriate exception to signal a violation if the postcondition is violated at runtime.

The class implements a variant of the Template Pattern [GoF95], prescribed in the class AssertionMethod.

Author:

Yoonsik Cheon and Amritam Sarcar

See Also:

AssertionMethod

Constructor Summary

PostconditionMethod(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) Generate and return a postcondition checking method.

Methods inherited from class java.lang.Object

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

Constructor Detail

PostconditionMethod

public PostconditionMethod(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)

Generate and return a postcondition checking method. Append to the body (stmt) (1) code to check the inherited postcondition if any, and (2) code to throw an appropriate exception to notify a violation if the postcondition is violated at runtime.

Specified by:

generate in class AssertionMethod

Parameters:

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

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

result - TODO