org.jmlspecs.jml4.rac
Class InvariantLikeMethod

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

Direct Known Subclasses:

ConstraintMethod, InvariantMethod

public abstract class InvariantLikeMethod
extends AssertionMethod

Generates assertion check methods for type assertions such as invariants and history constraints. There are two kinds of type assertions: instance (non-static) assertions and class (static) assertions. This class can generate both kinds of assertion check methods. An instance assertion check method checks both the instance and class assertions while a class assertion check method checks only the class assertions. The assertion check methods inherit assertions of its superclass and interfaces by dynamically invoking the corresponding assertion methods.

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

Author:

Yoonsik Cheon, Amritam Sarcar

See Also:

AssertionMethod

Method Summary

RacMethodDeclaration

generate(java.lang.StringBuffer stmt, java.util.Set<ASTNode> terms, RacResult result) Generates an type-level assertion check method.

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)

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

Specified by:

generate in class AssertionMethod

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 - TODO