zbMATH — the first resource for mathematics

Heterogeneous development graphs and heterogeneous borrowing. (English) Zbl 1077.68609
Nielsen, Mogens (ed.) et al., Foundations of software science and computation structures. 5th international conference, FOSSACS 2002, held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43366-X). Lect. Notes Comput. Sci. 2303, 326-341 (2002).
Summary: 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.
For the entire collection see [Zbl 0989.00051].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: Link