Coinduction for preoredered algebras
We develop a combination, called hidden preordered algebra,
between preordered algebra, which is an algebraic framework
supporting specification and reasoning about transitions,
and hidden algebra, which is the algebraic
framework for behavioural specification.
This combination arises naturally within the heterogeneous framework
of the modern formal specification language CafeOBJ.
The novel specification concept arising from this combination,
and which constitutes its single unique feature,
is that of behavioural transition.
We extend the coinduction proof method for behavioural equivalence to
coinduction for proving behavioural transitions.
back to Selected Publications