Programming with Invariants

Computation is a process of unfolding the given problem over time.  It is the process of identifying if the problem is solvable or not. In more concrete terms, as we speak to computer science graduates, it the question of “Can you write an algorithm for the given problem?”

Algorithms play a central role in both the science and practice of computing. They are sequence of unambiguous instructions for solving a problem. Precisely, algorithm is a logical, arithmetical or computational procedure that if correctly applied ensures the solution of a problem. An algorithm has to be lucid, precise and unambiguous and give the correct solution in all cases. More importantly it has to terminate after a finite numbers of steps aka the finiteness property.

The algorithms we study concentrate on the space and time efficiency. Though we list several desirable properties of an algorithm like simplicity, correctness, unambiguous etc there is no formal method established to verify these properties. Primary concern of every algorithm designer has to be indeed verifying correctness; only then later to establish efficiency parameters. In this regard, programming with invariants is not a new paradigm but definitely the one every programmer needs to adapt.

Procedure:

1. Understand the problem.

2. Write few examples to verify your understanding.

3. Write the state space. State space is basically the domain of the problem. The type of data on which the processing is about to happen.

4. Identify the transition function which describes the various states the process can be in.

5. Write down the traces to authenticate the transition function

6. Identify the invariant. Invariant is property that proves the correctness of the algorithm. It is that one property that does not change in the algorithm.

 

Example:

1. Problem: 

Given a list, find the length of the list. The task is to identify how many elements are present in the list.

2. Examples:

3. State Space:

Input: List of integers

Output: Natural number with is the length of the list

List --> Natural

4. Transition Function:

5. Trace:

6. Invariant:

Observing the transition function and the trace we can conclude that the invariant for the process is:

1 + list-length (n-1)

Reasoning being at any point of iteration, we can use the invariant and find the length of the list! by the way, identifying a invariant is not an easy task. It comes by practice. I have just adapted the process into my coding routines!