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 -