[isabelle] auto2 on imperative programs

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

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

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.