org.jmlspecs.jml4.rac
Class InvariantMethod

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

public class InvariantMethod
extends InvariantLikeMethod

Generates assertion check methods for invariants. There are two types of invariants: instance (non-static) invariants and class (static) invariants. This class can generates both types of invariant check methods. An instance invariant method checks both the instance and class invariants while a class invariant method checks only the class invariants. The generated invariant methods inherit invariants of its superclass 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

See Also:

AssertionMethod

Method Summary

Methods inherited from class org.jmlspecs.jml4.rac.InvariantLikeMethod

generate

Methods inherited from class java.lang.Object

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