Correctness of recursive flow diagram programs

J. A. Goguen, J. Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationMathematical Foundations of Computer Science 1977 - Proceedings, 6th Symposium
EditorsJozef Gruska
Number of pages16
ISBN (Print)9783540083535
StatePublished - 1977
Externally publishedYes
Event6th Symposium on Mathematical Foundations of Computer Science, MFCS 1977 - Tatranska Lomnica, Slovakia
Duration: Sep 5 1977Sep 9 1977

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume53 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other6th Symposium on Mathematical Foundations of Computer Science, MFCS 1977
CityTatranska Lomnica

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Correctness of recursive flow diagram programs'. Together they form a unique fingerprint.

Cite this