On Oracles for Interpreting Test Results against Algebraic Specifications

摘要

This paper presents a solution to the so-called oracle problem for oracles derived from flat algebraic specifications expressed in first-order logic. The oracle problem in this context reduces to the general problem of comparing two values of a non-observable sort and also to the limitations imposed by quantifiers. The solution is based on constructing an oracle where equality between values of a non-observable sort is computed by one of two "approximate" equalities, according to the context in which the equation occurs. The interpretation given by the oracle does not make any assumptions on test sets and depends on how these equalities approximate the behavioural equality, which is based on behavioural theories, and also on the use of quantifiers.