Heterogeneous development graphs and heterogeneous borrowing

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. Often, different aspects of a software system have to be specified in different logics, since the construction of a huge logic covering all needed features would be too complex to be feasible. Therefore, we introduce heterogeneous development graphs as a means to cope with heterogeneous specifications. We cover both the semantics and the proof theory of heterogeneous development graphs. A proof calculus can be obtained either by combining proof calculi for the individual logics, or by representing these in some “universal” logic like higher-order logic in a coherent way and then “borrowing” its calculus for the heterogeneous language.