This directory contains the Isabelle/HOL 2007 source for the Hume formalisation
described in the paper:
 "Reasoning about Resources in the Embedded Systems Language Hume"
  Hans-Wolfgang Loidl, Gudmund Grov.
  To appear in FOPARA'13 --- Third International Workshop on Foundational and Practical Aspects of Resource Analysis,
  CEUB, Bertinoro, Italy, August 29th to 31st, 2013.
  URL: http://www.macs.hw.ac.uk/~dsg/projects/hume-reasoning.html#FOPARA13

Abstract:
In this paper we present an instrumented program logic for the embedded systems language Hume,
suitable to reason about resource consumption. Matching the structure of Hume programs, it
integrates two logics, a VDM-style program logic for the functional language and 
a TLA-style logic for the coordination language of Hume.
We present a soundness proof of the program logic, and demonstrate
the usability of these logics by proving resource bounds for a Hume program.
Both logics, the soundness proof and the example have been fully formalised in the Isabelle/HOL theorem prover.


The structure of the files is as follows

README         ... this file
Coord/	       ... coordination-layer formalisation
Expr/          ... expression-layer formalisation
Integrated.thy ... theory integrating both (through Theorem vdmexe)
ListCopy.thy   ... list-copy example (expression layer), with proof of resource bound
ST.thy         ... list-copy example (coordination layer)

./Coord:
Hume/
Intensional.thy
Liveness.thy
PreFormulas.thy
Rules.thy
Semantics.thy
Sequence.thy
State.thy

./Coord/Hume:
HumeSemantics.thy
Hume.thy        ... main theory for the TLA-style formalisation of the coordination language

./Expr:
Basics.thy
DummyExpr.thy
Finmap.thy
Grail.thy
GRUMPY.thy      ... main theory for the soundness proof of the VDM-style program logic
Lang.thy
ResAlg.thy
VdmDerived.thy
VM.thy

The main example of the paper corresponds to ListCopy.thy (expression level) with these theorems:
 . copy_resources_ok
 . fuse_resources_ok
and theory ST.thy, which proves the components of Theorem 4 in the paper.

We hope you find these theories useful!
--
 Hans-Wolfgang Loidl & Gudmund Grov