Proving correctness w.r.t. specifications with hidden parts

Jordi Farres-Casals

Abstract: The task of proving the correctness of an implementation w.r.t. a formal specification is sometimes complicated by the use of auxiliary (hidden) functions and sorts within the specification which are needed for the specification but are not meant to be implemented.

Auxiliary sorts and functions are the normal way to express requirements in abstract model specification. Algebraic specifications became popular as a way to define the elements of a system without representing them in terms of more primitive concepts, avoiding the definition of any extra structure. However, it has been shown that hidden functions are in general necessary for specifying computable functions [Maj 77, TWW 79].

In this paper we analyze general proving techniques for specifications with hidden parts and, in particular, a strategy which is complete when some side conditions are met.

LFCS report ECS-LFCS-90-117

Previous | Index | Next