Holfoot
Description
Holfoot is an implementation
of Smallfoot
inside the HOL 4 theorem prover. In addition to the features supported
by Smallfoot it can handle data and supports interactive
proofs. Moreover, it can handle arrays.
It is described in detail in my dissertation.
Simple specifications with data like copying a list can be handled
automatically. More complicated ones like fully functional
specifications of filtering a list, mergesort, quicksort or an
implementation of red-black trees require user interaction. During
this interaction all the features of the HOL 4 theorem prover can be
used, including the interface to external SMT solvers like Yices.
HOL 4 is needed to run Holfoot interactively. For purely automated useage
precompiled command-line versions are available.
Downloads
- Holfoot (32 bit, x86, Linux)
(4.03 MB, last update 1 Mar 2013 08:50)
A command-line version of holfoot. It supports completely
automated proofs (and stepping through automatic proofs).
Interactive proofs are not supported in this command-line
version. You need to run holfoot inside HOL 4 to use its full
power.
There is a 32- and a 64-bit version. If your system supports both,
the 32-bit one is usually the better choice. It's faster and smaller than the
64-bit version.
- Holfoot (64 bit, x86, Linux)
(4.92 MB, last update 1 Mar 2013 08:50)
- Holfoot (extended version) (32 bit, x86, Linux)
(20.3 MB, last update 1 Mar 2013 08:50)
This command-line version of Holfoot is able to run the interactive proof scripts.
To do so, unpack the archive and go to the EXAMPLES directory. There run
../holfoot -f interactive/???.hol, where ??? represents the example of
your choice.
This binary is intended as an easy way to get an overview of the use of Holfoot. It's not intended for
longer use or the development of own proofs. Compared to running Holfoot inside HOL 4, it
has a lot of substantial limitations
(just use prewritten scripts instead of true interaction, a limited number of libraries, ...).
So, please use Holfoot inside the HOL theorem prover if want to have more than just a quick lock.
Instructions on how to download and install HOL can be found at the HOL 4 - webpage.
- Holfoot (Apple, 64 bit Intel) (4.17 MB, last update 1 Mar 2013 08:50) An Apple version that is dynamically linked and requires PolyML
libraries to be available. Since I don't have easy access to a
Mac, I did not compile it myself and did not test it.
- Holfoot sources are available on GitHub in the HOL 4 repository.
It can be found in subdirectory examples/separationLogic
Web-Interface
Documentation