A logic for the Russell programming language

Front Cover
Cornell University, Jan., 1984 - Mathematics - 310 pages
0 Reviews
We consider a programming language with a number of characteristics detrimental to conventional axiomatic descriptions. These include arbitrary side effects in expressions, aliasing among variables, very general recursive function declarations, and the ability to pass functions as parameters and return them as results. We give an axiomatic definition of this language based on a novel formalism. We prove the axiomatization sound and relatively complete with respect to a (somewhat nonstandard) denotational semantics. In spite of the nonstandard formalism, most conventional techniques for developing and reasoning about programs can be carried over. (ABRIDGED).

From inside the book

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

adef
12
e compactness thm
13
s monotonicity thm
16

20 other sections not shown

Common terms and phrases

Bibliographic information