Abstract
A new approach for automating the construction and verification of imperative programs is presented. Based on the standard methods of Floyd, Dijkstra, Gries and Hoare, it supports proof and refutation games with automated theorem provers, model search tools and computer algebra systems combined with “hidden” domain-specific algebraic theories that have been designed and optimised for automation. The feasibility of this approach is demonstrated through fully automated correctness proofs of some classical algorithms: Warshall’s transitive closure algorithm, reachability algorithms for digraphs, and Szpilrajn’s algorithm for linear extensions of partial orders. Sophisticated mathematical methods that have been developed over decades could thus be integrated into push-button engineering technology.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)
Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)
Berghammer, R.: Combining Relational Calculus and the Dijkstra-Gries Method for Deriving Relational Programs. Information Sciences 119, 155–171 (1999)
Berghammer, R., Leoniuk, B., Milanese, U.: Implementation of Relation Algebra using Binary Decision Diagrams. In: de Swart, H. (ed.) RelMiCS 2001. LNCS, vol. 2561, pp. 241–257. Springer, Heidelberg (2002)
Berghammer, R., Neumann, F.: RelView – an OBDD-based computer algebra system for relations. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) CASC 2005. LNCS, vol. 3718, pp. 40–51. Springer, Heidelberg (2005)
Berghammer, R.: Applying Relation Algebra and RelView to Solve Problems on Orders and Lattices. Acta Informatica 45, 211–236 (2008)
Cormen, T.H., Leiserson, C.E., Rivest, D.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)
Desharnais, J., Struth, G.: Modal Semirings Revisited. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 360–387. Springer, Heidelberg (2008)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Floyd, R.W.: Assigning Meanings to Programs. In: Proc. AMS Symposia on Applied Mathematics, vol. 19, pp. 19–31 (1967)
Gries, D.: The Science of Computer Programming. Springer, Heidelberg (1981)
Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10), 576–580 (1969)
Höfner, P., Struth, G.: Algebraic Reasoning with Prover9 (2009), www.dcs.shef.ac.uk/~georg/ka/
Höfner, P., Struth, G.: Automated Reasoning in Kleene Algebra. In: Pfenning, P. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 279–294. Springer, Heidelberg (2007)
Höfner, P., Struth, G.: On Automating the Calculus of Relations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 50–66. Springer, Heidelberg (2008)
Jackson, D.: Software Abstractions. The MIT Press, Cambridge (2006)
Kozen, D.: Kleene Algebra with Tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (1997)
Maddux, R.D.: Relation Algebras. Elsevier, Amsterdam (2006)
McCune, W.: Prover9 and Mace4 (2007), www.prover9.org
Ng, J.: Relation Algebras with Transitive Closure. Ph.D. thesis, University of California, Berkeley (1984)
Schmidt, G., Ströhlein, T.: Relations and Graphs. Springer, Heidelberg (1993)
Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall, Englewood Cliffs (2006)
Szpilrajn, E.: Sur l’extension de l’ordre partiel. Fundamenta Math. 16, 386–389 (1930)
Tarski, A.: On the Calculus of Relations. J. Symbolic Logic 6, 73–89 (1941)
Warshall, S.: A Theorem on Boolean Matrices. Journal of the ACM 9, 11–12 (1962)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berghammer, R., Struth, G. (2010). On Automated Program Construction and Verification. In: Bolduc, C., Desharnais, J., Ktari, B. (eds) Mathematics of Program Construction. MPC 2010. Lecture Notes in Computer Science, vol 6120. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13321-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-13321-3_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13320-6
Online ISBN: 978-3-642-13321-3
eBook Packages: Computer ScienceComputer Science (R0)