Modular Correctness Proofs of Behavioural Implementations

. We introduce a concept of behavioural implementation for algebraic specifications which is based on an indistinguishability relation (called behavioural equality). The central objective of this work is the investigation of proof rules that first allow us to establish the correctness of behavioural implementations in a modular (and stepwise) way and, moreover, are practicable enough to induce proof obligations that can be discharged with existing theorem provers. Under certain conditions our proof technique can also be applied for proving the correctness of implementations based on an abstraction equivalence between algebras in the sense of Sannella and Tarlecki. The whole approach is presented in the framework of total algebras and first-order logic with equality. 1 Introduction Algebraic specification techniques allow one to formalize correctness notions for program development steps. Thereby an important role is played by observability concepts since it is often essential to abst..