29 Sep
2018
29 Sep
'18
12:30 a.m.
Chris Angelico wrote:
But as a part of the function's declared intent, it's fine to have a postcondition of "the directory will be empty" even though something could drop a file into it.
If you only intend the contract to serve as documentation, I suppose that's okay, but it means you can't turn on runtime checking of contracts, otherwise your program could suffer spurious failures. -- Greg