README
1A formalisation of a tool similar to Smallfoot in HOL
2
3(**************************************************************************)
4(* ACKNOWLEDGEMENT *)
5(* *)
6(* I would like to thank Cristiano Calcagno, Josh Berdine and Peter *)
7(* W. O'Hearn - the authors of Smallfoot - which generously allowed me to *)
8(* use large parts of the Smallfoot parser and the examples. Smallfoot *)
9(* can be found at *)
10(* *)
11(* http://www.dcs.qmul.ac.uk/research/logic/theory/projects/smallfoot. *)
12(**************************************************************************)
13
14(**************************************************************************)
15(* BUILDING *)
16(* *)
17(* Holfoot is designed to work mainly with PolyML and the experimental *)
18(* kernel. It should work with mosml, but then building instructions for *)
19(* the command line version and the header file have to be adapted. *)
20(* Moreover, some variable names in the proof-scripts might need changing *)
21(* when using the standard kernel. *)
22(* *)
23(* To build Holfoot, please do *)
24(* - build HOL (using experimental kernal and PolyML 5.3) *)
25(* - call "Holmake --qof -k" in directory *)
26(* "examples/separationLogic/src/holfoot" and then in *)
27(* "examples/separationLogic/src/holfoot/(yourml)" *)
28(* - if using polyML a state-file, the command-line tool and *)
29(* the web-interface executable should be in directory poly *)
30(* - for instructions on how to use this command-line tool, call *)
31(* "holfoot -h" or test it on the examples in EXAMPLES/automatic via *)
32(* "holfoot EXAMPLES/automatic/*" *)
33(* *)
34(**************************************************************************)
35
36(**************************************************************************)
37(* MOSML/POLYML *)
38(* *)
39(* The ml-specific code is in subdirectories called poly and mosml. *)
40(* Holfoot is mainly build for PolyML and the experimental kernel. For *)
41(* example the command-line-tool is intended to be compiled by PolyML. *)
42(* Moreover the initialisation code differs for both systems. *)
43(**************************************************************************)
44
45(**************************************************************************)
46(* EXAMPLES *)
47(* *)
48(* The directory EXAMPLES contains some example specifications and *)
49(* proofs. All examples in "automatic" work fully automatic and can be *)
50(* used with the command line tool. *)
51(* *)
52(* The examples in "interactive" need user interaction, i.e. customised *)
53(* proof scripts. For each file there is a file with the ending ".hol". *)
54(* This file contains the proof script. These scripts depend on a working *)
55(* "header.sml" file to initialise holfoot. *)
56(**************************************************************************)
57
58
59Thomas Tuerk
60