[Python-ideas] Transpiling contracts

Tue Oct 2 01:14:39 EDT 2018

Hi James,

I had another take at it. I wrote it down in the github issue (
https://github.com/Parquery/icontract/issues/48#issuecomment-426147468):

SLOW=os.environ.get("SOME_ENVIRONMENT_VARIABLE", "") != ""
class SomeClass:
    def __init__(self)->None:
        self.some_prop = 1984
def some_func(arg1: List[int], arg2: List[int])->SomeClass:
    with requiring:
        len(arg1) > 3, "some description"
        len(arg2) > 5, ValueError("some format {} {}".format(arg1, arg2))

        if SLOW:
            all(elt in arg2 for elt in arg1)
            len(arg2) == len(set(arg2))

    result = None  # type: SomeClass
    with ensuring, oldie as O:
        len(arg1) == len(O.arg1)
        result.some_prop < len(arg2)

This transpiles to/from:

SLOW=os.environ.get("SOME_ENVIRONMENT_VARIABLE", "") != ""
class SomeClass:
    def __init__(self)->None:
        self.some_prop = 1984
@requires(lambda P: len(P.arg1) > 3, "some
description")@requires(lambda P: len(P.arg2),
          error=lambda P: ValueError("some format {}
{}".format(P.arg1, P.arg2)))@requires(lambda P: all(elt in P.arg2 for
elt in P.arg1), enabled=SLOW)@requires(lambda P: len(arg2) ==
len(set(arg2)))@ensures(lambda O, P: len(P.arg1) ==
len(O.arg1))@ensures(lambda P, result: result.some_prop <
len(P.arg2))def some_func(arg1: List[int], arg2:
List[int])->SomeClass:
    ...

2. What’s the use case for preferring block syntax over lambda syntax? Is
> the block syntax only better when multiple statements are needed to test a
> single contract condition?
>
Actually no. The condition must be a single statement (specified as a
boolean expression) regardless of the form (readable or executable).

My idea was that contracts would be a more readable + easier to type and
group by the respective enabled flags. It should be a 1-to-1 back and forth
transformation. I didn't aim for any other advantages other than
readability/easier modification.

The use case I have in mind is not to separate each file into two
(executable and readable). I'm more thinking of a tool that I can attach to
key shortcuts in the IDE that let me quickly transform the contracts into
readable form when I need to read them / make my modifications and then
convert them back into executable form.

3. When we do need multiple statements to formally verify/specify, is it
> usually a better idea to factor out major functionality of the contract
> testing to an external function? (So other contracts can use the same
> external function and the intent of the contract is clear trough the
> function name)
>

I would say so (i.e. no multi-statement conditions) . Making
multi-statement conditions would be rather confusing and also harder to put
into documentation. And it would be hard to implement :)

4. If this is true, is it a good idea to include a contracts/ folder at the
> same folder level or a .contracts.py file to list “helper” or verification
> functions for a contract?
>

So far, we never had to make a function external to a contract -- it was
often the signal that something had to be refactored out of the function if
the condition became complex, but the resulting functions usually either
stayed in the same file or were more general and had to move to a separate
module anyhow. Our Python code base has about 95K LOC, I don't know how
contracts behave on larger code bases or how they would need to be
structured.

Cheers,
Marko

On Mon, 1 Oct 2018 at 17:18, James Lu <jamtlu at gmail.com> wrote:

> Hi Marko,
>
> I’m going to refer to the transpiler syntax as “block syntax.”
>
> 1. How does Eiffel do formal contracts?
> 2. What’s the use case for preferring block syntax over lambda syntax? Is
> the block syntax only better when multiple statements are needed to test a
> single contract condition?
> 2. If the last proposition is true, how often do we need multiple
> statements to test or specify a single contract condition?
> 3. When we do need multiple statements to formally verify/specify, is it
> usually a better idea to factor out major functionality of the contract
> testing to an external function? (So other contracts can use the same
> external function and the intent of the contract is clear trough the
> function name)
> 4. If this is true, is it a good idea to include a contracts/ folder at
> the same folder level or a .contracts.py file to list “helper” or
> verification functions for a contract?
>
> I think we should answer questions two and three by looking at real code.
> —
>
> If MockP is supported, it could be used for all the contract decorators:
> @snapshot(var=P.self.name)
> @post(var=R.attr == P.old.var)
>
> The decorator can also check the type of the returned object, and if it’s
> MockP it will use MockP protocol and otherwise it will check the object is
> callable and treat it as a lambda.
>
> Your approach has better type hinting, but I’m not sure if type hinting
> would be that useful if you’re adding a contract whilst writing the
> function.
>
> James Lu
>
> On Oct 1, 2018, at 1:01 AM, Marko Ristin-Kaufmann <marko.ristin at gmail.com>
> wrote:
>
> Hi James,
>
> Regarding the “transpile into Python” syntax with with statements: Can I
>> see an example of this syntax when used in pathlib? I’m a bit worried this
>> syntax is too long and “in the way”, unlike decorators which are before the
>> function body. Or do you mean that both MockP and your syntax should be
>> supported?
>>
>> Would
>>
>> with requiring: assert arg1 < arg2, “message”
>>
>> Be the code you type or the code that’s actually run?
>>
>
> That's the code you would type. Let me make a full example (I'm omitting
> "with contracts" since we actually don't need it).
>
> You would read/write this:
> def some_func(arg1: List[int])->int:
>   with requiring:
>     assert len(arg1) > 3, "some description"
>
>   with oldie as O, resultie as result, ensuring:
>     if SLOW:
>       O.var1 = sum(arg1)
>       assert result > sum(arg1) > O.var1
>
>     assert len(result) > 5
>
> This would run:
> @requires(lambda P: len(P.arg1) > 3, "some description")
> @snapshot(lambda P, var1: sum(P.arg1), enabled=SLOW)
> @ensures(lambda O, P, result: result > sum(arg1) > O.var1, enabled=SLOW)
> @ensures(lambda result: len(result) > 5)
>
> I omitted in the example how to specify a custom exception to avoid
> confusion.
>
> If we decide that transpiler is the way to go, I'd say it's easier to just
> stick with lambdas and allow no mock-based approach in transpilation.
>
> Cheers,
> Marko
>
>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.python.org/pipermail/python-ideas/attachments/20181002/a9f35025/attachment.html>