Universität Bremen  
  FB 3  
  Group BKB > Publications > Search > Deutsch
English
 

Publications Search - Details

 
Publication type: Article
Author: T. Mossakowski, S. Autexier, D. Hutter
Title: Development Graphs -- Proof Management for Structured Specifications
Volume: 67
Page(s): 114 – 145
Journal: Journal of Logic and Algebraic Programming
Number: 1-2
Year published: 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.
ISSN: 1567-8326
Internet: http://www.sciencedirect.com/science?_ob=GatewayURL&_origin=CONTENTS&_method=citationSearch&_piikey=S1567832605000810&_version=1&md5=7c18897e9ffad42e0649c6b41203f41e
PostScript Version: http://www.informatik.uni-bremen.de/~till/papers/dgh_journal.ps
Keywords: development graph proof logic institution completeness
Status: Reviewed
Last updated: 09. 03. 2006

 Back to result list
 
   
Author: Automatically generated page
 
  Group BKB 
Last updated: May 9, 2023   impressum