[Python-ideas] Transpiling contracts

Tue Oct 2 11:05:25 EDT 2018

Hi Ned,

The idea is to polish a proof-of-concept library and then try to introduce
it into the standard libs eventually.

On Tue, 2 Oct 2018 at 16:57, Ned Batchelder <ned at nedbatchelder.com> wrote:

> I'm getting confused: is this still about an idea for Python, or
> development of a third-party library?
>
> --Ned.
>
> On 10/2/18 1:14 AM, Marko Ristin-Kaufmann wrote:
>
> 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
>>
>>
>>
>
> _______________________________________________
> Python-ideas mailing listPython-ideas at python.orghttps://mail.python.org/mailman/listinfo/python-ideas
> Code of Conduct: http://python.org/psf/codeofconduct/
>
>
> _______________________________________________
> Python-ideas mailing list
> Python-ideas at python.org
> https://mail.python.org/mailman/listinfo/python-ideas
> Code of Conduct: http://python.org/psf/codeofconduct/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.python.org/pipermail/python-ideas/attachments/20181002/82ee47ce/attachment-0001.html>