A logic for the Russell programming language
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).
What people are saying - Write a review
We haven't found any reviews in the usual places.
abbreviate alias aliases allocation component allow application of f arbitrary arg ax argument array assignment assume assumption axiomatization binding BL++ formula block chapter compactness thm complete description consider define the meaning definition denotational semantics denote environment equivalent evaluation explicitly extended general applications extended meaning functions false follows formal func function construction function signature globally valid Hoare logic Hoare's holds identifier induction hypothesis inference rules integer introduce Is_allocated[x l-values letrec locations loop monotonicity thm NewIntQ NewT NewT[k NewTQ nonterminating notation notion operator parameter preceding predicate calculus prenex normal form programming language proof rules provable prove recursive declarations rename ax renaming thm replaced result Russell expression Russell subset Russell terms semantics semi-basic sequence side effect free simplify singleton set Soundness Proof statement subexpressions Theorem tion true Tvar[i undefined universally quantified val ax value axiom value component value produced variables XeXs