<div dir="ltr">One thought I had pertains to a very narrow sub-set of cases, but may provide a starting point. For the cases where a precondition, invariant, or postcondition only involves a single parameter, attribute, or the return value (respectively) and it's reasonably simple, one could write it as an expression acting directly on the type annotation:<br><br>def encabulate(<br> reactive_inductance: 1 >= float > 0, # description <br><div> capacitive_diractance: int > 1, # description</div><div> delta_winding: bool # description</div><div> ) -> len(Set[DingleArm]) > 0: # ??? I don't know how you would handle more complex objects...<br> do_stuff<br> with_things<br> ....<br><br>Anyway. Just more food for thought...<br><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Tue, Nov 27, 2018 at 10:47 PM Abe Dillon <<a href="mailto:abedillon@gmail.com">abedillon@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="ltr"><div dir="ltr">I've been pulling a lot of ideas from the recent discussion on design by contract (DBC), the elegance and <a href="https://bemusement.org/doctests-arent-code" target="_blank">drawbacks</a> of <a href="https://docs.python.org/3/library/doctest.html" target="_blank">doctests</a>, and the <a href="https://www.youtube.com/watch?v=MYucYon2-lk" target="_blank">amazing talk</a> given by Hillel Wayne at this year's PyCon entitled "Beyond Unit Tests: Taking your Tests to the Next Level".<div><br></div><div>To recap a lot of previous discussions:<br><br>- Documentation should tell you:</div><div> A) What a variable represents</div><div> B) What kind of thing a variable is<br> C) The acceptable values a variable can take<br><br>- Typing and Tests can partially take the place of documentation by filling in B and C (respectively) and sometimes A can be inferred from decent naming and context.<br><br>- Contracts can take the place of many tests (especially when combined with a library like hypothesis)</div><div><br></div><div>- Contracts/assertions can provide "stable" documentation in the sense that it can't get out of sync with the code.<br><br>- Attempts to implement contracts using standard Python syntax are verbose and noisy because they rely heavily on decorators that add a lot of repetitive preamble to the methods being decorated. They may also require a metaclass which restricts their use to code that doesn't already use a metaclass.<br><br>- There was some discussion about the importance of "what a variable represents" which pointed to <a href="http://pgbovine.net/python-unreadable.htm" target="_blank">this article</a> by Philip J. Guo (author of the magnificent <a href="http://pythontutor.com" target="_blank">pythontutor.com</a>). I believe Guo's usage of "in-the-small" and "in-the-large" are confusing because a well decoupled program shouldn't yield functions that know or care how they're being used in the grand machinations of your project. The examples he gives are of functions that could use a doc string and some type annotations, but don't actually say how they relate to the rest of the project.<br><br>One thing that caught me about Hillel Wayne's talk was that some of his examples were close to needing practically no code. He starts with:<br><br><font face="monospace, monospace">def tail(lst: List[Any]) -> List[Any]:<br> assert len(lst) > 0, "precondition"<br> result = lst[1:]</font></div><div><font face="monospace, monospace"> assert [lst[0]] + result == lst, "postcondition"<br> return result</font><br><br>He then re-writes the function using a contracts library:<br><br><font face="monospace, monospace">@require("lst must not be empty", lambda args: len(args.lst) > 0)<br>@ensure("result is tail of lst", lambda args, result: [args.lst[0]] + result == args.lst)<br>def tail(lst: List[Any]) -> List[Any]:<br> return lst[1:]</font><br><br>He then writes a unit test for the function:<br><br><font face="monospace, monospace">@given(lists(integers(), 1))<br>def test_tail(lst):<br> tail(lst)</font><br><br>What strikes me as interesting is that the test pretty-much doesn't need to be written. The 'given' statement should be redundant based on the type annotation and the precondition. Anyone who knows hypothesis, just imagine the @require is a hypothesis 'assume' call. Furthermore, hypothesis should be able to build strategies for more complex objects based on class invariants and attribute types:<br><br>@invariant("no overdrafts", lambda self: self.balance >= 0)<br>class Account:</div><div> def __init__(self, number: int, balance: float = 0):</div><div> super().__init__()<br> self.number: int = number</div><div> self.balance: float = balance<br><br>A library like hypothesis should be able to generate valid account objects. Hypothesis also has <a href="https://hypothesis.readthedocs.io/en/1.4.1/stateful.html" target="_blank">stateful testing</a> but I think the implementation could use some work. As it is, you have inherit from a class that uses a metaclass AND you have to pollute your class's name-space with helper objects and methods.</div><div><br>If we could figure out a cleaner syntax for defining invariants, preconditions, and postconditions we'd be half-way to automated testing UTOPIA! (ok, maybe I'm being a little over-zealous)<br><br>I think there are two missing pieces to this testing problem: side-effect verification and failure verification.<br><br>Failure verification should test that the expected exceptions get thrown when known bad data is passed in or when an object is put in a known illegal state. This should be doable by allowing Hypothesis to probe the bounds of unacceptable input data or states, though it might seem a bit silly because if you've already added a precondition, "x >= 0" to a function, then it obviously should raise a PreconditionViolated when passed any x < 0. It may be important, however; if for performance reasons, you need to disable invariant checking but you still want certain bad input to raise exceptions, or your system has two components that interact with slightly mis-matched invariants and you want to make sure the components handle the edge-condition correctly. You can think of Types from a set-theory perspective where the Integer type is conceptually the set of all integers, and invariants would specify a smaller subset than Typing alone, however if the set of all valid outputs of one component is not completely contained within the set of all valid inputs to another component, then there will be edge-cases resulting from the mismatch. In that sense, some of the invariant verification could be static-ish (as much as Python allows).<br><br>Side-effect verification is usually done by mocking dependencies. You pass in a mock database connection and make sure my object sends and receives data as expected. As crazy as it sounds, this too can be almost completely automated away if all of the above tools are in place AND if Python gained support for Exception annotations. I wrote a Java (yuck) library at work that does this. I wan't to port it to Python and share it, but it basically enumerates a bunch of stuff: the "sources" and "destinations" of the system, how those relate to dependencies, how they relate to each other (if dependency X is unresponsive, I can't get sources A, B, or G and if I can't get source B, I can't write destination Y), the dependency failure modes (Exceptions raised, timeouts, unrecognized key, missing data, etc.), all the public methods of the class under test and what sources and destinations they use.<br><br>Then I enumerate 'k' from 0 to some limit for the max number of simultaneous faults to test for:<br> Then for each method that can have n >= k simultaneous faults I test all (n choose k) combinations of faults for that method against the desired behavior.<br><br>I'm sure that explanation is as clear as mud. I will try to get a working Python example at some point to demonstrate.<br><br>Finally, in the PyCon video; Hillel Wayne shows an example of testing that an "add" function is commutative. It seems that once you write that invariant, it might apply to many different functions. A similar invariant may be "reversibility" like:<br><br>@given(text())<br>def test_reversable_codex(s):<br> assert s == decode(encode(s)), "not reversible"<br><br>That might be a common property that other functions share:<br><br>@invariant(reversible(decode))<br>def encode(s: str) -> bytes: ...<br><br>Having said all that, I wanted to brainstorm some possible solutions for implementing some or all of the above in Python without drowning you code in decorators. <br><br>NOTE: Please don't get hung up on specific syntax suggestions! Try to see the forest through the trees!<br><br>An example syntax could be:<br><br>#Instead of this<br><font face="monospace, monospace">@require("lst must not be empty", lambda args: len(args.lst) > 0)<br>@ensure("result is tail of lst", lambda args, result: [args.lst[0]] + result == args.lst)<br>def tail(lst: List[Any]) -> List[Any]:<br> return lst[1:]</font><br><br>#Maybe this?<br>non_empty = invariant("Must not be empty", lambda x: len(x) > 0) # can be re-used</div><div><br>def tail(lst: List[Any] d"Description of what this param represents. {non_empty}") -> List[Any] d"Description of return value {lst == [lst[0]] + __result__}":</div><div> """</div><div> Description of function</div><div> """<br> return lst[1:]<br><br>Python could build the full doc string like so:<br><br>""" <br>Description of function<br><br>Args:<br> lst: Description of what this param represents. Must not be empty.<br><br>Returns: </div><div> Description of return value.<br>"""</div><div><br></div><div>d-strings have some description followed by some terminator after which either invariant objects or [optionally strings] followed by an expression on the arguments and __return__?<br><br>I'm sorry this is so half-baked. I don't really like the d-string concept and I'm pretty sure there are a million problems with it. I'll try to flesh out the side-effect verification concept more later along with all the other poorly explained stuff. I just wanted to get these thoughts out for discussion, but now it's super late and I have to go!<br><br><br> <br></div><div><br><br><br></div></div></div>
</blockquote></div>