Towards sound refactoring in ERLANG

Abstract

Refactoring tools aim to improve program code without affecting the observable behaviour of the said code. The problem with refactoring tools for actor-based programming languages such as ERLANG is that either the tool only provides simple refactorings, or it provides complex refactorings without guaranteeing that the behaviour is preserved. The shortage of more effective refactorings is, in part, due to the lack of a semantic theory for ERLANG actors. This would allow us to develop formal proofs for behaviour preservation a priori, which could in turn be used to verify the correctness of the refactoring tool. In this work, we develop a test-based semantic theory for behaviour preservation of concurrent actor programs such as those constructed in ERLANG. In ERLANG, the accepted notion of program correctness is that of passing a suite of tests, and testing frameworks and test case generators are often used. However, software testing is ultimately a means to an end, i.e., to attempt to determine if an application behaves as expected. We therefore develop a formal definition for a test-based preorder that quantifies over the set of all possible tests. This definition is most useful for determining when a refactoring is erroneous, achieved by identifying a witness test which no longer passes after refactoring. However, proving two actor systems are related by this preorder is a difficult task as the definition is infinitary. We thus develop a sound and complete alternative characterisation which is tracebased, and therefore does not quantify over all possible tests. The development of an alternative characterisation was particularly challenging in our case due to inherent characteristics of the actor model such as asynchrony, persistence and the single receiver property.