On Sun, Sep 23, 2018 at 2:05 AM Marko Ristin-Kaufmann <[email protected]> wrote: > > Hi, > > (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.) > > 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. > > 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. > > The library is available at http://github.com/Parquery/icontract. 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 conflicting > contract libraries can not integrate (e.g., the contracts can not be > inherited between two different contract libraries). > > So far, the most important bits have been implemented in icontract: > > Preconditions, postconditions, class invariants > Inheritance of the contracts (including strengthening and weakening of the > inherited contracts) > Informative violation messages (including information about the values > involved in the contract condition) > Sphinx extension to include contracts in the automatically generated > documentation (sphinx-icontract) > Linter to statically check that the arguments of the conditions are correct > (pyicontract-lint) > > We are successfully using it in our code base and have been quite happy about > the implementation so far. > > There is one bit still missing: accessing "old" values in the postcondition > (i.e., 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. > > For example, consider a new dictionary class that has "get" and "put" methods: > > from typing import Optional > > from icontract import post > > class NovelDict: > def length(self)->int: > ... > > def get(self, key: str) -> Optional[str]: > ... > > @post(lambda self, key, value: self.get(key) == value) > @post(lambda self, key: old(self.get(key)) is None and old(self.length()) > + 1 == self.length(), > "length increased with a new key") > @post(lambda self, key: old(self.get(key)) is not None and > old(self.length()) == self.length(), > "length stable with an existing key") > def put(self, key: str, value: str) -> None: > ... > > How could we possible implement this "old" function? > > Here is my suggestion. I'd introduce a decorator "before" that would allow > you to store whatever values in a dictionary object "old" (i.e. an object > whose properties correspond to the key/value pairs). The "old" is then passed > to the condition. Here is it in code: > > # omitted contracts for brevity > class NovelDict: > def length(self)->int: > ... > > # omitted contracts for brevity > def get(self, key: str) -> Optional[str]: > ... > > @before(lambda self, key: {"length": self.length(), "get": self.get(key)}) > @post(lambda self, key, value: self.get(key) == value) > @post(lambda self, key, old: old.get is None and old.length + 1 == > self.length(), > "length increased with a new key") > @post(lambda self, key, old: old.get is not None and old.length == > self.length(), > "length stable with an existing key") > def put(self, key: str, value: str) -> None: > ... > > 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. > > "before" decorator would also have "enabled" property, so that you can turn > it off (e.g., 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. > > Is this a sane approach to "old" values? Any alternative approach you would > prefer? What about better naming? Is "before" a confusing name?
The dict can be splatted into the postconditions, so that no special name is required. This would require either that the lambdas handle **kws, or that their caller inspect them to see what names they take. Perhaps add a function to functools which only passes kwargs that fit. Then the precondition mechanism can pass `self`, `key`, and `value` as kwargs instead of args. For functions that have *args and **kwargs, it may be necessary to pass them to the conditions as args and kwargs instead. The name "before" is a confusing name. It's not just something that happens before. It's really a pre-`let`, adding names to the scope of things after it, but with values taken before the function call. Based on that description, other possible names are `prelet`, `letbefore`, `predef`, `defpre`, `beforescope`. Better a name that is clearly confusing than one that is obvious but misleading. By the way, should the first postcondition be `self.get(key) is value`, checking for identity rather than equality? _______________________________________________ Python-ideas mailing list [email protected] https://mail.python.org/mailman/listinfo/python-ideas Code of Conduct: http://python.org/psf/codeofconduct/
