This document is available by FTP in various formats. It was converted to HTML using Hyperlatex 2.5.
Development graphs are a tool for dealing with structured specifications in a way easing management of change and reusing proofs. In this work, we extend development graphs with hiding. 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 absolute complete set of rules cannot exist. The whole framework is developed in a way independent of the underlying logical system.
The rest of this document has not yet been converted to HTML; please refer to the FTP directory for the full document.