Email Gateway (Aug 22 2022 at 11:13): Email Gateway (Aug 22 2022 at 11:13):From: Bohua Zhan <bzhan@mit.edu>
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:
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
Last updated: Apr 25 2024 at 12:23 UTC