Inspector Methods for State Abstraction
By: Bart Jacobs, Frank Piessens
Abstract
This paper proposes an approach, based on the Boogie methodology, to the verification of programs that use inspector methods in method contracts and object invariants, to support state abstraction in specifications. However, performing state abstraction in a programming language that allows aliasing through object references poses a framing problem, which is solved thanks to a novel logical encoding of the heap, without breaking information hiding.
Cite as:
Bart Jacobs, Frank Piessens, “Inspector Methods for State Abstraction”, Journal of Object Technology, Volume 6, no. 5 (June 2007), pp. 55-75, doi:10.5381/jot.2007.6.5.a1.
PDF | HTML | DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn