Soundness of data refinement for a higher-order imperative language

Research output: Contribution to journalArticlepeer-review

11 Scopus citations

Abstract

Using a set-theoretic model of predicate transformers and ordered data types, we give a semantics for an Oberon-like higher-order imperative language with record subtyping and procedure-type variables and parameters. Data refinement is shown to be sound for this language: It implies algorithmic refinement when suitably localized. All constructs are shown to preserve simulation, so data refinement can be carried out piecewise.

Original languageEnglish
Pages (from-to)271-301
Number of pages31
JournalTheoretical Computer Science
Volume278
Issue number1-2
DOIs
StatePublished - 6 May 2002

Keywords

  • Data refinement
  • Formal semantics
  • Predicate transformers
  • Program correctness
  • Programming Calculi

Fingerprint

Dive into the research topics of 'Soundness of data refinement for a higher-order imperative language'. Together they form a unique fingerprint.

Cite this