On Sun, Oct 07, 2018 at 04:24:58PM -0400, Terry Reedy wrote:
A mathematical function is defined or specified by a input domain, output range, and a mapping from inputs to outputs. The mapping can be defined either by an explicit listing of input-output pairs or by a rule specifying either a) the process, what is done to inputs to produce outputs or, b) the result, how the output relates to the input.
Most code does not define pure mathematical functions, unless you're writing in Haskall :-)
defines contracts as "precise (legally unambiguous) specifications" (5.2 Business Contracting/Sub-contracting Metaphor)
You are quoting that out of context. The full context says (emphasis added):
IN THE BUSINESS WORLD, contracts are precise (legally unambiguous) specifications that define the obligations and benefits of the (usually two) parties involved.
and later goes on to say:
How does this apply to software correctness?
Consider the execution of a routine. The called routine provides a service - it is a supplier. The caller is the client that is requesting the service. We can impose a contract that spells out precisely the obligations and benefits of both the caller (client) and the callee (supplier). This contract SERVES AS THE INTERFACE SPECIFICATION FOR THE ROUTINE.
(I would add *executable* interface specification.)
It is not obvious to me that the metaphor of contracts adds anything worthwhile to the idea of 'function'.
It doesn't. That's not what the metaphor is for.
Design By Contract is not a redefinition of "function", it is a software methodology, a paradigm for helping programmers reason better about functions and specify the interface so that bugs are discovered earlier.
- Only a small sliver of human interactions are governed by formal
legal contracts read, understood, and agreed to by both (all) parties.
- The idealized definition is naive in practice. Most legal contracts,
unlike the example in the link article, are written in language that most people cannot read.
Dicts aren't actual paper books filled with definitions of words, floats don't actually float, neural nets are not made of neurons nor can you catch fish in them, and software contracts are code, not legally binding contracts. It is a *metaphor*.
Many contracts are imprecise and legally ambiguous, which is why we have contract dispute courts. And even then, the expense means that most people who feel violated in a transaction do not use courts.
Is this a critique of the legal system? What relevance does it have to Design By Contract?
Honestly Terry, you seem to be arguing:
"Hiring a lawyer is too expensive, and that's why Design By Contract doesn't work as a software methodology."
Post-conditions specify a function by result. I claim that this is not always sensible.
In this context, "result" can mean either "the value returned by the function" OR "the action performed by the function (its side-effect)".
Post-conditions can check both.
I said above that functions may be specified by process rather than result.
Fine. What of it? Can you describe what the function does?
"It sorts the list in place."
"It deletes the given record from the database."
"It deducts the given amount from Account A and transfers it to Account B, guaranteeing that either both transactions occur or neither of them, but never one and not the other."
These are all post-conditions. Write them as code, and they are contracts. If you can't write them as code, okay, move on to the next function.
(By the way, since you started off talking about mathematical functions, functions which perform a process rather than return a result aren't mathematical functions.)
Ironically, the contract metaphor reinforces my claim. Many contracts, such as in teaching and medicine, only specify process and explicitly disclaim any particular result of concern to the client.
b)//If you write contracts in text, they will become stale over time
Not true for good docstrings. We very seldom change the essential meaning of public functions.
What about public functions while they are still under active development with an unstable interface?
How has "Return the sine of x (measured in radians).", for math.sin, become stale? Why would it ever?
Of course a stable function with a fixed API is unlikely to change. What's your point? The sin() function implementation on many platforms probably hasn't changed in 10 or even 20 years. (It probably just calls the hardware routines.) Should we conclude that unit testing is therefore bunk and nobody needs to write unit tests?
What formal executable post condition would help someone who does not understand 'sine', or 'sine of x'?
Does x have to be a float? A number? (Decimal, Fraction, int, complex?)
What if x is an INF or NAN?
Can sin(x) return -0.0 rather than 0.0?
Let's consider some related functions...
Will tan(x) ever return NAN or INF?
What does sqrt(x) do if x is negative? Will it raise?
What are the possible valid arguments for the three-value form of pow(a, b, c)?
Or consider "Stable sort *IN PLACE*." for list.sort. A formal executable post-condition for this *can* be written. But for someone who understands the words 'stable', 'sort', and 'in place', this compact English post condition is much more readable than any formal version could be.
Not everybody knows what those terms mean.
And even if they can read the comment, it is a comment, and therefore a lie until proven different.
Post-conditions can be checked. Comments can't.
More over, that addition of 'stable', when we were ready to do so, did not make "Sort *IN PLACE*" stale in any sense of being wrong.
I don't understand what point you think you are making here. It is still stale -- the documentation is incomplete. Whether that is "wrong" or merely "stale" is a matter of how fine a line we wish to draw.
(Is a *partially* true but incomplete statement right, or wrong?)
I said above that functions definitions and contracts can specify the process rather than the result. For functions, the code is the process, and the code may then be the specification and the contract. For instance,
def append_first(seq): "Append seq to seq."
But with duck-typing, no post condition is possible.
def append_first(seq): require: len(seq) > 0 hasattr(seq, "append") ensure: len(seq) == len(OLD.seq) + 1 seq == seq[-1]
Nothing in the above requires seq to be a specific type. It just needs to support the len, append and getitem interfaces.
If one wanted to be *really* pedantic, we could add a O(N) check as well, requiring only slicing and equality:
seq[0:-1] == OLD.seq
but just because we CAN write a condition, doesn't mean we MUST write the condition. You still get to choose whether to check that as a contract, or a test, or both, or neither.