org.jmlspecs.jml4.rac
Class AssertionMethod

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

Direct Known Subclasses:

InvariantLikeMethod, PrePostconditionMethod

public abstract class AssertionMethod
extends java.lang.Object

An abstract class to generate assertion check methods for various kinds of assertions such as preconditions, normal and exceptional postconditions, invariants, and history constraints. An assertion check method inherits the assertions of its superclass and interfaces by dynamically invoking their corresponding assertion check methods. For example, if a method m is overriding an inherited method, its precondition check method invokes dynamically m's precondition method defined in the overridden superclass. In general, the following rules govern the inheritance of assertions.

• Method specifications such as preconditions and postconditions are inherited by subclasses. However, assertions are inherited only for for instance (non-static) methods; class (static) method specifications are not inherited by subclasses. Constructor specifications are not inherited by subclasses.

• Both static and non-static invariants are inherited by subclasses.

• Both static and non-static constraints are inherited by subclasses. However, the inheritance of constraints is subjected to the strong and weak behavioral subtyping, specified by the weakly annotation in the extends clause. This feature is not implemented yet.

All inheritances are subjected to the accessibility; only public and protected assertions are inherited. This is not implemented yet.

The class is implemented using the Template Pattern [GoF95]. The abstract method generate is supposed to call the methods Header and checker, respectively, to compose the header and the body of the assertion method under construction. The method checker calls the query method canInherit to decide whether to generate code for inheriting specifications. The actual code for inheritance is generated by calling the method inheritAssertion.

  generate {abstract}
    methodHeader
    checker
      canInherit {abstract}
      inheritAssertion {abstract}
 

Author:

Yoonsik Cheon and Amritam Sarcar

Method Summary

abstract AbstractMethodDeclaration

generate(java.lang.StringBuffer code, java.util.Set<ASTNode> terms, RacResult racResult) Generates an assertion check method.

Methods inherited from class java.lang.Object

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

Method Detail

generate

public abstract AbstractMethodDeclaration generate(java.lang.StringBuffer code,
                                                   java.util.Set<ASTNode> terms,
                                                   RacResult racResult)

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

Parameters:

code - 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.

racResult - TODO