The previous section illustrates an important point about the contract paradigm: contracts do not always need to completely specify the behavior of a method or system to be useful. For example, the absValue method contract did not completely specify the functional behavior (e.g., indicating given a negative value -v that the corresponding positive value v would be returned). It simply indicated that the result would be non-negative.

Note

Eventually say more here with additional examples