Behaviour-refinement of coalgebraic specifications with coinductive correctness proofs

Abstract

A notion of refinement is defined in the context of coatgebraic specification of classes in object-oriented languages. It tells us when objects in a “concrete” class behave exactly like (or: simulate) objects in an “abstract” class. The definition of refinement involves certain selection functions between procedure-inputs and attribute-outputs, which gives this notion considerable flexibility. The coatgebraic approach allows us to use coinductive proof methods in establishing refinements (via (bi)simulations). This is illustrated in several examples.