A notion of refinement is defined in the context of coalgebraic 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 seelction functions between procedure-inputs and attribute-outputs, which gives this notion considerable flexibility. The coalgebraic approach allows us to use coinductive proofmethods in establishing refinements (via (bi) simulations). This is illustrated in several examples.
展开▼
