Class ClassInvariantGenerator


  • public class ClassInvariantGenerator
    extends BaseGenerator

    Code generator for class invariants.

    • Constructor Detail

      • ClassInvariantGenerator

        public ClassInvariantGenerator​(ReaderSource source)
    • Method Detail

      • generateInvariantAssertionStatement

        public void generateInvariantAssertionStatement​(ClassNode type,
                                                        ClassInvariant classInvariant)
        Reads the Invariant boolean expression and generates a synthetic method holding this class invariant. This is used for heir calls to find out about inherited class invariants.
        Parameters:
        type - the current ClassNode
        classInvariant - the ClassInvariant the assertion statement should be generated from
      • addInvariantAssertionStatement

        public void addInvariantAssertionStatement​(ClassNode type,
                                                   MethodNode method)
        Adds the current class-invariant to the given method.
        Parameters:
        type - the ClassNode which declared the given MethodNode
        method - the current MethodNode