Inputs are contravariant….

Inputs are contravariant, outputs are covariant and input-outputs are invariant.”
Sounds erudite but what does it really mean. Well the concept is not new. My first introduction to the concept was from the VDM book by C.B.Jones where it is referred to as reification. Although this concept is not restricted to Object Oriented programming it has become better known in recent years (See Meilir Page-Jones “Fundamentals of Object Oriented Design in UML”, Chapter 11)
Here I will go back to model based program design for this discussion.
Consider an instance A of a data structure S. In the model based method S should have an invariant. Any method that modifies A must maintain the invariant relation. As an example, let S denote a sorted array. By definition, the invariant of a sorted array is that it is sorted. Now consider the following operations:
  • Add an element
  • Delete an Element
  • Check for existence of an element with a specific value.

Each of these methods must preserve the invariant. In addition each of these methods must satisfy a post condition. For instance the post condition of Delete will be that A will contain all elements it had before the call to Delete except for the element that must be deleted. If A contains duplicate items then the invariant must be restated to indicate that. Hence the post condition of Delete must state whether it will delete all elements that match a value or a specific one. The precondition can be that the element must exist if that is what is intended.
Notice we are dealing only with specification here. We are not dealing with implementation just yet. For a simple data structure like a sorted array the implementation can follow the specification exactly. In other cases the specification cannot be translated to an implementation easily. Hence we go through a process of reification.

Reification of specification

Consider a function F(S,I,O) where S is the model of the data structure, I is the set of inputs and O is the set of outputs. Here S is not the data structure per se. It is a model in that it is defined by the invariants and the set of operations defined on it. For instance S could refer to a stack and an the implementation of stack could be a linked list or a vector or even a binary tree.
Consider the implementation Fi of the specification F, or in object oriented terms F is an abstract method that must be implemented. The implementation Fi must satisfy the following requirements:

  • It must preserve the invariant
  • If the input I satisfies a pre-condition in the model that the implementation must accept that input
  • The output of the implementation must be at least as strong as that required by the model. If the output is required to satisfy a post condition in the model then the implementation must at satisfy that post condition. Eg. if the output is expected to be an integer greater than 0, the implementation can produce an output greater than 1, which is what is meant by stronger.

In object oriented terms the output object may be an instance of a class that inherits from the class specified in the abstraction of the method. The input set for the implementation may also be the derived class of the input set specified in the abstract method.
To summarise:
“Inputs are contravariant, outputs are covariant and input-output (the object itself ) is invariant.”


About The Sunday Programmer

Joe is an experienced C++/C# developer on Windows. Currently looking out for an opening in C/C++ on Windows or Linux.
This entry was posted in Software Engineering and tagged . Bookmark the permalink.

1 Response to Inputs are contravariant….

  1. It’s neary impossible to find knowledgeable people inn this particulasr subject,
    but you sound like yyou know whyat you’re talking about!

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s