A Framework for Reasoning about ERLANG Code

by Fredlund, Lars-Åke

Fredlund, L.- ?A. 2001: A Framework for Reasoning about ERLANG Code. TRITA-IT AVH 01:04, Department of Microelectronics and Information Technology, Stockholm. ISSN 1403- 5286. We present a framework for formal reasoning about the behaviour of software written in ERLANG, a functional programming language with prominent support for process based concurrency, message passing communication and distribution. The framework contains the following key ingredients: a specification language based on the µ-calculus and first-order predicate logic, a hierarchical small-step structural operational semantics of ERLANG, a judgement format allowing parametrised behavioural assertions, and a Gentzen style proof system for proving validity of such assertions. The proof system supports property decomposition through a cut rule and handles program recursion through well-founded induction. An implementation is available in the form of a proof assistant tool for checking the correctness of proof steps. The tool offers support for automatic proof discovery through higher–level rules tailored to ERLANG. As illustrated in several case studies this framework provides the expressive power required by the open and dynamic nature of distributed systems. Lars- ?Ake Fredlund, Department of Microelectronics and Information Technology, Royal Institute of Technology, KTH Electrum 229, SE-16440 Kista, Sweden, E-mail: fred@sics.se