TY - GEN

T1 - Correctness of recursive flow diagram programs

AU - Goguen, J. A.

AU - Meseguer, J.

N1 - Funding Information:
The content is a simple algebraic semantics for non-deterministic recursive flow diagram programs with parallel assignment, culminating in a method for proving their correctness which generalizes the so-called Floyd method for proving ordinary flow diagrams, as reformulated by Burstall (1972) and Goguen (1974), in which a non-deterministic (non-recursive) flow diagram program is a graph, whose nodes are labelled with sets, and whose edges are labelled with relations, such that if e:n~' is an edge from n to n ~, and if the labels of e, n, n ~ are f, S, S' respectively, then f is a function P(S) ÷P(S'), where P(A) is the set of all subsets of A, that is, the powerset of A. The nodes correspond to the "states of control" of the program, while an element of the label of a node is an "environment," for the computation (e.g., a memory state). The edges correspond to transitions of control, and are labelled *supported in part by the U.S. National Science Foundation, Grant No. tpartlally suppQrted by a Marab Foundation Research Fellowship.
Publisher Copyright:
© 1977, Springer-Verlag.
Copyright:
Copyright 2017 Elsevier B.V., All rights reserved.

PY - 1977

Y1 - 1977

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85035065771&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85035065771&partnerID=8YFLogxK

U2 - 10.1007/3-540-08353-7_183

DO - 10.1007/3-540-08353-7_183

M3 - Conference contribution

AN - SCOPUS:85035065771

SN - 9783540083535

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 580

EP - 595

BT - Mathematical Foundations of Computer Science 1977 - Proceedings, 6th Symposium

A2 - Gruska, Jozef

PB - Springer

T2 - 6th Symposium on Mathematical Foundations of Computer Science, MFCS 1977

Y2 - 5 September 1977 through 9 September 1977

ER -