Capturing the Divide and Conquer Methodology in Isabelle Tactics

Johannes Herrmann
Logic and AI Group Department of Computer Science, The University of Western Australia, Nedlands 6907, Australia.
hannes@cs.uwa.edu.au

C.P.Tsang
Logic and AI Group Department of Computer Science, The University of Western Australia, Nedlands 6907, Australia.
tsang@cs.uwa.edu.au

Abstract

The Divide and Conquer methodology is commonly used in all forms of programming, and its corresponding proof tactic would be useful for proving recursive specifications. In this paper we address the issues of extracting a program from the constructive proof of a specification, in this case the specification of a data-structure and a pair of conditions.

We have designed methods for constructive proof in first-order logic which allow us to extract the Divide and Conquer algorithm. These methods are then captured in Isabelle tactics. The exact methods used to obtain the tactics are discussed, as well as possible modifications to our methods to account for different data-structures and conditions. We show the implementation of algorithms based on Divide and Conquer by modifying the conditions. We also show that the Isabelle theory FOLP (First Order Logic with Proof terms) can be considered as a verification system for stepwise refinement.

One of the aims of our implementation is to minimise the number of functions to be supplied by the user, and to make those that have to be supplied as simple as possible. We show the flexibility of our approach by applying our methodology to lists and binary trees. We compare the steps required to prove either case, and show that there are similarities in style despite the differences in the structures.

Conference Home Page