Predicate transformer semantics of a higher-order imperative language withrecord subtyping

Using a set-theoretic model of predicate transformers and ordered data type s, we give a total-correctness semantics for a typed higher-order imperativ e 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 sema ntic complications of Algol-like languages. The semantics is used to valida te simple proof rules for non-interference, type extension, and calls of pr ocedure variables and constants. (C) 2001 Elsevier Science B.V. All rights reserved.