@anonymous234 said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@Gąska said in What if we just didn't write the bugs, then we wouldn't have buggy software:
@dkf how so? If I make a function that stores some information in a shared storage available as system service, it makes sense to make sure the information is then accessible as a postcondition.
I think, strictly speaking, the postcondition would be "Write() function has been called once pointing to data that had this content". Whether the file now contains the data or not is the OS' responsibility, and if you know that for sure you'll now have to involve all the hairy file system details (caching, etc.) in your model...
There's a reason I said "shared storage available as system service", not "filesystem". I meant something like RPC manager/local master server, not a bottomless hole you drop things to and not care what happens to them afterwards that files usually are. Though looking how literally everyone thought I'm talking about filesystems, I admit I could've worded it very poorly.