Transpiling contracts
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
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@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
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@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@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
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@gmail.com <mailto:jamtlu@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@gmail.com <mailto:marko.ristin@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@python.org https://mail.python.org/mailman/listinfo/python-ideas Code of Conduct: http://python.org/psf/codeofconduct/
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@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@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@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@python.orghttps://mail.python.org/mailman/listinfo/python-ideas Code of Conduct: http://python.org/psf/codeofconduct/
_______________________________________________ Python-ideas mailing list Python-ideas@python.org https://mail.python.org/mailman/listinfo/python-ideas Code of Conduct: http://python.org/psf/codeofconduct/
On 10/2/2018 11:05 AM, Marko Ristin-Kaufmann wrote:
Hi Ned,
The idea is to polish a proof-of-concept library and then try to introduce it into the standard libs eventually.
I'd suggest taking this off-list until such a library is developed, then. But, if the library needs some hook provided by Python to make it work (or work better), then I think it's appropriate to discuss that on this list. Eric
participants (4)
-
Eric V. Smith -
James Lu -
Marko Ristin-Kaufmann -
Ned Batchelder