TY - JOUR
T1 - Predicate transformer semantics of a higher-order imperative language with record subtyping
AU - Naumann, David A.
PY - 2001/9
Y1 - 2001/9
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0035452474&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0035452474&partnerID=8YFLogxK
U2 - 10.1016/S0167-6423(00)00005-8
DO - 10.1016/S0167-6423(00)00005-8
M3 - Article
AN - SCOPUS:0035452474
SN - 0167-6423
VL - 41
SP - 1
EP - 51
JO - Science of Computer Programming
JF - Science of Computer Programming
IS - 1
ER -