Heap-Hop

The Heap-Hop sources are available on the tool's website: heaphop.

ocaml (version 3.07 or later) is required to compile it. After unpacking the tarball, performing cd heaphop ; make will build the native code executable heaphop, and make heaphop.byte will build the bytecode executable heaphop.byte. These programs do not hardcode any paths, so they can be moved anywhere after compilation.

If you use emacs, you may copy the file heaphop.el to a directory /some/where/ and then add the following lines to your .emacs file:

;; heaphop !
(setq auto-mode-alist (cons `("\\.sf\\'" . heap-hop-mode) auto-mode-alist))
(setq auto-mode-alist (cons `("\\.hop\\'" . heap-hop-mode) auto-mode-alist))
(autoload 'heap-hop-mode "/some/where/heaphop.el" "Major mode for Heap-Hop" t)

If you want to see the graphical representation of contracts, you will need a .dot viewer. See the wikipedia page for instance.

heaphop [options] <file>, where the following command line options are accepted:

-verbose

Display additional internal information

-all_states

Display intermediate states

-very_verbose

Display more additional internal information

-help

Display usage message

For instance

$ ./heaphop EXAMPLES/send_list.hop

Function putter

Function getter

Function send_list
Valid

indicates a successful verification, while:

$ ./heaphop EXAMPLES/send_list_bug.hop 

Function putter
File "EXAMPLES/send_list_bug.hop", line 35, characters 4-14:
ERROR: lookup x->tl in 0!=e * 0!=x * split_1!=e * e!=x
       * e |-> st:{wait},ep:1,cid:C,rl:server
       * listseg(tl; split_1, 0)

Function getter

Function send_list

NOT Valid

indicates a failed verification, identifying the source code location associated with the error, a brief textual description, and the implication which the theorem prover failed to verify.

Note that the source code locations are printed in standard form, so e.g. emacs can parse them and highlight the position in the source code. That is, after executing the M-x compile function with ./heaphop EXAMPLES/send_list_bug.hop as the compile command, M-x next-error will indicate the source locations.

Heap-Hop also generates .dot files representing the contracts that appear in the file passed as an argument. For a contract C, the file is named output-C.dot.

The programming language of heaphop is an extension of the one of Smallfoot, and basically follows the same syntax. The main difference is that new keywords are available (see examples for their use):

message - contract - initial - final - state
open - close - send - receive - switch receive

Note that switch receive are optional when there is only one receive. Similarly, x = receive(m,e) can be written receive(m,e) when the value of the message is irrelevant.

The logical language of heaphop is also an extension of the one of Smallfoot. The new feature is the endpoint's predicate e|->C{s} or e|->~C{s} that indicates that e is an endpoint of a channel ruled by contract C (respectively the dual of C), and it is currently in contract's state s. The extended form of this predicate permits to precise all fields of an endpoint's structure, namely:

field	description
ep	true iff the cell is an endpoint
cid	contract's identifier
st	current state in the contract
pr	endpoint's peer
rl	endpoint's role: either server (follows contract)
	or client (follows dual contract)

The pr field might be useful to state that some endpoint keeps the same peer across the program, see for instance send_list_dualized.hop. Note that one uses existentially quantified variables for this, whose identifier should start with an underscore.

Two new keywords are available for specifying message invariants:

• val represents the value of the message.
• src represents the endpoint that emitted the message

Messages with several values are also supported with the following slight changes in the syntax:

message twice  [val0==val1]
message thrice [val0==val1 * val1==val2]

send(twice,e,0,0);
(x,y) = receive(twice,f);
send(thrice,e,0,0,0);
(x,y,z) = receive(thrice,f);