[Python-ideas] Pre-conditions and post-conditions

[Steven D'Aprano]

On Tue, Aug 28, 2018 at 07:46:02AM +0200, Marko Ristin-Kaufmann wrote:
> Hi,
> To clarify the benefits of the contracts, let me give you an example from
> our code base:
> 
> @icontract.pre(lambda x: x >= 0)
> @icontract.pre(lambda y: y >= 0)
> @icontract.pre(lambda width: width >= 0)
> @icontract.pre(lambda height: height >= 0)
> @icontract.pre(lambda x, width, img: x + width <= pqry.opencv.width_of(img))
> @icontract.pre(lambda y, height, img: y + height <= pqry.opencv.height_of(img))
> @icontract.post(lambda self: (self.x, self.y) in self)
> @icontract.post(lambda self: (self.x + self.width - 1, self.y +
> self.height - 1) in self)
> @icontract.post(lambda self: (self.x + self.width, self.y +
> self.height) not in self)
> def __init__(self, img: np.ndarray, x: int, y: int, width: int,
> height: int) -> None:


Thanks for your example Marko. I think that is quite close to the 
ugliest piece of Python code I've ever seen, and I don't mean that as a 
criticism of you for writing it or the icontract library's design.

We write code that our language allows us to write, not the code we want 
to write. Python has not been designed for contracts, and it shows.

I think this demonstrates a truth about programming languages:

    Aethestics matter. Syntax matters.

Some features, no matter how useful and beneficial, have no hope at all 
of getting widespread use if the syntax is awkward or the result ugly. I 
think that contracts will be doomed to be a minor niche used only by 
really keen proponents of the style so long as the best way to write a 
contract is to use a sequence of decorator calls with lambdas.

I'm going to re-write that in a pseudo-Eiffel like syntax:

def __init__(self, img: np.ndarray, x: int, y: int, width: int, height: int) -> None:
    require:
        x >= 0
        y >= 0
        width >= 0
        height >= 0
        x + width <= pqry.opencv.width_of(img)
        y + height <= pqry.opencv.height_of(img)

    # possibly this should be an invariant, not a post-condition?
    ensure:
        (self.x, self.y) in self
        (self.x + self.width - 1, self.y + self.height - 1) in self
        (self.x + self.width, self.y + self.height) not in self

    # body of __init__ goes here...


This makes a huge difference to readability:

- block structure to give visual shape to the code;

- related code stays together (all the pre-conditions naturally go
  into the require block, post-conditions in the ensure block, and
  no chance of interleaving them

    @pre(...)
    @post(...)
    @pre(...)

- no extraneous lambdas (they are pure noise);

- no long sequence of decorators (more than one of each is pure noise);

- possibility to write assertions which take more than one statement.



-- 
Steve