Interface EnsuresNode

All Superinterfaces:
ASTNode, ContractNode

public interface EnsuresNode extends ContractNode
An "ensures" clause in a procedure contract represents a post-condition.
  • Method Details

    • getExpression

      ExpressionNode getExpression()
      An expression of boolean type which is the post-condition
      Returns:
      the boolean expression post-condition
    • copy

      EnsuresNode copy()
      Description copied from interface: ASTNode
      Returns a deep copy of this AST node. The node and all of its descendants will be cloned. The cloning does not copy analysis or attribute information.
      Specified by:
      copy in interface ASTNode
      Specified by:
      copy in interface ContractNode
      Returns:
      deep copy of this node
    • isGuarantee

      boolean isGuarantee()
      Returns:
      true iff this ensures clause specifies a "guarantee", i.e. a set of absence assertions that is guaranteed to be satisfied by any execution of the function specified by this clause.
    • setIsGuarantee

      void setIsGuarantee(boolean isGuarantee)
      Parameters:
      isGuarantee - true to set this clause to be isGuarantee()