False myth: Abstract interpretation can only do "easy" properties as nonnull

When demoing the CodeContracts static checker, often people ask me what's underneath. I tell them that is based on abstract interpretation, a theory developed in the late 70s by two French computer scientists, Patrick and Radhia Cousot. According to abstract interpretation, concrete program executions can be observed at different abstraction levels (called abstract semantics). A static analysis is just an abstract semantics which is coarse enough to be computable (and fast!), and precise enough to be useful.

For instance in the program below, instead of considering all the possible input arrays - there are (almost) infinitely many -  cccheck only considers an abstraction of them.

 public int Max(int[] arr)
{
 Contract.Requires(arr != null);
 Contract.Requires(arr.Length > 0);

 var max = arr[0];
 for(var i = 1; i < arr.Length; i++)
 {
 if (max < arr[i]) max = arr[i];
 }

 return max;
}

Now the question is which abstraction of the array we should keep?

A very simple abstraction is whether the input array is null or not. This help us to prove the absence of null pointer exceptions – i.e., in the example, all the array loads are safe.

A more refined abstraction keeps track of the array indexes. In our example, the local variable i is initialized to 1 and always incremented. Therefore we can infer that it always assume values in the interval [1, Int32.MaxValue]. Furthermore, inside the body of the loop we also know that i < arr.Length. As a consequence, we can deduce that is safe to index the array with i, i.e., no out-of-bounds exception is ever thrown, no matter which is the concrete array.

A false myth is that abstract interpretation is good only for those “simple” properties, and for “real” verification we need some other technique, as for instance deductive verification. For instance, in the example below the myth goes as abstract interpretation is unable to infer that Max is effectively computing the max of the array. Let’s debunk the myth.  We can ask cccheck to tell us which postcondition infers for our program (we use the extra option “-suggest methodensures”):

…: message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.ForAll(0, arr.Length, __k__ => arr[__k__] <= Contract.Result<int>()));

…: message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Exists(0, arr.Length, __j__ => arr[__j__] == Contract.Result<int>())); 

The analyzer infers that the returned value is larger or equal to all the elements in the array and that there exists one element in the array that is equal to the returned value, i.e, and the returned value is effectively the maximum element and not a simple upper bound!

To sum up, let me illustrate why we use abstract interpretation and not, e.g., deductive verification in CodeContracts. Using deductive verification, i.e., Hoare-Logic style reasoning, one should provide all the boundary contracts and the loop invariants. Our Max will then look like as this one:

 public int Max(int[] arr){

  Contract.Requires(arr != null); 
 Contract.Requires(arr.Length > 0); 
 Contract.Ensures(Contract.ForAll(arr, el => el <= Contract.Result<int>())); 
 Contract.Ensures(Contract.Exists(arr, el => el == Contract.Result<int>())); 

 var max = arr[0];
 for(var i = 1; i < arr.Length; i++)
 { // Those below are effectively Loop invariants, CC has no Contract.Invariant(...)
 Contract.Assert(i >= 1);  
 Contract.Assert(Contract.ForAll(0, i, __j__ => arr[__j__] <= max));  
 Contract.Assert(Contract.Exists(0, i, __j__ => arr[__j__] == max)); 

 if (max < arr[i]) max = arr[i];
 }

 return max;
}

Compare it with cccheck, which infers, precondition, postcondition, and loop invariants!

 public int Max(int[] arr)
{ // Precondition & postcondition inferred   
 

  var max = arr[0];
 for(var i = 1; i < arr.Length; i++)
 { // Loop invariant inferred
 if (max < arr[i]) max = arr[i];
 }

 return max;
}

…: message : CodeContracts: Suggested requires: Contract.Requires(arr != null);

…: message : CodeContracts: Suggested requires: Contract.Requires(0 < arr.Length);

…: message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.ForAll(0, arr.Length, __k__ => arr[__k__] <= Contract.Result<System.Int32>()));

…: message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.Exists(0, arr.Length, __j__ => arr[__j__] == Contract.Result<System.Int32>()));