This paper presents a simple algebraic description of the semantics of non-deterministic recursive flow diagram programs with parallel assignment, culminating in a method for proving their partial correctness which generalizes the well-known Floyd-Naur method for ordinary flow diagram programs. Our treatment involves first considering a program scheme, and then interpreting it in an appropriate semantic model. The program schemes are conveniently viewed as diagrams in an algebraic theory, with semantic model a relational algebra. Some examples are given in a simple programming language whose features correspond precisely to our algebraic framework.
CITATION STYLE
Goguen, J. A., & Meseguer, J. (1977). Correctness of recursive flow diagram programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 53 LNCS, pp. 580–595). Springer Verlag. https://doi.org/10.1007/3-540-08353-7_183
Mendeley helps you to discover research relevant for your work.