[Python-ideas] Why is design-by-contracts not widely adopted?

[Steven D'Aprano]

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 :-)


> https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html 
> 
> 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.


> 1. Only a small sliver of human interactions are governed by formal 
> legal contracts read, understood, and agreed to by both (all) parties.

Irrelevant.


> 2. 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. 

Irrelevant. 

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.

Irrelevant.


> >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.

https://stackoverflow.com/questions/15125552/what-is-the-meaning-of-stable-and-unstable-for-various-sorting-algorithms?noredirect=1

https://stackoverflow.com/questions/1517793/what-is-stability-in-sorting-algorithms-and-why-is-it-important

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[0] to seq."
[...]
> But with duck-typing, no post condition is possible.

That's incorrect.

def append_first(seq):
    require:
        len(seq) > 0
        hasattr(seq, "append")
    ensure:
        len(seq) == len(OLD.seq) + 1
        seq[0] == 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.



-- 
Steve