# A New Roadmap for Linking Theories of Programming

## Abstract

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.

## Keywords

Machine State Operational Semantic Program Variable Weak Precondition Predicate Transformer## Notes

### Acknowledgements

This work is supported by National Natural Science Foundation of China (Grant No. 61321064), Shanghai Knowledge Service Platform Project (No. ZF1213) and the NSFC-Zhejiang Joint Fund for the Integration of Industrialization and Informatization (No. U1509219).

## References

- 1.Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge Press, Cambridge (1996)CrossRefzbMATHGoogle Scholar
- 2.Abrial, J.-R.: Modelling in Event-B: System and Software Engineering. Cambridge Press, Cambridge (2010)CrossRefzbMATHGoogle Scholar
- 3.Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
- 4.Henner, E.C.R.: Predicative programming, Part 1, 2. Commun. ACM
**27**(2), 134–151Google Scholar - 5.Hennessy, M.C.: Algebraic Theory of Process. The MIT Press, Cambridge (1988)zbMATHGoogle Scholar
- 6.Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM
**12**, 576–583 (1969)CrossRefzbMATHGoogle Scholar - 7.Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Upper Saddle River (1985)zbMATHGoogle Scholar
- 8.Hoare, C.A.R., et al.: Laws of programming. Commun. ACM
**30**(8), 672–686 (1987)MathSciNetCrossRefzbMATHGoogle Scholar - 9.Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)zbMATHGoogle Scholar
- 10.Jones, C.B.: Systematic Software Development Using VDM. Prentice Hall, Englewood Cliffs (1986)zbMATHGoogle Scholar
- 11.Milner, R.: Communicating and Mobile Systems: The \(\pi \)-Calculus. Cambridge Univ. Press, Cambridge (1999)zbMATHGoogle Scholar
- 12.G.D. Plotkin. A structural approach to operational semantics. Technical report, DAIMI-FN-19, Aarhus University, Denmark, (1981)Google Scholar
- 13.Roscoe, A.W.: Laws of occam programming. Theoret. Comput. Sci.
**60**, 177–229 (1988)MathSciNetCrossRefzbMATHGoogle Scholar - 14.Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall (1998)Google Scholar
- 15.Spivey, J.M., Notation, T.Z.: A Reference Manual. Prentice Hall, Englewood Cliffs (1992)Google Scholar