NameDateSize

..25-Jul-201919

AssembleHolfootParser.sigH A D25-Jul-2019191

AssembleHolfootParser.smlH A D25-Jul-20191.7 KiB

EXAMPLES/H25-Jul-20196

hfheader.smlH A D25-Jul-2019438

holfoot.cssH A D25-Jul-2019502

holfoot.grmH A D25-Jul-201914 KiB

holfoot.lexH A D25-Jul-20194.7 KiB

holfoot_pp_print.sigH A D25-Jul-2019452

holfoot_pp_print.smlH A D25-Jul-201951.6 KiB

holfootLib.sigH A D25-Jul-201914.3 KiB

holfootLib.smlH A D25-Jul-2019102.5 KiB

holfootParser.sigH A D25-Jul-2019621

holfootParser.smlH A D25-Jul-201952.7 KiB

holfootParserGenpreds.sigH A D25-Jul-2019205

holfootParserGenpreds.smlH A D25-Jul-201911.8 KiB

holfootScript.smlH A D25-Jul-2019416.7 KiB

holfootSyntax.sigH A D25-Jul-20195.6 KiB

holfootSyntax.smlH A D25-Jul-201914.1 KiB

HolmakefileH A D25-Jul-20191.8 KiB

mosml/H25-Jul-20193

Parsetree.smlH A D25-Jul-20192.9 KiB

poly/H25-Jul-201911

READMEH A D25-Jul-20193.9 KiB

selftest.smlH A D25-Jul-20192.8 KiB

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