<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Hi,<br><br>(I'd like to fork from a previous thread, "Pre-conditions and
post-conditions", since it got long and we started discussing a couple
of different things. Let's discuss in this thread the implementation of a library for design-by-contract and how to push it forward to hopefully add it to the standard library one day.)<br><br></div><div>For those unfamiliar with contracts and current state of the discussion in the previous thread, here's a short summary. The discussion started by me inquiring about the possibility to add design-by-contract concepts into the core language. The idea was rejected by the participants mainly because they thought that the merit of the feature does not merit its costs. This is quite debatable and seems to reflect many a discussion about design-by-contract in general. Please see the other thread, "Why is design-by-contract not widely adopted?" if you are interested in that debate.<br><br></div><div>We (a colleague of mine and I) decided to implement a library to bring design-by-contract to Python since we don't believe that the concept will make it into the core language anytime soon and we needed badly a tool to facilitate our work with a growing code base. <br><br>The library is available at <a href="http://github.com/Parquery/icontract">http://github.com/Parquery/icontract</a>. The hope is to polish it so that the wider community could use it and once the quality is high enough, make a proposal to add it to the standard Python libraries. We do need a standard library for contracts, otherwise projects with <i>conflicting</i> contract libraries can not integrate<i> </i>(<i>e.g., </i>the contracts can not be inherited between two different contract libraries).<br><br></div><div>So far, the most important bits have been implemented in icontract:<br><ul><li>Preconditions, postconditions, class invariants</li><li>Inheritance of the contracts (including strengthening and weakening of the inherited contracts)</li><li>Informative violation messages (including information about the values involved in the contract condition)</li><li>Sphinx extension to include contracts in the automatically generated documentation (sphinx-icontract)<br></li><li>Linter to statically check that the arguments of the conditions are correct (pyicontract-lint)<br></li></ul><p>We are successfully using it in our code base and have been quite happy about the implementation so far.</p><p>There is one bit still missing: accessing "old" values in the postcondition (<i>i.e., </i>shallow copies of the values prior to the execution of the function). This feature is necessary in order to allow us to verify state transitions.</p><p>For example, consider a new dictionary class that has "get" and "put" methods:</p><pre style="background-color:rgb(255,255,255);color:rgb(0,0,0);font-family:"DejaVu Sans Mono";font-size:10.5pt"><font size="2"><span style="color:rgb(0,0,128);font-weight:bold">from </span>typing <span style="color:rgb(0,0,128);font-weight:bold">import </span>Optional<br><br><span style="color:rgb(0,0,128);font-weight:bold">from </span>icontract <span style="color:rgb(0,0,128);font-weight:bold">import </span>post<br><br><span style="color:rgb(0,0,128);font-weight:bold">class </span>NovelDict:<br> <span style="color:rgb(0,0,128);font-weight:bold">def </span>length(<span style="color:rgb(148,85,141)">self</span>)-><span style="color:rgb(0,0,128)">int</span>:<br> ...<br><br> <span style="color:rgb(0,0,128);font-weight:bold">def </span>get(<span style="color:rgb(148,85,141)">self</span>, key: <span style="color:rgb(0,0,128)">str</span>) -> Optional[<span style="color:rgb(0,0,128)">str</span>]:<br> ...<br><br> <span style="color:rgb(0,0,178)">@post</span>(<span style="color:rgb(0,0,128);font-weight:bold">lambda </span>self, key, value: <span style="color:rgb(148,85,141)">self</span>.get(key) == value)<br> <span style="color:rgb(0,0,178)">@post</span>(<span style="color:rgb(0,0,128);font-weight:bold">lambda </span>self, key: old(<span style="color:rgb(148,85,141)">self</span>.get(key)) <span style="color:rgb(0,0,128);font-weight:bold">is None and </span>old(<span style="color:rgb(148,85,141)">self</span>.length()) + <span style="color:rgb(0,0,255)">1 </span>== <span style="color:rgb(148,85,141)">self</span>.length(),<br> <span style="color:rgb(0,128,128);font-weight:bold">"length increased with a new key"</span>)<br> <span style="color:rgb(0,0,178)">@post</span>(<span style="color:rgb(0,0,128);font-weight:bold">lambda </span>self, key: old(<span style="color:rgb(148,85,141)">self</span>.get(key)) <span style="color:rgb(0,0,128);font-weight:bold">is not None and </span>old(<span style="color:rgb(148,85,141)">self</span>.length()) == <span style="color:rgb(148,85,141)">self</span>.length(),<br> <span style="color:rgb(0,128,128);font-weight:bold">"length stable with an existing key"</span>)<br> <span style="color:rgb(0,0,128);font-weight:bold">def </span>put(<span style="color:rgb(148,85,141)">self</span>, key: <span style="color:rgb(0,0,128)">str</span>, value: <span style="color:rgb(0,0,128)">str</span>) -> <span style="color:rgb(0,0,128);font-weight:bold">None</span>:<br> ...</font><br></pre><p>How could we possible implement this "old" function? <br></p><p>Here is my suggestion. I'd introduce a decorator "before" that would allow you to store whatever values in a dictionary object "old" (<i>i.e. </i>an object whose properties correspond to the key/value pairs). The "old" is then passed to the condition. Here is it in code:</p><pre style="background-color:rgb(255,255,255);color:rgb(0,0,0);font-family:"DejaVu Sans Mono";font-size:10.5pt"><font size="2"><span style="color:rgb(128,128,128);font-style:italic"># omitted contracts for brevity<br></span><span style="color:rgb(0,0,128);font-weight:bold">class </span>NovelDict:<br> <span style="color:rgb(0,0,128);font-weight:bold">def </span>length(<span style="color:rgb(148,85,141)">self</span>)-><span style="color:rgb(0,0,128)">int</span>:<br> ...<br><br> <span style="color:rgb(128,128,128);font-style:italic"># omitted contracts for brevity<br></span><span style="color:rgb(128,128,128);font-style:italic"> </span><span style="color:rgb(0,0,128);font-weight:bold">def </span>get(<span style="color:rgb(148,85,141)">self</span>, key: <span style="color:rgb(0,0,128)">str</span>) -> Optional[<span style="color:rgb(0,0,128)">str</span>]:<br> ...<br><br> <span style="color:rgb(0,0,178)">@before</span>(<span style="color:rgb(0,0,128);font-weight:bold">lambda </span>self, key: {<span style="color:rgb(0,128,128);font-weight:bold">"length"</span>: <span style="color:rgb(148,85,141)">self</span>.length(), <span style="color:rgb(0,128,128);font-weight:bold">"get"</span>: <span style="color:rgb(148,85,141)">self</span>.get(key)})<br> <span style="color:rgb(0,0,178)">@post</span>(<span style="color:rgb(0,0,128);font-weight:bold">lambda </span>self, key, value: <span style="color:rgb(148,85,141)">self</span>.get(key) == value)<br> <span style="color:rgb(0,0,178)">@post</span>(<span style="color:rgb(0,0,128);font-weight:bold">lambda </span>self, key, old: old.get <span style="color:rgb(0,0,128);font-weight:bold">is None and </span>old.length + <span style="color:rgb(0,0,255)">1 </span>== <span style="color:rgb(148,85,141)">self</span>.length(),<br> <span style="color:rgb(0,128,128);font-weight:bold">"length increased with a new key"</span>)<br> <span style="color:rgb(0,0,178)">@post</span>(<span style="color:rgb(0,0,128);font-weight:bold">lambda </span>self, key, old: old.get <span style="color:rgb(0,0,128);font-weight:bold">is not None and </span>old.length == <span style="color:rgb(148,85,141)">self</span>.length(),<br> <span style="color:rgb(0,128,128);font-weight:bold">"length stable with an existing key"</span>)<br> <span style="color:rgb(0,0,128);font-weight:bold">def </span>put(<span style="color:rgb(148,85,141)">self</span>, key: <span style="color:rgb(0,0,128)">str</span>, value: <span style="color:rgb(0,0,128)">str</span>) -> <span style="color:rgb(0,0,128);font-weight:bold">None</span>:<br> ...</font><br></pre><p>The linter would statically check that all attributes accessed in "old" have to be defined in the decorator "before" so that attribute errors would be caught early. The current implementation of the linter is fast enough to be run at save time so such errors should usually not happen with a properly set IDE.</p><p>"before" decorator would also have "enabled" property, so that you can turn it off (<i>e.g., </i>if you only want to run a postcondition in testing). The "before" decorators can be stacked so that you can also have a more fine-grained control when each one of them is running (some during test, some during test and in production). The linter would enforce that before's "enabled" is a disjunction of all the "enabled"'s of the corresponding postconditions where the old value appears.<br></p><p>Is this a sane approach to "old" values? Any alternative approach you would prefer? What about better naming? Is "before" a confusing name?</p><p>Thanks a lot for your thoughts!<br></p><p>Cheers,<br></p><p>Marko<br></p><p><br></p><p> <br></p><p><br></p></div></div></div></div></div></div></div>