Compositionality and Concurrent Networks: Soundness and Completeness of a Proofsystem

Specification, construction and verification of programs should be done in a compositional way. This means that for each syntactic programming construct it should be possible to infer a specification for the whole construct from specifications of the constituent syntactic components of that construct. A compositional proofsystem is presented for a language that includes parallel executing networks and recursive creation of subnetworks. This system is then shown to be arithmetically complete.