Predicate transformer semantics of a higher-order imperative language with record subtyping

Research output: Contribution to journalArticlepeer-review

22 Scopus citations

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.

Original languageEnglish
Pages (from-to)1-51
Number of pages51
JournalScience of Computer Programming
Volume41
Issue number1
DOIs
StatePublished - Sep 2001

Fingerprint

Dive into the research topics of 'Predicate transformer semantics of a higher-order imperative language with record subtyping'. Together they form a unique fingerprint.

Cite this