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