A New Roadmap for Linking Theories of Programming

  • He JifengEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10134)


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.


Machine State Operational Semantic Program Variable Weak Precondition Predicate Transformer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



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).


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

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Shanghai Key Laboratory of Trustworthy Computing, International Research Center of Trustworthy SoftwareEast China Normal UniversityShanghaiChina

Personalised recommendations