Loading...
Please wait, while we are loading the content...
Similar Documents
A Proof Method based on Folding Lemmas : Applications to Algorithm
| Content Provider | Semantic Scholar |
|---|---|
| Author | Bonnier, Correctness Sta An Laurent Fribourg L. |
| Copyright Year | 2007 |
| Abstract | In Fri92] a proof method was developed for proving arithmetic consequences of Horn clause programs deened over integer lists and integers. To be applicable, the method requires the recursion schemes of all predicates involved to be compatible. This is to guarantee a sequence of unfold transformations to eventually lead to a foldable clause. In this paper we consider the case when such a compatibility is not present. To enable folding folding lemmas are constructed. The proof then proceeds using the old method, and the theorem is proved with the lemmas as hypotheses. The method is illustrated by proving correctness criteria for Boyer and Moore's string matching algorithm and for Dijkstra's descending subsequence algorithm. |
| File Format | PDF HTM / HTML |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
