Abstraction barriers in equational proof

Abstract

Module constructs in programming languages have protection mechanisms hindering unauthorised external access to internal operators of data types. In some cases, granting external access to internal operators would result in serious violation of a data type's specified external properties. In order to reason consistently about specifications of such data types, it is necessary in general to incorporate a notion of protective abstraction barrier in proof strategies as well. We show how this can be done in equational calculus by simply restricting the congruence axiom, and see how the motivation for this naturally arises from FI and FRI approaches to specification refinement.