zbMATH — the first resource for mathematics

Reasoning about resources in the embedded systems language Hume. (English) Zbl 1445.68044
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].
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
Full Text: DOI