A New Roadmap on Linking Theories of Programming
He Jifeng · 2016
Formal methods advocate the crucial role played by the algebra of programs in specification and implementation of programs. Study leads to the conclusion that both the top-down approach (with denotational model as its origin) and the bottom-up approach (a journey started from operational model) can meet in the middle with a program algebra. This paper proposes a new approach on linking theories of programming. Given a program algebra, we construct a test operator taking a test case and the testing program as its arguments. The operator yields a collection of observations of the test outcomes. The denotational model of a program can be derived as a binary relation which relates the test cases with their outcomes. An operational model is considered as consistent if its step relation is consistent with the algebraic semantics.