Class Invariant


  • public class Invariant
    extends ConditionType
    An Invariant is an condition which should always hold when its preconditions are satisfied.
    • Constructor Detail

      • Invariant

        public Invariant​(String description,
                         Condition invariantCondition)
        Parameters:
        description - Description of the invariant.
        invariantCondition - Condition to check.
      • Invariant

        public Invariant​(String description,
                         Condition invariantCondition,
                         Condition... preConditions)
        Parameters:
        description - Description of the invariant.
        invariantCondition - Condition to check.
        preConditions - Only check if the preconditions are true.
      • Invariant

        public Invariant​(String description,
                         Condition invariantCondition,
                         List<Condition> preConditions)
        Parameters:
        description - Description of the invariant.
        invariantCondition - Condition to check.
        preConditions - Only check if the preconditions are true.