Reasoning about resources in the embedded systems language Hume. (English) Zbl 1445.68044

Loidl, Hans-Wolfgang; Grov, Gudmund

Dal Lago, Ugo (ed.) et al., Foundational and practical aspects of resource analysis. Third international workshop, FOPARA 2013, Bertinoro, Italy, August 29–31, 2013. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 8552, 110-126 (2014).

Summary: 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.
For the entire collection see [Zbl 1326.68011].

MSC:

68N15	Theory of programming languages
03B70	Logic in computer science
68M20	Performance evaluation, queueing, and scheduling in the context of computer systems
68V20	Formalization of mathematics in connection with theorem provers

Software:

Isabelle/HOL