Publication
Development Graphs -- Proof Management for Structured Specifications
Till Mossakowski; Serge Autexier; Dieter Hutter
In: Journal of Logic and Algebraic Programming (JLAP), Vol. 67, No. 1--2, Pages 114-145, 2006.
Abstract
Development graphs are a tool for dealing with structured
specifications in a formal program development in order to ease the
management of change and reusing proofs. In this work, we extend
development graphs with hiding (e.g. hidden operations). Hiding is
a particularly difficult to realize operation, since it does not
admit such a good decomposition of the involved specifications as
other structuring operations do. We develop both a semantics and
proof rules for development graphs with hiding. The rules are proven
to be sound, and also complete relative to an oracle for
conservative extensions. We also show that an absolutely complete set
of rules cannot exist.
The whole framework is developed in a way independent of the
underlying logical system (and thus also does not prescribe the
nature of the parts of a specification that may be hidden). We also
show how various other logic independent specification formalisms
can be mapped into development graphs; thus, development graphs can
serve as a kernel formalism for management of proofs and of change.