<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p>I'm getting confused: is this still about an idea for Python, or
      development of a third-party library?</p>
    <p>--Ned.<br>
    </p>
    <br>
    <div class="moz-cite-prefix">On 10/2/18 1:14 AM, Marko
      Ristin-Kaufmann wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAGu4bVA=qd0DZ_r=m5QPWqEKcNPBJGWuugyx1g6D12o3R_rQ2w@mail.gmail.com">
      <meta http-equiv="content-type" content="text/html; charset=utf-8">
      <div dir="ltr">
        <div dir="ltr">
          <div dir="ltr">
            <div dir="ltr">
              <div dir="ltr">
                <div dir="ltr">
                  <div dir="ltr">
                    <div dir="ltr">
                      <div dir="ltr">
                        <div>Hi James,<br>
                          <br>
                        </div>
                        I had another take at it. I wrote it down in the
                        github issue (<a
href="https://github.com/Parquery/icontract/issues/48#issuecomment-426147468"
                          moz-do-not-send="true">https://github.com/Parquery/icontract/issues/48#issuecomment-426147468</a>):<br>
                        <br>
                        <pre><span class="gmail-pl-c1">SLOW</span><span class="gmail-pl-k">=</span>os.environ.get(<span class="gmail-pl-s"><span class="gmail-pl-pds">"</span>SOME_ENVIRONMENT_VARIABLE<span class="gmail-pl-pds">"</span></span>, <span class="gmail-pl-s"><span class="gmail-pl-pds">"</span><span class="gmail-pl-pds">"</span></span>) <span class="gmail-pl-k">!=</span> <span class="gmail-pl-s"><span class="gmail-pl-pds">"</span><span class="gmail-pl-pds">"</span></span>

<span class="gmail-pl-k">class</span> <span class="gmail-pl-en">SomeClass</span>:
    <span class="gmail-pl-k">def</span> <span class="gmail-pl-c1">__init__</span>(<span class="gmail-pl-smi"><span class="gmail-pl-smi">self</span></span>)-><span class="gmail-pl-c1">None</span>:
        <span class="gmail-pl-c1">self</span>.some_prop <span class="gmail-pl-k">=</span> <span class="gmail-pl-c1">1984</span>

<span class="gmail-pl-k">def</span> <span class="gmail-pl-en">some_func</span>(<span class="gmail-pl-smi">arg1</span>: List[<span class="gmail-pl-c1">int</span>], <span class="gmail-pl-smi">arg2</span>: List[<span class="gmail-pl-c1">int</span>])->SomeClass:
    <span class="gmail-pl-k">with</span> requiring:
        <span class="gmail-pl-c1">len</span>(arg1) <span class="gmail-pl-k">></span> <span class="gmail-pl-c1">3</span>, <span class="gmail-pl-s"><span class="gmail-pl-pds">"</span>some description<span class="gmail-pl-pds">"</span></span>
        <span class="gmail-pl-c1">len</span>(arg2) <span class="gmail-pl-k">></span> <span class="gmail-pl-c1">5</span>, <span class="gmail-pl-c1">ValueError</span>(<span class="gmail-pl-s"><span class="gmail-pl-pds">"</span>some format <span class="gmail-pl-c1">{}</span> <span class="gmail-pl-c1">{}</span><span class="gmail-pl-pds">"</span></span>.format(arg1, arg2))

        <span class="gmail-pl-k">if</span> <span class="gmail-pl-c1">SLOW</span>:
            <span class="gmail-pl-c1">all</span>(elt <span class="gmail-pl-k">in</span> arg2 <span class="gmail-pl-k">for</span> elt <span class="gmail-pl-k">in</span> arg1)
            <span class="gmail-pl-c1">len</span>(arg2) <span class="gmail-pl-k">==</span> <span class="gmail-pl-c1">len</span>(<span class="gmail-pl-c1">set</span>(arg2))

    result <span class="gmail-pl-k">=</span> <span class="gmail-pl-c1">None</span>  <span class="gmail-pl-c"># <span class="gmail-pl-c">type:</span> <span class="gmail-pl-c">SomeClass</span></span>
    <span class="gmail-pl-k">with</span> ensuring, oldie <span class="gmail-pl-k">as</span> O:
        <span class="gmail-pl-c1">len</span>(arg1) <span class="gmail-pl-k">==</span> <span class="gmail-pl-c1">len</span>(O.arg1)
        result.some_prop <span class="gmail-pl-k"><</span> <span class="gmail-pl-c1">len</span>(arg2)</pre>
                        <div><br>
                        </div>
                        <div>This transpiles to/from:<br>
                          <br>
                          <div class="gmail-highlight
                            gmail-highlight-source-python">
                            <pre><span class="gmail-pl-c1">SLOW</span><span class="gmail-pl-k">=</span>os.environ.get(<span class="gmail-pl-s"><span class="gmail-pl-pds">"</span>SOME_ENVIRONMENT_VARIABLE<span class="gmail-pl-pds">"</span></span>, <span class="gmail-pl-s"><span class="gmail-pl-pds">"</span><span class="gmail-pl-pds">"</span></span>) <span class="gmail-pl-k">!=</span> <span class="gmail-pl-s"><span class="gmail-pl-pds">"</span><span class="gmail-pl-pds">"</span></span>

<span class="gmail-pl-k">class</span> <span class="gmail-pl-en">SomeClass</span>:
    <span class="gmail-pl-k">def</span> <span class="gmail-pl-c1">__init__</span>(<span class="gmail-pl-smi"><span class="gmail-pl-smi">self</span></span>)-><span class="gmail-pl-c1">None</span>:
        <span class="gmail-pl-c1">self</span>.some_prop <span class="gmail-pl-k">=</span> <span class="gmail-pl-c1">1984</span>

<span class="gmail-pl-en">@requires</span>(<span class="gmail-pl-k">lambda</span> <span class="gmail-pl-smi">P</span>: <span class="gmail-pl-c1">len</span>(P.arg1) <span class="gmail-pl-k">></span> <span class="gmail-pl-c1">3</span>, <span class="gmail-pl-s"><span class="gmail-pl-pds">"</span>some description<span class="gmail-pl-pds">"</span></span>)
<span class="gmail-pl-en">@requires</span>(<span class="gmail-pl-k">lambda</span> <span class="gmail-pl-smi">P</span>: <span class="gmail-pl-c1">len</span>(P.arg2),
          <span class="gmail-pl-v">error</span><span class="gmail-pl-k">=</span><span class="gmail-pl-k">lambda</span> <span class="gmail-pl-smi">P</span>: <span class="gmail-pl-c1">ValueError</span>(<span class="gmail-pl-s"><span class="gmail-pl-pds">"</span>some format <span class="gmail-pl-c1">{}</span> <span class="gmail-pl-c1">{}</span><span class="gmail-pl-pds">"</span></span>.format(P.arg1, P.arg2)))
<span class="gmail-pl-en">@requires</span>(<span class="gmail-pl-k">lambda</span> <span class="gmail-pl-smi">P</span>: <span class="gmail-pl-c1">all</span>(elt <span class="gmail-pl-k">in</span> P.arg2 <span class="gmail-pl-k">for</span> elt <span class="gmail-pl-k">in</span> P.arg1), <span class="gmail-pl-v">enabled</span><span class="gmail-pl-k">=</span><span class="gmail-pl-c1">SLOW</span>)
<span class="gmail-pl-en">@requires</span>(<span class="gmail-pl-k">lambda</span> <span class="gmail-pl-smi">P</span>: <span class="gmail-pl-c1">len</span>(arg2) <span class="gmail-pl-k">==</span> <span class="gmail-pl-c1">len</span>(<span class="gmail-pl-c1">set</span>(arg2)))
<span class="gmail-pl-en">@ensures</span>(<span class="gmail-pl-k">lambda</span> <span class="gmail-pl-smi">O</span>, <span class="gmail-pl-smi">P</span>: <span class="gmail-pl-c1">len</span>(P.arg1) <span class="gmail-pl-k">==</span> <span class="gmail-pl-c1">len</span>(O.arg1))
<span class="gmail-pl-en">@ensures</span>(<span class="gmail-pl-k">lambda</span> <span class="gmail-pl-smi">P</span>, <span class="gmail-pl-smi">result</span>: result.some_prop <span class="gmail-pl-k"><</span> <span class="gmail-pl-c1">len</span>(P.arg2))
<span class="gmail-pl-k">def</span> <span class="gmail-pl-en">some_func</span>(<span class="gmail-pl-smi">arg1</span>: List[<span class="gmail-pl-c1">int</span>], <span class="gmail-pl-smi">arg2</span>: List[<span class="gmail-pl-c1">int</span>])->SomeClass:
    <span class="gmail-pl-c1">...</span></pre>
                          </div>
                          <br>
                        </div>
                        <blockquote class="gmail_quote"
                          style="margin:0px 0px 0px
                          0.8ex;border-left:1px solid
                          rgb(204,204,204);padding-left:1ex">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? <br>
                        </blockquote>
                        <div>Actually no. The condition must be a single
                          statement (specified as a boolean expression)
                          regardless of the form (readable or
                          executable).<br>
                          <br>
                          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.<br>
                          <br>
                          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.<br>
                          <br>
                          <blockquote class="gmail_quote"
                            style="margin:0px 0px 0px
                            0.8ex;border-left:1px solid
                            rgb(204,204,204);padding-left:1ex">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)<br>
                          </blockquote>
                          <div><br>
                          </div>
                          <div>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 :)<br>
                            <br>
                            <blockquote class="gmail_quote"
                              style="margin:0px 0px 0px
                              0.8ex;border-left:1px solid
                              rgb(204,204,204);padding-left:1ex">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?<br>
                            </blockquote>
                             <br>
                          </div>
                          <div>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.<br>
                          </div>
                          <br>
                        </div>
                      </div>
                      <div>Cheers,<br>
                      </div>
                      <div>Marko<br>
                      </div>
                      <div dir="ltr"><br>
                        <br>
                      </div>
                    </div>
                  </div>
                </div>
              </div>
            </div>
          </div>
        </div>
      </div>
      <br>
      <div class="gmail_quote">
        <div dir="ltr">On Mon, 1 Oct 2018 at 17:18, James Lu <<a
            href="mailto:jamtlu@gmail.com" moz-do-not-send="true">jamtlu@gmail.com</a>>
          wrote:<br>
        </div>
        <blockquote class="gmail_quote" style="margin:0 0 0
          .8ex;border-left:1px #ccc solid;padding-left:1ex">
          <div 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=<a href="http://P.self.name"
                target="_blank" moz-do-not-send="true">P.self.name</a>)</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" target="_blank"
                  moz-do-not-send="true">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"><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>
          </div>
        </blockquote>
      </div>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <br>
      <pre wrap="">_______________________________________________
Python-ideas mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Python-ideas@python.org">Python-ideas@python.org</a>
<a class="moz-txt-link-freetext" href="https://mail.python.org/mailman/listinfo/python-ideas">https://mail.python.org/mailman/listinfo/python-ideas</a>
Code of Conduct: <a class="moz-txt-link-freetext" href="http://python.org/psf/codeofconduct/">http://python.org/psf/codeofconduct/</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>