Correctness of recursive parallel nondeterministic flow programs

J. A. Goguen; J. Meseguer

doi:10.1016/0022-0000(83)90043-0

Correctness of recursive parallel nondeterministic flow programs

Research output: Contribution to journal › Article › peer-review

Abstract

This paper presents a method for proving the partial correctness of programs with the following features: strongly typed expressions with call-by-value semantics for variables; iteration; recursive procedures with call-by-name semantics; nondeterminism; parallel assignment; and good old fashioned go-to's. An operational semantics is given to a program by viewing it as a program scheme together with an appropriate interpretation in a given model. Program schemes are viewed as diagrams in an algebraic theory, and the given models are relational algebras of this theory. A simple programming language, REPNOD, that embodies exactly the features that are discussed theoretically is defined, and several simple REPNOD programs, as well as a sample correctness proof, are given. This approach seems to provide a particularly simple framework for many problems in concurrent programming.

Original language	English (US)
Pages (from-to)	268-290
Number of pages	23
Journal	Journal of Computer and System Sciences
Volume	27
Issue number	2
DOIs	https://doi.org/10.1016/0022-0000(83)90043-0
State	Published - Oct 1983
Externally published	Yes

ASJC Scopus subject areas

Theoretical Computer Science
Computer Networks and Communications
Computational Theory and Mathematics
Applied Mathematics

Online availability

10.1016/0022-0000(83)90043-0

Library availability

Discover UIUC Full Text

Cite this

@article{8154f84406044365b94dd7bb5991ea48,

title = "Correctness of recursive parallel nondeterministic flow programs",

abstract = "This paper presents a method for proving the partial correctness of programs with the following features: strongly typed expressions with call-by-value semantics for variables; iteration; recursive procedures with call-by-name semantics; nondeterminism; parallel assignment; and good old fashioned go-to's. An operational semantics is given to a program by viewing it as a program scheme together with an appropriate interpretation in a given model. Program schemes are viewed as diagrams in an algebraic theory, and the given models are relational algebras of this theory. A simple programming language, REPNOD, that embodies exactly the features that are discussed theoretically is defined, and several simple REPNOD programs, as well as a sample correctness proof, are given. This approach seems to provide a particularly simple framework for many problems in concurrent programming.",

author = "Goguen, {J. A.} and J. Meseguer",

note = "Funding Information: * Research supported in part Office of Naval Research contracts NOOO14-80-0296 and NOOO14-82-C 0333, and National Science Foundation Grant MCS8201380.",

year = "1983",

month = oct,

doi = "10.1016/0022-0000(83)90043-0",

language = "English (US)",

volume = "27",

pages = "268--290",

journal = "Journal of Computer and System Sciences",

issn = "0022-0000",

publisher = "Academic Press Inc.",

number = "2",

}

TY - JOUR

T1 - Correctness of recursive parallel nondeterministic flow programs

AU - Goguen, J. A.

AU - Meseguer, J.

N1 - Funding Information: * Research supported in part Office of Naval Research contracts NOOO14-80-0296 and NOOO14-82-C 0333, and National Science Foundation Grant MCS8201380.

PY - 1983/10

Y1 - 1983/10

N2 - This paper presents a method for proving the partial correctness of programs with the following features: strongly typed expressions with call-by-value semantics for variables; iteration; recursive procedures with call-by-name semantics; nondeterminism; parallel assignment; and good old fashioned go-to's. An operational semantics is given to a program by viewing it as a program scheme together with an appropriate interpretation in a given model. Program schemes are viewed as diagrams in an algebraic theory, and the given models are relational algebras of this theory. A simple programming language, REPNOD, that embodies exactly the features that are discussed theoretically is defined, and several simple REPNOD programs, as well as a sample correctness proof, are given. This approach seems to provide a particularly simple framework for many problems in concurrent programming.

AB - This paper presents a method for proving the partial correctness of programs with the following features: strongly typed expressions with call-by-value semantics for variables; iteration; recursive procedures with call-by-name semantics; nondeterminism; parallel assignment; and good old fashioned go-to's. An operational semantics is given to a program by viewing it as a program scheme together with an appropriate interpretation in a given model. Program schemes are viewed as diagrams in an algebraic theory, and the given models are relational algebras of this theory. A simple programming language, REPNOD, that embodies exactly the features that are discussed theoretically is defined, and several simple REPNOD programs, as well as a sample correctness proof, are given. This approach seems to provide a particularly simple framework for many problems in concurrent programming.

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

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

U2 - 10.1016/0022-0000(83)90043-0

DO - 10.1016/0022-0000(83)90043-0

M3 - Article

AN - SCOPUS:0020828766

SN - 0022-0000

VL - 27

SP - 268

EP - 290

JO - Journal of Computer and System Sciences

JF - Journal of Computer and System Sciences

IS - 2

ER -

Correctness of recursive parallel nondeterministic flow programs

Abstract

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this