LARA

Lecture 18: Reasoning about Specified Procedures

Specification Variables

Specification Variables with Definitions: ListReverse.java

Ghost Specification Variables: CursorList.java

  • variables that are under user
  • public and private invariants
  • specifying simple iterators

Modeling Cycles: CircularList.java

(Implicit) Dynamic Frames

  • Hiding Reusable Objects (not Just Fields or inner classes) by using Variables in Modifies Clauses

Doing Proofs Using Specification Variables: PriorityQueueAnnot.java

Continued in Lecture 19