In this thesis, we undertake a study of imperative reasoning . Beginning with a philosophical analysis of the distinction between imperative and functional language features, we define a (pure) imperative language as one whose constructs are inherently referentially opaque. We then give a definition of a reasoning language by identifying desirable properties such a language should have.;AC consists of only four basic constructs, assignment 'X := t', sequence 't; u', procedure formation '¡t' and procedure invocation,! t'. Three interpretations are given for AC: an operational semantics, a denotational semantics, and a term-rewriting system. The three are shown to be equivalent. Running examples are used to illustrate each of the interpretations.;Five variants of AC are then studied. By removing restrictions from AC's syntactic and denotational definitions, we can incorporate L-values, lazy evaluation, state backtracking, and procedure composition into AC. By incorporating procedure composition, we show that AC becomes a self-contained Turing complete language in the same way as the untyped lambda-calculus: by encoding numerals, Booleans, and control structures as AC terms. Finally we look at the combination of AC with a typed lambda-calculus.;The rest of the thesis presents a new pure imperative reasoning language, Assignment Calculus AC. The main idea behind AC is that R. Montague's modal operators of intension and extension are useful tools for modeling procedures in programming languages. This line of thought builds on T. Janssen's demonstration that Montague's intensional logic is well suited to dealing with assignment statements, pointers, and other difficult features of imperative languages.
展开▼
