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

[Brice Parent]

I've never used contracts, so excuse me if I didn't get how they would 
work, and what they should do.

The last example is about pre-post conditions in a class constructor. 
But I imagine this is not the only case where one would want to define 
contracts, like probably: within methods that return something and to 
functions (and in both cases, we'd want to contractually state some of 
the return's specificities).

Is the following function something someone used to work with contracts 
would write?

def calculate(first: int, second: int) -> float:
     def __require__():
         first > second
         second > 0
         # or first > second > 0 ?

     def __ensure__(ret):  # we automatically pass the return of the 
function to this one
         ret > 1

     return first / second

If so, having a reference to the function's output would probably be 
needed, as in the example above.

Also, wouldn't someone who use contracts want the type hints he provided 
to be ensured without having to add requirements like `type(first) is 
int` or something?

- Brice

Le 29/08/2018 à 07:52, Greg Ewing a écrit :
> Wes Turner wrote:
>>     I'm going to re-write that in a pseudo-Eiffel like syntax:
>
> Maybe some magic could be done to make this work:
>
>      def __init__(self, img: np.ndarray, x: int, y: int, width: int,
>              height: int) -> None:
>
>          def __require__():
>              x >= 0
>              y >= 0
>              width >= 0
>              height >= 0
>              x + width <= pqry.opencv.width_of(img)
>              y + height <= pqry.opencv.height_of(img)
>
>          def __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...
>