A Logic for the Russell Programming LanguageWe 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). |
Contents
The Logical Framework | 41 |
An Axiomatization | 55 |
A Relative Completeness Proof | 97 |
2 other sections not shown
Common terms and phrases
abbreviate aliasing allocation component allows application of f arbitrary arg ax arguments array assignment assume axiomatic semantics axiomatization b₁ binding chapter compactness thm compl lemma completely determines conditional definition denotational semantics denote Dynamic Logic effect axiom environment equivalent evaluation explicitly extended general application extended meaning functions false fn subst ax fn val ax follows formal formula func signature function construction function signature globally valid Hoare logic Hoare's holds id ef ax identifier induction hypothesis inference rules Integer Is_allocated l-values loop monotonicity thm NewT NewT[k nonterminating constructs operator parameter predicate prenex normal form programming language proof rules provable prove quantifier free recursive declarations rename ax renaming thm replaced result rewrite Russell subset Russell terms semantics semi-basic sequence side effect free signature val simplify singleton Soundness Proof statement termination theorem tion true Tvar[i undefined universally quantified value produced variables