<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body dir="auto">Hi Marko,<br><br>I’m going to refer to the transpiler syntax as “block syntax.”<div><br></div><div>1. How does Eiffel do formal contracts?</div><div>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? </div><div>2. If the last proposition is true, how often do we need multiple statements to test or specify a single contract condition?</div><div>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)</div><div>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?</div><div><br></div><div>I think we should answer questions two and three by looking at real code.</div><div>—</div><div><br></div><div>If MockP is supported, it could be used for all the contract decorators:</div><div>@snapshot(var=P.self.name)</div><div>@post(var=R.attr == P.old.var)</div><div><br></div><div>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.</div><div><br></div><div>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. </div><div><br><div dir="ltr">James Lu</div><div dir="ltr"><br>On Oct 1, 2018, at 1:01 AM, Marko Ristin-Kaufmann <<a href="mailto:marko.ristin@gmail.com">marko.ristin@gmail.com</a>> wrote:<br><br></div><blockquote type="cite"><div dir="ltr"><div dir="auto"><div><div class="gmail_quote"><div dir="ltr">Hi James,</div><div dir="ltr"><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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?<br>
<br>
Would<br>
<br>
with requiring: assert arg1 < arg2, “message”<br>
<br>
Be the code you type or the code that’s actually run?<br></blockquote></div></div><div dir="auto"><br></div><div dir="auto">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).</div><div dir="auto"><br></div><div dir="auto">You would read/write this:</div><div dir="auto">def some_func(arg1: List[int])->int:</div><div dir="auto"> with requiring:</div><div dir="auto"> assert len(arg1) > 3, "some description"</div><div dir="auto"><br></div><div dir="auto"> with oldie as O, resultie as result, ensuring:</div><div dir="auto"> if SLOW:</div><div dir="auto"> O.var1 = sum(arg1)</div><div dir="auto"> assert result > sum(arg1) > O.var1</div><div dir="auto"><br></div><div dir="auto"> assert len(result) > 5</div><div dir="auto"><br></div><div dir="auto">This would run:</div><div dir="auto">@requires(lambda P: len(P.arg1) > 3, "some description")</div><div dir="auto">@snapshot(lambda P, var1: sum(P.arg1), enabled=SLOW)</div><div dir="auto">@ensures(lambda O, P, result: result > sum(arg1) > O.var1, enabled=SLOW)</div><div dir="auto">@ensures(lambda result: len(result) > 5)</div><div dir="auto"><br></div><div dir="auto">I omitted in the example how to specify a custom exception to avoid confusion.</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto">Cheers,</div><div dir="auto">Marko</div><div dir="auto"> </div><div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote></div></div><div dir="auto"><br></div><div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
</blockquote></div></div></div>
</div></blockquote></div></body></html>