Behavioural correctness of data representations

AbstractTwo methods for proving the correctness of data representations are presented which employ a mathematical relation between the data values in a representation and those in its abstract model. One method reflects the behavioural equivalence relation of abstract data type theory, and the other a new “behavioural inclusion” notion that formalizes the idea of a “partial representation” of a data type.These correctness concepts and proof methods are strictly more general than the conventional ones based on abstraction functions, and they are no longer affected by “implementation bias” in specifications