Coalgebraic Description of Generalized Binary Methods

We extend the Reichel-Jacobs coalgebraic account of specification and refinement of objects and classes in Object Oriented Programming to (generalized) binary methods. These are methods that take more than one parameter of a class type. Class types include sums and (possibly infinite) products type constructors. We study and compare two solutions for modeling generalized binary methods, which use purely covariant functors. In the first solution, which applies when we already have a class implementation, we reduce the behaviour of a generalized binary method to that of a bunch of unary methods. These are obtained by freezing the types of the extra class parameters to constant types. The bisimulation behavioural equivalence induced on objects by this model amounts to the greatest congruence w.r.t method application. Alternatively, we treat binary methods as graphs instead of functions, thus turning contravariant occurrences in the functor into covariant ones