- Abstract:
- We introduce a reasoning infrastructure for proving statements on resource consumption in an abstract fragment of the Java Virtual Machine Language (JVML). The infrastructure is based on a small hierarchy of program logics, with increasing levels of abstraction: at the top there is a type system for a high-level language that encodes resource consumption. % da: added PCC motivation The infrastructure is designed to be used in a proof-carrying code (PCC) scenario, where mobile programs can be equipped with formal evidence that they have good resource behaviour. This article presents the core logic in our infrastructure, a VDM-style program logic for partial correctness, that can make statements about resource consumption in a general form. % da: avoid effects baggage (or more general ``effects''). We establish some important results for this logic, including soundness and completeness with respect to a resource-aware operational semantics for the JVML. We also present a second logic built on top of the core logic, which is used to express termination; it is also shown to be sound and complete. The entire infrastructure has been formalised in the theorem prover Isabelle/HOL, both to enhance confidence in the meta-theoretical results, and to provide a prototype implementation for PCC. We give examples to show the usefulness of this approach, including proofs of resource bounds on code resulting from compiling high-level functional programs.
- Links To Paper
- 1st link
- Bibtex format
- @Article{EDI-INF-RR-0296,
- author = {
David Aspinall
and Lennart Beringer
and Martin Hofmann
and Hans-Wolfgang Loidl
and Alberto Momigliano
},
- title = {A Program Logic for Resources},
- journal = {A Program Logic for Resources},
- publisher = {Theoretical Computer Science},
- year = 2007,
- month = {Dec},
- doi = {http://dx.doi.org/10.1016/j.tcs.2007.09.003},
- url = {http://homepages.inf.ed.ac.uk/amomigl1/papers/TCS.pdf},
- }
|
