Module dev.civl.mc
Package dev.civl.mc.model.IF.contract

Interface LoopContract

All Superinterfaces:
Sourceable
public interface LoopContract extends Sourceable
This class represents a group of loop annotations for a loop, including loop invariants, loop assigns and loop variants.

  • Method Details

    • loopLocation

      Location loopLocation()
      Returns the location which identifies the corresponding loop.
      Returns:
      the location which identifies the corresponding loop.

    • loopInvariants

      Expression[] loopInvariants()
      Returns an array of loop invariants specified for this loop.
      Returns:
      An array of expression whose type must be bool; Empty array if no loop invariants specified.

    • loopAssigns

      LHSExpression[] loopAssigns()
      Returns an array of loop assigns specified for this loop.
      Returns:
      An array of left-hand side expressions;Empty array if no loop assigns specified.

    • loopVariants

      Expression[] loopVariants()
      Returns an array of loop variants specified for this loop.
      Returns:
      An array of loop variants; Empty array if no loop variants specified.

    • setLocation

      void setLocation(Location loopLocation)
      Set the location which identifies a loop statement.
      Parameters:
      loopLocation -