Model Programs for Preserving Composite Invariants

By: Steve M. Shaner, Hridesh Rajan, and Gary T. Leavens

Abstract

We describe a solution for the SAVCBS challenge problem: a technique for specifying and verifying invariants for objects designed using the Composite design pattern. The solution presents a grey-box speciﬁcation technique using JML’s model program feature. We show that model program speciﬁcations function as exemplars for capturing helper method calls in a way that preserves modularity and encapsulation.

ACM Reference

Shaner, S.M. et al. 2008. Model Programs for Preserving Composite Invariants. Seventh International Workshop on Specification and Verification of Component-Based Systems (SAVCBS) (2008), 95–100.

BibTeX Reference

@inproceedings{ShanerRajanLeavens2008,
  title = {Model Programs for Preserving Composite Invariants},
  author = {Shaner, Steve M and Rajan, Hridesh and Leavens, Gary T},
  booktitle = {Seventh International Workshop on Specification and Verification of Component-Based Systems (SAVCBS)},
  pages = {95-100},
  year = {2008},
  numpages = {6},
  institution = {Iowa State U., U. of Central Fl.},
  entrysubtype = {workshop},
  abstract = {
    We describe a solution for the SAVCBS challenge problem: a technique for
    specifying and verifying invariants for objects designed using the Composite
    design pattern. The solution presents a grey-box speciﬁcation technique using
    JML’s model program feature. We show that model program speciﬁcations function
    as exemplars for capturing helper method calls in a way that preserves
    modularity and encapsulation.
  }
}