1. Jules Villard
  2. Heap-Hop


Copyright 2001-2009
Jules Villard (jules.villard@ens-lyon.org)
Etienne Lozes (lozes@lsv.ens-cachan.fr)

Code of Smallfoot copyrighted by
Cristiano Calcagno (ccris@doc.ic.ac.uk),
Josh Berdine (berdine@dcs.qmul.ac.uk),
Peter O'Hearn (ohearn@dcs.qmul.ac.uk)

tree_shares.ml and tree_shares.mli are part of the Mechanized Semantic
Library (http://msl.cs.princeton.edu/) and are (c) 2009, Andrew Appel,
Robert Dockins and Aquinas Hobor.

Unless specified otherwise at the top of the file, all files are
distributed under the terms of the Q Public License version 1.0 with a
change to choice of law. You should have received a copy of this
license with this software (see LICENSE).

Heap-Hop is a prover for concurrent heap-manipulating programs that
use Hoare monitors and message-passing synchronization. Programs are
annotated with pre and post-conditions and loop invariants, written in
a fragment of separation logic. Communications are governed by a form
of session types called contracts.  Heap-Hop can prove safety and
race-freedom and, thanks to contracts, absence of communication errors
and memory leaks.  For further information see:


Compilation requires OCaml (version 3.07 or later).  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 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 contract's graphical representation, you will need a
".dot" viewer. See http://en.wikipedia.org/wiki/DOT_language
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

See the EXAMPLES and SMALLFOOT_EXAMPLES directories for some
sample programs.

For instance:

    $ ./heaphop EXAMPLES/send_list.hop

    Function putter

    Function getter

    Function send_list

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, and a brief description.

Note that the source code locations are printed in standard form, and
so e.g. emacs can parse them.  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.
This is particularly useful with e.g. "./heaphop -all_states

Syntax overview

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 - switch - receive

Note that switch receive are optional when there is only one receive.
Similarly, x = receive(m,e) should 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:

ep  : is 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, that is 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 specifications of 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

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

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