Set Interfaces for Generalized Typestate and Data Structure Consistency Verification
Typestate systems allow the type of an object to change during its lifetime in the computation. Unlike standard type systems, they can enforce safety properties that depend on changing object states. We present a new, generalized formulation of typestate that models the typestate of an object throug...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Published: |
2007
|
| Online Access: | http://hdl.handle.net/1721.1/39419 |
| _version_ | 1826209554847760384 |
|---|---|
| author | Lam, Patrick Zee, Karen Kuncak, Viktor Rinard, Martin |
| author2 | Martin Rinard |
| author_facet | Martin Rinard Lam, Patrick Zee, Karen Kuncak, Viktor Rinard, Martin |
| author_sort | Lam, Patrick |
| collection | MIT |
| description | Typestate systems allow the type of an object to change during its lifetime in the computation. Unlike standard type systems, they can enforce safety properties that depend on changing object states. We present a new, generalized formulation of typestate that models the typestate of an object through membership in abstract sets. This abstract set formulation enables developers to reason about cardinalities of sets, and in particular to state and verify the condition that certain sets are empty. We support hierarchical typestate classifications by specifying subset and disjointness properties over the typestate sets.We present our formulation of typestate in the context of the Hob program specification and verification framework. The Hob framework allows the combination of typestate analysis with powerful independently developed analyses such as shape analyses or theorem proving techniques. We implemented our analysis and annotated several programs (75-2500 lines of code) with set specifications. Our implementation includes several optimizations that improve the scalability of the analysis and a novel loop invariant inferencealgorithm that eliminates the need to specify loop invariants. We present experimental data demonstrating the effectiveness of our techniques. |
| first_indexed | 2024-09-23T14:24:22Z |
| id | mit-1721.1/39419 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T14:24:22Z |
| publishDate | 2007 |
| record_format | dspace |
| spelling | mit-1721.1/394192019-04-12T09:30:42Z Set Interfaces for Generalized Typestate and Data Structure Consistency Verification Lam, Patrick Zee, Karen Kuncak, Viktor Rinard, Martin Martin Rinard Computer Architecture Typestate systems allow the type of an object to change during its lifetime in the computation. Unlike standard type systems, they can enforce safety properties that depend on changing object states. We present a new, generalized formulation of typestate that models the typestate of an object through membership in abstract sets. This abstract set formulation enables developers to reason about cardinalities of sets, and in particular to state and verify the condition that certain sets are empty. We support hierarchical typestate classifications by specifying subset and disjointness properties over the typestate sets.We present our formulation of typestate in the context of the Hob program specification and verification framework. The Hob framework allows the combination of typestate analysis with powerful independently developed analyses such as shape analyses or theorem proving techniques. We implemented our analysis and annotated several programs (75-2500 lines of code) with set specifications. Our implementation includes several optimizations that improve the scalability of the analysis and a novel loop invariant inferencealgorithm that eliminates the need to specify loop invariants. We present experimental data demonstrating the effectiveness of our techniques. 2007-11-02T18:45:31Z 2007-11-02T18:45:31Z 2007-10-31 MIT-CSAIL-TR-2007-049 http://hdl.handle.net/1721.1/39419 Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 30 p. application/pdf application/postscript |
| spellingShingle | Lam, Patrick Zee, Karen Kuncak, Viktor Rinard, Martin Set Interfaces for Generalized Typestate and Data Structure Consistency Verification |
| title | Set Interfaces for Generalized Typestate and Data Structure Consistency Verification |
| title_full | Set Interfaces for Generalized Typestate and Data Structure Consistency Verification |
| title_fullStr | Set Interfaces for Generalized Typestate and Data Structure Consistency Verification |
| title_full_unstemmed | Set Interfaces for Generalized Typestate and Data Structure Consistency Verification |
| title_short | Set Interfaces for Generalized Typestate and Data Structure Consistency Verification |
| title_sort | set interfaces for generalized typestate and data structure consistency verification |
| url | http://hdl.handle.net/1721.1/39419 |
| work_keys_str_mv | AT lampatrick setinterfacesforgeneralizedtypestateanddatastructureconsistencyverification AT zeekaren setinterfacesforgeneralizedtypestateanddatastructureconsistencyverification AT kuncakviktor setinterfacesforgeneralizedtypestateanddatastructureconsistencyverification AT rinardmartin setinterfacesforgeneralizedtypestateanddatastructureconsistencyverification |