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.
Eventually say more here with additional examples