Combining Top-Down and Bottom-Up Techniques in Program Derivation
- 252 Downloads
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.
KeywordsCalculational 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.
- 5.Carrington, D., Hayes, I., Nickson, R., Watson, G.N., Welsh, J.: A tool for developing correct programs by refinement. Technical report (1996). http://espace.library.uq.edu.au/view/UQ:10768
- 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.Conchon, S., Contejean, E.: The alt-ergo automatic theorem prover (2008). http://alt-ergo.lri.fr
- 12.Franssen, M.: Cocktail: A tool for deriving correct programs. In: Workshop on Automated Reasoning (1999)Google Scholar
- 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