Abstract :
Using a set-theoretic model of predicate transformers and ordered data types, we give a total-correctness semantics for a typed higher-order imperative programming language that includes record extension, local variables, and procedure-type variables and parameters. The language includes infeasible specification constructs, for a calculus of refinement. Procedures may have global variables, subject to mild syntactic restrictions to avoid the semantic complications of Algol-like languages. The semantics is used to validate simple proof rules for non-interference, type extension, and calls of procedure variables and constants.
