A micromodularity mechanism. - Jackson, Daniel
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.
Keywords: Software; Software engineering; Requirements / Specifications; Languages; Z; Theory of computation; Mathematical logic and formal languages; Mathematical logic; Design; Documentation; Languages; Verification; Alloy language; Z Specification language; First order logic; Formal specification; Modeling languages; Relational calculus; Schema calculus