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 <n...@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 <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) >> @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> >> 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/ >
_______________________________________________ Python-ideas mailing list Python-ideas@python.org https://mail.python.org/mailman/listinfo/python-ideas Code of Conduct: http://python.org/psf/codeofconduct/
