Correctness of recursive parallel nondeterministic flow programs

J. A. Goguen, J. Meseguer

Research output: Contribution to journalArticle

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 languageEnglish (US)
Pages (from-to)268-290
Number of pages23
JournalJournal of Computer and System Sciences
Volume27
Issue number2
DOIs
StatePublished - Oct 1983
Externally publishedYes

ASJC Scopus subject areas

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

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

  • Cite this