Re: [Python-ideas] Transpiling contracts
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 ___ Python-ideas mailing list Python-ideas@python.org https://mail.python.org/mailman/listinfo/python-ideas Code of Conduct: http://python.org/psf/codeofconduct/
Re: [Python-ideas] Transpiling contracts
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 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 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
Re: [Python-ideas] Transpiling contracts
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 > 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
Re: [Python-ideas] Transpiling contracts
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 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,
Re: [Python-ideas] Transpiling contracts
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 > 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/
[Python-ideas] 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 > ___ Python-ideas mailing list Python-ideas@python.org https://mail.python.org/mailman/listinfo/python-ideas Code of Conduct: http://python.org/psf/codeofconduct/
