Title :
Customised induction rules for proving correctness of imperative programs
Author :
Olsson, Ola ; Wallenburg, Angela
Author_Institution :
Dept. of Comput. Sci., Chalmers Univ. of Technol., Goteborg, Sweden
Abstract :
In this paper we develop a method for automatic construction of customised induction rules for use in a semi-interactive theorem prover. The induction rules are developed to prove the total correctness of loops in an imperative language. We concentrate on integers. First we compute a partition of the domain of the induction variable. Our method makes use of failed proof attempts in the theorem prover to gain information about the problem structure and create the partition. Then, based on this partition we create an induction rule, in destructor style, that is customised to make the proving of the loop simpler. Our concern is in user interaction, rather than in proof strength. Using the customised induction rules, we find that in comparison to standard (Peano) induction or Noetherian induction, the proofs become more modularised and simpler user interaction can be expected. Furthermore, by using destructor style induction we circumvent the problem of creating inverses of functions and we use the machinery of a theorem prover (with symbolic execution) to make the method automatic. We also show that the customised induction rules created by the method are sound.
Keywords :
program verification; theorem proving; user interfaces; Noetherian induction; Peano induction; customised induction rules; destructor style induction; imperative program correctness; semiinteractive theorem prover; user interaction; Acoustical engineering; Computer industry; Computer languages; Computer science; Functional programming; Induction generators; Industrial training; Machinery; Software tools; User interfaces;
Conference_Titel :
Software Engineering and Formal Methods, 2005. SEFM 2005. Third IEEE International Conference on
Print_ISBN :
0-7695-2435-4
DOI :
10.1109/SEFM.2005.15