Loading...
Please wait, while we are loading the content...
Verifying programs using inspector methods for state abstraction
| Content Provider | Semantic Scholar |
|---|---|
| Author | Jacobs, Bart Piessens, Frank |
| Copyright Year | 2005 |
| Abstract | Most classes in an object-oriented program provide access to an object's state through methods, so that client code does not depend on and cannot interfere with the object's internal representation composed of fields and internal component objects. Methods used for this purpose are sometimes called inspector methods. In order to extend the benefits of inspector methods to specifications, the method contracts of non-inspector methods may be expressed using inspector methods. In this paper, we propose an approach to the verification of programs that use inspector methods in method contracts and object invariants. Performing state abstraction in a programming language that allows aliasing through object references poses a framing problem. Our solution to this framing problem is a formulation of the Boogie methodology in terms of read bags and write sets which, combined with the Boogie methodology's ownership system, abstractly capture a method's effects. We show how programs that are specified using inspector methods can be translated into the input language of the Boogie |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.kuleuven.ac.be/publicaties/rapporten/cw/CW432.pdf |
| Alternate Webpage(s) | http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW432.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
