Division of Informatics
Forrest Hill & 80 South Bridge
Technical Paper #37 | |
|---|---|
| Title: | A Heuristic for Case Analysis |
| Authors: | Pientka,B |
| Date: | Jan 1995 |
| Presented: | |
| Keywords: | |
| Abstract: | Case analysis together with recursion are common techniques used in program specifications. In order to verify programs, we use mathematical induction. In this paper, we will outline the importance of non-inductive proof obligations such as case analysis, if we want to prove recursive and non-recursive properties of programs. The heuristic we propose exploits conditions provided by conditional defining equations and selects potential case split variables based on the pattern of the theorem. We will show that proofs obtained with a heuristic for case analysis are often shorter and more sophisticated. Hence it represents a more efficient approach to deal with non-inductive proof obligations. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}