Omitting Sections of a Method Contract
Sections of a method contract may be omitted. The following abstract
value example abs
does not include a pre-condition since it does
not need to make any assumptions about its inputs (i.e., it “works”
for all possible inputs of the argument type). And, since the the
method does not modify a non-local variable, the modifies
section
can be omitted::
def absValue(y: Z): Z = {
Contract(
Ensures(Res >= 0)
)
var ans: Z = 0
if (x < 0) {
ans = -y
} else {
ans = y
}
return ans
}
Omitting a pre-condition is semantically equivalent to stating that
the pre-condition is always satisfied, no matter how the method is
called. To emphasize this point, one can explicitly include a
Requires
clause with a body T
::
Contract(
Requires(T),
Ensures(Res >= 0)
)
A trivial Modifies
clause (one with no entries) can also be
included if one wishes to make a visually explicit indication that
“nothing” is modified::
Contract(
Requires(T),
Modifies(),
Ensures(Res >= 0)
)
Post-conditions can also be omitted. This is common early on in the development process where one is prototyping and only using contracts to indicate situations where bad inputs could cause problems like run-time exceptions or where the input domain for which the method is defined is limited. For example, one might want to rule out negative inputs for a square root or factorial function without saying anything about the result::
def factorial(y : Z): Z = {
Contract(
Requires(y >= 0)
)
...
}
In such situations, the service contract is making no “promises” to clients about what the service will do. However, it is still provides valuable information by indicating that the function is only defined for non-negative values.