Common use of (function contracts) Clause in Contracts

(function contracts). ‌ Following Findler and ▇▇▇▇▇▇▇▇▇’s work on contracts for higher-order functions [41], a function contract is built from zero or more contracts for the domain of a function (one contract per argument) and one contract for the range (return) of a function. We call a function contract delayed because asserting it to a value does not immediately signal a violation. Asserting the function contract amounts to asserting the domain contracts to the argument values and asserting the range contract to the return value of each call. A function contract applied to a non-function value will never signal a contract violation. For example, consider the function plus which first checks if both arguments are greater than 0 and second, depending on the result of this test, it either applies JavaScript’s native addition operator + to its arguments or it returns a string message. } Listing 4.10 Definition of function plus. As a running example we develop several contracts for plus. Our first contract restricts input and output to values of type "number".