Contract metaphor for preconditions and postconditions [closed]

Question

English is not my primary language but I'm "forced" to write code and code's comments in English. I'm now trying to develop a PHP code (doesn't really matter this aspect) like this:

function divide($x, $y) {}

Which describes a function that divide $x / $y. Now I want to be able to add a comment related to that function listing few pre-conditions such as

@[A]: $x is an int
@[A]: $y is an int
@[A]: $y != 0

and a list of post-conditions (that are verified only if the pre-conditions are respected), such as:

@[B]: returns $x / $y

How should I call [A] and [B] using a contract metaphor?

Something like [A] = "law" and [B] = "assurance" (which is obliviously wrong). How should I better call them to make it appears that

If you follow all the [A]s I'll guarantee you that [B] will be verified.

?

Answer 1

I suggest stipulation and guarantee.

stipulation:

something stipulated; especially : a condition, requirement, or item specified in a legal instrument

guarantee

an assurance for the fulfillment of a condition: as

Answer 2

As noted in the Design-by-contract webpage mentioned in a comment, conditions on inputs are known as preconditions, and on outputs as postconditions. Of the former, wikipedia says:

A precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification. If a precondition is violated, the effect of the section of code becomes undefined and thus may or may not carry out its intended work.

and of postconditions it says

A postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification.

Edit: You could also use phrasings like "The caller agrees to ...", "If these stipulated conditions are met, the routine will...", "Given that ..., the routine is required to ...". You might also refer to the preconditions as "Requirements" or "Stipulations", and the postconditions as "Guarantees" or "Undertakings". Mix and match to similar effect. For example:

If the caller meets stipulations P,Q,R, the program undertakes to deliver X,Y,Z.
If the caller satisfies requirements P,Q,R, the program guarantees it will return X,Y,Z.