Deriving Properties of Systems from Properties of Parts and Lists of Connections
John R. Gabriel, Richard Chapman · 1986
This paper presents an algorithm in PROLOG for compiling recursively computable descriptions of system behavior from computable descriptions of behavior for parts and lists of interconnections. We give a set of conditions that must be satisfied by various data structures in the computation. It seems possible to provide an informal verification (by hand) that these conditions are true also of the output.