Generalized Typestate Checking Using Set Interfaces and Pluggable Analyses

paper ps   
We present a generalization of standard typestate systems in which the typestate of each object is determined by its membership in a collection of abstract typestate sets. This generalization supports typestates that model participation in abstract data types, composite typestates that correspond to membership in multiple sets, and hierarchical typestates. Because membership in typestate sets corresponds directly to participation in data structures, our typestate system characterizes global sharing patterns. In our approach, each module encapsulates a data structure and uses membership in abstract sets to characterize how objects participate in its data structure. Each analysis verifies that the implementation of the module 1) preserves important internal data structure representation invariants and 2) conforms to a specification that uses formulas in a set algebra to characterize the effects of operations on the data structure. The analyses use the common set abstraction to 1) characterize how objects participate in multiple data structures and to 2) enable the inter-analysis communication required to verify properties that depend on multiple modules analyzed by different analyses.

Citation

Patrick Lam, Viktor Kuncak, and Martin Rinard. Generalized typestate checking using set interfaces and pluggable analyses. SIGPLAN Notices, 39:46--55, March 2004.

BibTex Entry

@article{LamETAL04GeneralizedTypestateCheckingUsingSets,
  author = {Patrick Lam and Viktor Kuncak and Martin Rinard},
  title = {Generalized Typestate Checking Using Set Interfaces and Pluggable Analyses},
  journal = {SIGPLAN Notices},
  year = 2004,
  volume = 39,
  issue = 3,
  month = {March},
  pages = {46--55},
  abstract = {
We present a generalization of standard typestate systems
in which the typestate of each object is determined
by its membership in a collection of abstract typestate
sets. This generalization supports typestates that model
participation in abstract data types, composite typestates
that correspond to membership in multiple sets, and 
hierarchical typestates. Because membership in typestate
sets corresponds directly to participation in data
structures, our typestate system characterizes
global sharing patterns. 

In our approach, each module
encapsulates a data structure and uses membership
in abstract sets to characterize how objects participate
in its data structure. Each analysis verifies
that the implementation of the module 1) preserves important
internal data structure representation invariants and
2) conforms to a specification that uses formulas in
a set algebra to characterize the effects of operations
on the data structure. The analyses use the common set
abstraction to 1) characterize how objects participate in
multiple data structures and to 2) enable the inter-analysis
communication required to verify properties that depend
on multiple modules analyzed by different analyses.
}
}