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

State | Published - Oct 1983 |

Externally published | Yes |

## ASJC Scopus subject areas

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