Correctness of recursive parallel nondeterministic flow programs
type: Item
instance of: scholarly article
title: Correctness of recursive parallel nondeterministic flow programs
zbMATH Open document ID: 0532.68019
DOI: 10.1016/0022-0000(83)90043-0
published in: Journal of Computer and System Sciences
publication date: 1983-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N25
zbMATH DE Number: 3845022
zbMATH Keywords: flow
zbMATH Keywords: parallel
zbMATH Keywords: correctness
zbMATH Keywords: nondeterministic
zbMATH Keywords: verification
zbMATH Keywords: program scheme
author: Joseph Goguen
author: José Meseguer
MaRDI profile type: Publication
full work available at URL: 0022-0000(83)90043-0
OpenAlex ID: W1993492813
cites work: Q4152697
cites work: Can programming be liberated from the von Neumann style?
cites work: Q5545978
cites work: Q4130967
cites work: Q4054648
cites work: Q4138103
cites work: Automata in general algebras
cites work: Q5636309
cites work: Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II
cites work: On homomorphisms, correctness, termination, unfoldments, and equivalence of flow diagram programs
cites work: Q4168048
cites work: Q4125728
cites work: Parallel realization of systems, using factorizations and quotients in categories
cites work: Topoi. The categorial analysis of logic
cites work: Q4178466
cites work: FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
cites work: Q5639839
cites work: Q4772698
cites work: The correctness of nondeterministic programs
cites work: Mathematical theory of partial correctness
description: scientific article; zbMATH DE number 3845022