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 <jam...@gmail.com
<mailto:jam...@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.ris...@gmail.com <mailto:marko.ris...@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/
