[Python-ideas] Transpiling contracts

[Ned Batchelder]

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>