Verifiable Semantic Difference Languages

Characterizing the differences between two close versions of the same program is a crucial and frequent activity during software development, being for change review, bug fixing or feature extension. Nonetheless, determining the meaning of such differences is up-to-now only done by humans, tools supporting this activity being only text-based (diff, patch, version control systems, ...).

We propose a foundational framework to semantically characterize the difference of behavior between two close programs. This framework relies on small-step-prediction oracles that consume one reduction step of one program and produce a potentially empty finite sequence of reduction steps of the other program.

Such oracles are operational, can handle diverging or stuck computations, difference in evaluation order and can express local differences independently of evaluation contexts of compared programs. They can be composed, allowing to characterize a difference as a sequence of simpler differences. Last but not least, small-prediction-step oracles can be explained to programmers in terms of evaluation of the two compared programs.