Programs as partial graphs I: Flow equivalence and correctness

AbstractA common feature of most theoretical investigations on semantics, correctness and termination is the strict distinction between the descriptional tool used for the flow of program control and the completely different tool describing single program steps. Since these different methods are difficult to handle when it is necessary that they be used together this paper presents a unified approach to the presentation of these concepts in terms of Tarski's and Riguet's relational algebra. Partial graphs and programs are introduced to formally manipulate relational notions of semantics, correctness and termination. The second part of this paper will extend these notions to systems of recursive programs