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

Fingerprint

Flow diagram
Correctness
Semantics
Relational Algebra
Computer programming languages
Algebra
Algebraic Theory
Programming Languages
Assignment
Diagram
Partial
Generalise
Model

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Goguen, J. A., & Meseguer, J. (1977). Correctness of recursive flow diagram programs. In J. Gruska (Ed.), Mathematical Foundations of Computer Science 1977 - Proceedings, 6th Symposium (pp. 580-595). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 53 LNCS). Springer-Verlag. https://doi.org/10.1007/3-540-08353-7_183

Correctness of recursive flow diagram programs. / Goguen, J. A.; Meseguer, J.

Mathematical Foundations of Computer Science 1977 - Proceedings, 6th Symposium. ed. / Jozef Gruska. Springer-Verlag, 1977. p. 580-595 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 53 LNCS).

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

Goguen, JA & Meseguer, J 1977, Correctness of recursive flow diagram programs. in J Gruska (ed.), Mathematical Foundations of Computer Science 1977 - Proceedings, 6th Symposium. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 53 LNCS, Springer-Verlag, pp. 580-595, 6th Symposium on Mathematical Foundations of Computer Science, MFCS 1977, Tatranska Lomnica, Slovakia, 9/5/77. https://doi.org/10.1007/3-540-08353-7_183
Goguen JA, Meseguer J. Correctness of recursive flow diagram programs. In Gruska J, editor, Mathematical Foundations of Computer Science 1977 - Proceedings, 6th Symposium. Springer-Verlag. 1977. p. 580-595. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-08353-7_183
Goguen, J. A. ; Meseguer, J. / Correctness of recursive flow diagram programs. Mathematical Foundations of Computer Science 1977 - Proceedings, 6th Symposium. editor / Jozef Gruska. Springer-Verlag, 1977. pp. 580-595 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{728208ebfcc54e4083e99d3e4b12083a,
title = "Correctness of recursive flow diagram programs",
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.",
author = "Goguen, {J. A.} and J. Meseguer",
year = "1977",
month = "1",
day = "1",
doi = "10.1007/3-540-08353-7_183",
language = "English (US)",
isbn = "9783540083535",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "580--595",
editor = "Jozef Gruska",
booktitle = "Mathematical Foundations of Computer Science 1977 - Proceedings, 6th Symposium",

}

TY - GEN

T1 - Correctness of recursive flow diagram programs

AU - Goguen, J. A.

AU - Meseguer, J.

PY - 1977/1/1

Y1 - 1977/1/1

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-Verlag

ER -