TY - JOUR
T1 - Soundness of data refinement for a higher-order imperative language
AU - Naumann, David A.
PY - 2002/5/6
Y1 - 2002/5/6
N2 - 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.
AB - 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.
KW - Data refinement
KW - Formal semantics
KW - Predicate transformers
KW - Program correctness
KW - Programming Calculi
UR - http://www.scopus.com/inward/record.url?scp=0037029887&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0037029887&partnerID=8YFLogxK
U2 - 10.1016/S0304-3975(00)00339-X
DO - 10.1016/S0304-3975(00)00339-X
M3 - Article
AN - SCOPUS:0037029887
SN - 0304-3975
VL - 278
SP - 271
EP - 301
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 1-2
ER -