Object state invariance check between private methods execution

Question

In this reply to the question How to test private methods in C#? is referred to

The maximum that can be interesting is to have an object state invariance check between the execution of private methods.

What this verification is about and why it may be important?

Answer 1

Dbc

There is a secondary development paradigm called Design by Contract (Dbc). It can be used in any language, but some have their own syntax to facilitate. It is used to give more reliability to the code, to make it more explicit in the code how the code should interact at its tips.

As well as placing explicit type of variables in parameters, creating a contract that must be fulfilled, we can place other restrictions on how arguments should be passed to a method.

In general we use preconditions that verify what comes in the parameters in detail. The code should not compile or issue a programming error if some of the conditions have been breached in your call.

A little less used are the post-conditions that verify if the result generated by the method meets any condition, that is to say it answers what was expected.

Note that this ends up being part of the method contract. In some languages formally being part of the API, in others only as an additional check.

One can also use statements in the middle of the method to check in the middle of the algorithm whether everything is occurring correctly.

In some cases these checks can be turned off at runtime without prejudice. This gives more performance and can even reduce code size.

Invariance

Another check is whether the state of the object is always within certain established conditions. That is, the object variables must contain values in a specific way that keeps the object always valid. Usually this occurs at the end of some method that can change the state of any member of the instance or even of the type.

In other words, this state cannot be invalid. At least while the data can be accessed publicly.

Nothing prevents the status from being invalid during the execution of a method or even between various private methods, after private methods are implementation details. What you do internally doesn’t matter, everything is valid. When you finish something the state needs to be valid.

Private methods

In some cases one may want to prevent variance even between private methods. The text speaks of this.

Depending on the language it is even difficult to ensure public invariance without interfering in the private.

In general pre- and post-condition and invariance should be more than sufficient for private methods, as they are not part of the public API. In some cases it may be sufficient even for the public API, completely dispensing with the tests, in this type.

Completion

Dbc is something very useful to increase the quality of the code and avoid both testing while keeping a little more DRY since the specification is in the code.

Without it it either depends only on external testing or we’re in Umba-meu-boi, you trust that you or another will never make a change that compromises the object or result it should provide.

Of course, knowing how much to use it is almost an art. Some prefer the simple way to do everything, even when it may be more problematic, or the most common and simplest yet, not to check anything, after all she is Chuck Norris.

I wanted to see more of that in languages. C# has something like this, but it is half library gambiarra more external tool (Visual Studio), so few use. But want to put it in the language the right way.

It was even turned off in recent versions.

• Wikipedia article
• Wiki C2

Code example in Spec# which is a variation of C# developed by Microsoft Research.

public static int BinarySearch(int[]! a, int key)
    requires forall{int i in (0: a.Length), int j in (i: a.Length); a[i] <= a[j]};
    ensures 0 <= result ==> a[result] == key;
    ensures result < 0 ==> forall{int i in (0: a.Length); a[i] != key};
 {
     int low = 0;
     int high = a.Length - 1;
     while (low <= high)
         invariant high+1 <= a.Length;
         invariant forall{int i in (0: low); a[i] != key};
         invariant forall{int i in (high+1: a.Length); a[i] != key};
     {
         int mid = (low + high) / 2;
         int midVal = a[mid];
         if (midVal < key) {
             low = mid + 1;
         } else if (key < midVal) {
             high = mid - 1;
         } else {
             return mid; // key found
         }
    }
    return -(low + 1);  // key not found.
}

Note that there is invariance within the method, what it is seems to me is not the initial proposal of the Dbc, but that it is something that can be interesting in the place of the assertion.