Hidden congruent deduction

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

Behavioural specification is becoming an interesting concept in that programs usually fail to satisfy all its requirements strictly, but they appear to be satisfied under every experiment that can be performed. This is why it is interesting to develop techniques for behavioural verification. This paper presents some techniques of this kind which are called hidden algebra, clustered around the concept of coinduction. Proofs by coinduction are dual to proofs by induction. The latter requires choosing a set of constructors and is based on a smallest subalgebra, the former requires a cobasis (the dual notion) and is based on a largest congruence, and in both cases the right choice can result in a dramatically simplified proof. A complication arises in that the best choice of a cobasis may not be part of the given signature, but rather contain operations that can be defined over it. The contributions of this paper are a more general notion of congruence together with an easy-to-check criterion for operations to be congruent, the notion of cobasis, and the extension of concepts and results of hidden algebra to encompass operations with more than one hidden argument. For the entire collection see [Zbl 0933.00012].

Recommendations

Cited in

(15)

Describes a project that uses

Uses Software

CafeOBJ

This page was built for publication: Hidden congruent deduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4503915)