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 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/