Referential Opacity in Equational Reasoning

Jo Erskine Hannay


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 the equational calculus by simply restricting the congruence axiom, and see how the motivation for this naturally arises from the forget-identify (FI) and forget-restrict-identify (FRI) approaches to specification refinement.


This report is available in the following formats:

Previous | Index | Next