*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] auto2 on imperative programs*From*: Bohua Zhan <bzhan at mit.edu>*Date*: Sat, 19 Sep 2015 11:07:45 -0400

Hi, everyone I have uploaded the newest version of auto2, with work done over the summer. The main addition is examples on verifying imperative programs, in the framework of Imperative_HOL. The repository is at: https://github.com/bzhan/auto2 The main algorithms verified are: - Reverse and quicksort on arrays. - Insert, delete, reverse, and merge on linked lists. - Insert and delete on binary trees. Examples on arrays and linked lists follow the corresponding ones in HOL/Imperative_HOL/ex. Similar to examples in Imperative_HOL/ex, the proofs use directly the semantics of the heap monad. All loops are defined by recursion, and properties of recursive functions are proved by induction. No Hoare logic or separation logic is used (although some of the abstractions may be inspired by separation logic, as is necessary to deal with disjointness of sets of pointers, etc). The proofs are "mostly" automatic - only a few lines of hints are needed to give intermediate steps. Some technical notes: - I added a "comment" command similar to "assert". It is used to state intermediate results about variables in the middle of imperative functions. It is never intended to be evaluated (and in fact, often cannot be evaluated algorithmically). Right now the semantics is that all comments must be true for a function to "succeed", which of course cannot be realized in actual execution - so some restructuring would be needed for this to make more sense. - For both linked lists and binary trees, I defined proper-ness of a pointer as distinctness of reachable pointers. For linked lists, this is equivalent to the fact that the traversal of the pointer is a finite list. For binary trees it is different. The documentation is updated to reflect all the internal changes, but unfortunately I haven't had time to explain the newer examples in detail. Nevertheless I would be happy to answer any questions about them here. Any comments are also welcome. Thanks, Bohua

- Previous by Date: Re: [isabelle] some problems with the /\ quantifier
- Next by Date: Re: [isabelle] Isabelle Foundation & Certification (answer to Makarius)
- Previous by Thread: Re: [isabelle] Isabelle Foundation & Certification (answer to Makarius)
- Next by Thread: [isabelle] Lawrence Paulson's 60th Birthday today
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list