A micromodularity mechanism

Daniel Jackson, Ilya Shlyakhter, Manu Sridharan

Abstract

A simple mechanism for structuring specifications is described. By modelling structures as atoms, it remains entirely first-order and thus amenable to automatic analysis. And by interpreting fields of structures as relations, it allows the same relational operators used in the formula language to be used for dereferencing. An extension feature allows structures to be developed incrementally, but requires no textual inclusion nor any notion of subtyping. The paper demonstrates the flexibility of the mechanism by application in a variety of common idioms.

BibTeX

@inproceedings{Jackson-al:FSE01,
  author    = {Daniel Jackson and
               Ilya Shlyakhter and
               Manu Sridharan},
  title     = {A micromodularity mechanism},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {62--73},
  publisher = {{ACM}},
  year      = {2001},
}

A micromodularity mechanism

Abstract

Related papers