[Python-ideas] Transpiling contracts
Ned Batchelder
ned at nedbatchelder.com
Tue Oct 2 10:54:51 EDT 2018
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(eltin arg2for eltin arg1)
> len(arg2)== len(set(arg2))
>
> result= None # type: SomeClass
> with ensuring, oldieas 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(eltin P.arg2for eltin 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
> <mailto: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 <http://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 <mailto: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 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/a4ab7134/attachment-0001.html>
More information about the Python-ideas
mailing list