TY - GEN
T1 - A new roadmap for linking theories of programming
AU - Jifeng, He
N1 - Publisher Copyright:
© Springer International Publishing AG 2017.
PY - 2017
Y1 - 2017
N2 - Formal methods advocate the crucial role played by the algebraic approach in specification and implementation of programs. Traditionally, a top-down approach (with denotational model as its origin) links the algebra of programs with the denotational representation by establishment of the soundness and completeness of the algebra against the given model, while a bottom-up approach (a journey started from operational model) introduces a variety of bisimulations to establish the equivalence relation among programs, and then presents a set of algebraic laws in support of program analysis and verification. This paper proposes a new roadmap for linking theories of programming. Our approach takes an algebra of programs as its foundation, and generates both denotational and operational representations from the algebraic refinement relation.
AB - Formal methods advocate the crucial role played by the algebraic approach in specification and implementation of programs. Traditionally, a top-down approach (with denotational model as its origin) links the algebra of programs with the denotational representation by establishment of the soundness and completeness of the algebra against the given model, while a bottom-up approach (a journey started from operational model) introduces a variety of bisimulations to establish the equivalence relation among programs, and then presents a set of algebraic laws in support of program analysis and verification. This paper proposes a new roadmap for linking theories of programming. Our approach takes an algebra of programs as its foundation, and generates both denotational and operational representations from the algebraic refinement relation.
UR - https://www.scopus.com/pages/publications/85010641610
U2 - 10.1007/978-3-319-52228-9_2
DO - 10.1007/978-3-319-52228-9_2
M3 - 会议稿件
AN - SCOPUS:85010641610
SN - 9783319522272
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 26
EP - 43
BT - Unifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers
A2 - Bowen, Jonathan P.
A2 - Zhu, Huibiao
PB - Springer Verlag
T2 - 6th International Symposium on Unifying Theories of Programming, UTP 2016
Y2 - 4 June 2016 through 5 June 2016
ER -