Formal specifications are increasingly used in modeling software systems. An important aspect of a model is its value as an analytical tool to investigate the effect of changes. This paper defines the notion of predicate differences and shows how predicate differences may be used to analyze the... See full abstract

Formal specifications are increasingly used in modeling software systems. An important aspect of a model is its value as an analytical tool to investigate the effect of changes. This paper defines the notion of predicate differences and shows how predicate differences may be used to analyze the effects of changes in formal specifications. Predicate differences have both theoretical and practical applications. As a theoretical tool, predicate differences may be used to define a meaning for the ‘size” of a change to a formal specification. Practical applications include analyzing the effect of design changes on a previously verified design; defining an affinity function for reusable software components; computing slices of formal specifications, similar to program slices; investigating the conditions under which invalid assumptions will render a system non-secure; and formalizing the database inference problem.
Hide full abstract