Lab for Automated Reasoning and Analysis 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

 
sav10/lecture_18.txt · Last modified: 2010/05/31 10:13 by vkuncak
 
© EPFL 2018 - Legal notice