Correctness of recursive flow diagram programs

J. A. Goguen, J. Meseguer

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

Abstract

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
PublisherSpringer-Verlag Berlin Heidelberg
Pages580-595
Number of pages16
ISBN (Print)9783540083535
DOIs
StatePublished - Jan 1 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

Other

Other6th Symposium on Mathematical Foundations of Computer Science, MFCS 1977
CountrySlovakia
CityTatranska Lomnica
Period9/5/779/9/77

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

Cite this