Loading...
Please wait, while we are loading the content...
Similar Documents
Verifying event-driven programs using ramified frame properties
| Content Provider | ACM Digital Library |
|---|---|
| Author | Krishnaswami, Neel R. Birkedal, Lars Aldrich, Jonathan |
| Abstract | Interactive programs, such as GUIs or spreadsheets, often maintain dependency information over dynamically-created networks of objects. That is, each imperative object tracks not only the objects its own invariant depends on, but also all of the objects which depend upon it, in order to notify them when it changes. These bidirectional linkages pose a serious challenge to verification, because their correctness relies upon a global invariant over the object graph. We show how to modularly verify programs written using dynamically-generated bidirectional dependency information. The critical idea is to distinguish between the footprint of a command, and the state whose invariants depends upon the footprint. To do so, we define an application-specific semantics of updates, and introduce the concept of a ramification operator to explain how local changes can alter our knowledge of the rest of the heap. We illustrate the applicability of this style of proof with a case study from functional reactive programming, and formally justify reasoning about an extremely imperative implementation as if it were pure. |
| Starting Page | 63 |
| Ending Page | 76 |
| Page Count | 14 |
| File Format | |
| ISBN | 9781605588919 |
| DOI | 10.1145/1708016.1708025 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2010-01-23 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Subject-observer Separation logic Functional reactive programming Frame rule Ramification problem Dataflow |
| Content Type | Text |
| Resource Type | Article |
