Combining Top-Down and Bottom-Up Techniques in Program Derivation

  • Dipak L. ChaudhariEmail author
  • Om Damani
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9527)


The traditional stepwise refinement based program derivation methodologies are primarily top-down. Strictly following the top-down program derivation approach may require backtracking resulting in rework. Moreover, the top down approach does not directly help in suggesting the next course of action in case of a failed derivation attempt. In this work we seamlessly incorporate a bottom up assumption propagation technique into a primarily top down derivation methodology. We present new tactics for back-propagating the assumptions made during the top-down phase. These tactics help in reducing the guesswork during the derivations. We have implemented these tactics in a program derivation system. With the help of simple examples, we show how this approach is useful for avoiding backtracking thereby simplifying the derivations.


Calculational style Program derivation 



The work of the first author was supported by the Tata Consultancy Services (TCS) Research Fellowship and a grant from the Ministry of Human Resource Development, Government of India.


  1. 1.
    Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Berlin (1998)CrossRefzbMATHGoogle Scholar
  2. 2.
    Backhouse, R., Michaelis, D.: Exercises in quantifier manipulation. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 69–81. Springer, Heidelberg (2006) CrossRefGoogle Scholar
  3. 3.
    Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  4. 4.
    Butler, M., Långbacka, T.: Program derivation using the refinement calculator. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996) CrossRefGoogle Scholar
  5. 5.
    Carrington, D., Hayes, I., Nickson, R., Watson, G.N., Welsh, J.: A tool for developing correct programs by refinement. Technical report (1996).
  6. 6.
    Chaudhari, D.L., Damani, O.: Automated theorem prover assisted program calculations. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 205–220. Springer, Heidelberg (2014) Google Scholar
  7. 7.
    Conchon, S., Contejean, E.: The alt-ergo automatic theorem prover (2008).
  8. 8.
    de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) CrossRefGoogle Scholar
  9. 9.
    Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1997) zbMATHGoogle Scholar
  11. 11.
    Filliâtre, J.-C., Paskevich, A.: Why3 — Where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  12. 12.
    Franssen, M.: Cocktail: A tool for deriving correct programs. In: Workshop on Automated Reasoning (1999)Google Scholar
  13. 13.
    Gries, D.: The Science of Programming, 1st edn. Springer-Verlag New York Inc., Secaucus (1987) zbMATHGoogle Scholar
  14. 14.
    Kaldewaij, A.: Programming: The Derivation of Algorithms. Prentice-Hall Inc., Upper Saddle River (1990) zbMATHGoogle Scholar
  15. 15.
    Morgan, C.: Programming from Specifications. Prentice-Hall Inc., Englewood Cliffs (1990) zbMATHGoogle Scholar
  16. 16.
    Oliveira, M., Xavier, M., Cavalcanti, A.: Refine and gabriel: support for refinement and tactics. In: Proceedings of the Second International Conference on Software Engineering and Formal Methods, 2004, SEFM 2004, pp. 310–319. IEEE (2004)Google Scholar
  17. 17.
    Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: SPASS Version 2.0. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 275–279. Springer, Heidelberg (2002) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Indian Institute of Technology BombayMumbaiIndia

Personalised recommendations