Given a contract like nat32
, we can define contracts that are more restrictive:
var positive32 = function (n) { nat32(n); if (n === 0) { throw new TypeError('Expected a ' + 'strictly positive integer.'); } return n; }
The set of values that pass the positive32
contract is a subset of the values that pass the nat32
contract. A subcontract S
of a contract C
is a contract such that if a value v
passes S
, then it also passes C
. The contract positive32
is therefore a subcontract of nat32
.
For any contract C
, there is a category whose objects are all the subcontracts of C
and whose morphisms are injections. This is a subcategory (defined in the obvious way) of the category of all contracts and injections between them.