TY - GEN
T1 - Forward simulation for data refinement of classes
AU - Cavalcanti, Ana
AU - Naumann, David A.
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2002.
PY - 2002
Y1 - 2002
N2 - Simulation is the most widely used technique to prove data refinement. We define forward simulation for a language with recursive classes, inheritance, type casts and tests, dynamic binding, class based visibility, mutable state (without aliasing), and specification constructs from refinement calculi. It is a language based on sequential Java, but it also includes specification and deseign mechanisms appropriate for the construction of programs based on refinement. We show simulation to be sound for data refinement of classes in this language.
AB - Simulation is the most widely used technique to prove data refinement. We define forward simulation for a language with recursive classes, inheritance, type casts and tests, dynamic binding, class based visibility, mutable state (without aliasing), and specification constructs from refinement calculi. It is a language based on sequential Java, but it also includes specification and deseign mechanisms appropriate for the construction of programs based on refinement. We show simulation to be sound for data refinement of classes in this language.
KW - Data refinement
KW - Object-orientation
KW - Program analysis and verification
KW - Soundness of simulation
UR - http://www.scopus.com/inward/record.url?scp=84937396698&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84937396698&partnerID=8YFLogxK
U2 - 10.1007/3-540-45614-7_27
DO - 10.1007/3-540-45614-7_27
M3 - Conference contribution
AN - SCOPUS:84937396698
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 471
EP - 490
BT - FME 2002
A2 - Eriksson, Lars-Henrik
A2 - Lindsay, Peter Alexander
T2 - 11th International Symposium of Formal Methods Europe, FME 2002
Y2 - 22 July 2002 through 24 July 2002
ER -