Invariants

Let's discuss the concept of an invariant. What is an invariant? It is a condition that always holds. For example, refer to the following code:

scala> val arr = Array.fill[Int](5)(-1) 
arr: Array[Int] = Array(-1, -1, -1, -1, -1) 
 
scala> for(i <- 0 to 4) { 
     |   arr(i) = 0 
     | } 

To comprehend the preceding code, the following statements are always true:

• At the start of each iteration, elements at indices 0 to i-1 are zero

• After each iteration of the loop, elements 0 to i are zero

This is called a loop invariant. We can reason the code using invariants.

Another example of an invariant for a singly linked list is that every list node gets pointed at by one, and only one pointer. In other words, two adjacent pointers will never point to the same node.

Invariants can be relaxed temporarily and then restored. For example, consider the imperative version of the list node insertion algorithm:

       q <- new node 
       p <- node...