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 code more reliability, to make code more explicit as code should interact at its ends.

As with putting explicit type of variables into parameters, creating a contract that must be followed, we can place other constraints on how arguments should be passed to a method.

In general, you use preconditions that check what comes in the parameters in detail. The code should not compile or issue a programming error if some of the conditions were violated in your call.

A little less used are the postconditions that verify if the result generated by the method meets some condition, ie it responds to 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 just as an additional check.

You can also use assertions in the middle of the method to check in the middle of the algorithm if everything is happening correctly.

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

Invariance

Another check is whether the object's state is always within certain set conditions. That is, 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 some instance member or even type.

In other words this state can not vary invalidly. At least as long as the data can be accessed publicly.

Nothing prevents the state from being invalid during the execution of a method or even between several private methods, after all private methods are implementation details. What is done internally does not matter, everything is valid. When it finishes something, the state must be valid.

Private methods

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

Depending on the language, it is even difficult to guarantee public invariance without interfering with the private.

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

Conclusion

DbC is very useful for increasing code quality and avoiding both testing, while maintaining a little more DRY since the specification is in the code.

Without this or it depends only on external tests or we stay in bumba-meu-boi , you trust that you or another will never make a change that compromises the object or result that it should provide. p>

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

I wanted to see this more in languages. C # has something like that , but it's kind of more library gambiarra tool external (Visual Studio), then few use. But they want it in the right language.

• Wikipedia article
• Wiki C2

Code sample in #

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 inside the method, which seems to me not to be the initial proposal of DbC, but something that might be interesting in place of the assertion.