Hi, I annotated pathlib with contracts: https://github.com/mristin/icontract-pathlib-poc. I zipped the HTML docs into https://github.com/mristin/icontract-pathlib-poc/blob/master/contracts-pathlib-poc.zip, you can just unpack and view the index.html.
One thing I did observe was that there were contracts written in text all over the documentation -- I tried to formulate most of them in code. Since I'm not the implementer nor very familiar with the module, please consider that many of these contracts can be definitely made more beautiful. There were some limitations to icontract-sphinx extension and icontracts which I noted at the top of the document. (Note also that I had to rename the file to avoid import conflicts.) Some of the contracts might seem trivial -- but mind that you, as a writer, want to tell the user what s/he is expected to fulfill before calling the function. For example, if you say: rmdir() Remove this directory. The directory must be empty. Requires: - not list(self.iterdir()) (??? There must be a way to check this more optimally) - self.is_dir() self.is_dir() contract might seem trivial -- but it's actually not. You actually want to convey the message: dear user, if you are iterating through a list of paths, use this function to decide if you should call rmdir() or unlink(). Analogously with the first contract: dear user, please check if the directory is empty before calling rmdir() and this is what you need to call to actually check that. I also finally assembled the puzzle. Most of you folks are all older and were exposed to DbC in the 80ies championed by DbC zealots who advertised it as *the *tool for software development. You were repulsed by their fanaticism -- the zealots also pushed for all the contracts to be defined, and none less. Either you have 100% DbC or no sane software development at all. I, on the other side, were introduced to DbC in university much later -- Betrand held most of our software engineering lectures (including introduction to programming which was in Eiffel ;)). I started going to uni in 2004; by that time there was no fanaticism about DbC around -- not even by Bertrand himself. We were taught to use it just as yet another tool in our toolbox along unit testing and formal proofs. Not as a substitute for unit testing! Just as yet another instrument for correctness. There was no 100% DbC -- and we did quite some realistic school projects such as a backend for a flight-booking website in Eiffel (with contracts ;)). I remember that we got minus points if you wrote something in the documentation that could have been easily formalized. But nobody pushed for all the contracts; everybody was pragmatic. Nobody didn't even think about proposing to abolish unit testing and staff all the tests in the contracts to be smoke-tested. While you read my proposals in the light of these 80ies style DbC proponents, I think always only about a much more minor thing: a simple tool to make *some part* of the documentation verifiable. One lesson that I learned from all these courses was to what degree our understandings (especially among non-native speakers) differ. Even simple statements such as "x must be positive" can mean x > 0 and x >= 0 to different people. For me it became obvious that "x > 0" is clearer than "x must be positive" -- and this is that "obvious" which I always refer in my posts on this list. If a statement can not be formalized easily and introduces confusion, that's a different pair of shoes. But if it can -- why shouldn't you formalize it? I still can't wrap my head around the idea that it's not obvious that you should take the formal version over the informal version *if both are equally readable*, but one is far less unambiguous. It feels natural to me that if you want to kick out one, kick out the more ambiguous informal one. What's the point of all the maths if the informal languages just do as well? And that's why I said that the libraries on pypi meant to be used by multiple people and which already have type annotations would obviously benefit from contracts -- while you were imagining that all of these libraries need to be DbC'ed 100%, I was imagining something much more humble. Thus the misunderstanding. After annotating pathlib, I find that it actually needs contracts more thain if it had type annotations. For example: stat() Return the result of the stat() system call on this path, like os.stat() does. Ensures: - result is not None ⇒ self.exists() - result is not None ⇒ os.stat(str(self)).__dict__ == result.__dict__ (??? This is probably not what it was meant with ‘like os.stat() does’?) But what does it mean "like os.stat() does"? I wrote equality over __dict__'s in the contract. That was my idea of what the implementer was trying to tell me. But is that the operator that should be applied? Sure, the contract merits a description. But without it, how am I supposed to know what "like" means? Similarly with rmdir() -- "the directory must be empty" -- but how exactly am I supposed to check that? Anyhow, please have a look at the contracts and let me know what you think. Please consider it an illustration. Try to question whether the contracts I wrote are so obvious to everybody even if they are obvious to you and keep in mind that the user does not look into the implementation. And please try to abstract away the aesthetics: neither icontract library that I wrote nor the sphinx extension are of sufficient quality. We use them for our company code base, but they still need a lot of polishing. So please try to focus only on the content. We are still talking about contracts in general, not about the concrete contract implementation. Cheers, Marko On Thu, 27 Sep 2018 at 11:37, Marko Ristin-Kaufmann <marko.ris...@gmail.com> wrote: > Hi Paul, > I only had a contracts library in mind (standardized so that different > modules with contracts can interact and that the ecosystem for automic > testing could emerge). I was never thinking about the philosophy or design > methodology (where you write _all_ the contracts first and then have the > implementation fulfill them). I should have clarified that more. I > personally also don't think that such a methodology is practical. > > I really see contracts as verifiable docs that rot less fast than human > text and are formally precise / less unambiguous than human text. Other > aspects such as deeper tests and hand-braking (e.g., as postconditions > which can't be practically implemented in python without exit stack context > manager) are also nice to have. > > I should be done with pathlib contracts by tonight if I manage to find > some spare time in the evening. > > Cheers, > Marko > > Le jeu. 27 sept. 2018 à 10:43, Paul Moore <p.f.mo...@gmail.com> a écrit : > >> On Thu, 27 Sep 2018 at 08:03, Greg Ewing <greg.ew...@canterbury.ac.nz> >> wrote: >> > >> > David Mertz wrote: >> > > the reality is that they really ARE NOT much different >> > > from assertions, in either practice or theory. >> > >> > Seems to me that assertions is exactly what they are. Eiffel just >> > provides some syntactic sugar for dealing with inheritance, etc. >> > You can get the same effect in present-day Python if you're >> > willing to write the appropriate code. >> >> Assertions, as far as I can see, are the underlying low level >> *mechanism* that contracts would use. Just like they are the low level >> mechanism behind unit tests (yeah, it's really exceptions, but close >> enough). But like unit tests, contracts seem to me to be a philosophy >> and a library / programming technique layered on top of that base. The >> problem seems to me to be that DbC proponents tend to evangelise the >> philosophy, and ignore requests to show the implementation (often >> pointing to Eiffel as an "example" rather than offering something >> appropriate to the language at hand). IMO, people don't tend to >> emphasise the "D" in DbC enough - it's a *design* approach, and more >> useful in that context than as a programming construct. >> >> For me, the philosophy seems like a reasonable way of thinking, but >> pretty old hat (I learned about invariants and pre-/post-conditions >> and their advantages for design when coding in PL/1 in the 1980's, >> about the same time as I was learning Jackson Structured Programming). >> I don't think in terms of contracts as often as I should - but it's >> unit tests that make me remember to do so. Would a dedicated >> "contracts" library help? Probably not much, but maybe (if it were >> lightweight enough) I could get used to the idea. >> >> Like David, I find that having contracts inline is the biggest problem >> with them. I try to keep my function definitions short, and contracts >> can easily add 100% overhead in terms of lines of code. I'd much >> prefer contracts to be in a separate file. (Which is basically what >> unit tests written with DbC as a principle in mind would be). If I >> have a function definition that's long enough to benefit from >> contracts, I'd usually think "I should refactor this" rather than "I >> should add contracts". >> >> Paul >> _______________________________________________ >> Python-ideas mailing list >> Python-ideas@python.org >> https://mail.python.org/mailman/listinfo/python-ideas >> Code of Conduct: http://python.org/psf/codeofconduct/ >> >
_______________________________________________ Python-ideas mailing list Python-ideas@python.org https://mail.python.org/mailman/listinfo/python-ideas Code of Conduct: http://python.org/psf/codeofconduct/
