| Summary: | Type-based amortised resource analysis following Hofmann and Jost---where
resources are associated with individual elements of data structures and doled
out to the programmer under a linear typing discipline---have been successful
in providing concrete resource bounds for functional programs, with good
support for inference. In this work we translate the idea of amortised resource
analysis to imperative pointer-manipulating languages by embedding a logic of
resources, based on the affine intuitionistic Logic of Bunched Implications,
within Separation Logic. The Separation Logic component allows us to assert the
presence and shape of mutable data structures on the heap, while the resource
component allows us to state the consumable resources associated with each
member of the structure. We present the logic on a small imperative language,
based on Java bytecode, with procedures and mutable heap. We have formalised
the logic and its soundness property within the Coq proof assistant and
extracted a certified verification condition generator. We also describe an
proof search procedure that allows generated verification conditions to be
discharged while using linear programming to infer consumable resource
annotations. We demonstrate the logic on some examples, including proving the
termination of in-place list reversal on lists with cyclic tails.
|
|---|
