SPLASH 2014
Mon 20 - Fri 24 October 2014 Portland, Oregon, United States
Mon 20 Oct 2014 10:30 - 11:00 at Salon G - Research Papers Chair(s): Marco Servetto

Abstract: Often when programmers modify source code they intend to preserve some parts of the program behaviour. We propose a formal criterion by which to characterise the preserved part of the program behaviour. Two program versions are equivalent up to a set of affected objects A, if executions of the two versions correspond at each execution step when we do not consider the objects in A. We propose a sufficient condition for this criterion. It suffices to establish that traces of method calls and returns between A objects and other objects are equivalent. Examining the stack and heap at each execution step is not necessary. We give a proof of the sufficiency of this condition, much of which we have automatically verified using Dafny. We also discuss our experiences with Dafny and detail how some interesting parts of our Dafny proof work.