4 ms·
It's more like writing preconditions and postconditions, and proving that the implementation of the function will always satisfying the postconditions. And then
by elbows 10y ago
It's more like writing preconditions and postconditions, and proving that the implementation of the function will always satisfying the postconditions. And then also proving that no other part of your program can call the function in a way that violates its preconditions. The proofs are checked automatically.
I can't point you to a simple example. But you could check out the book "Software Foundations" (available for free at https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html). If you have time to read the first few chapters it may clarify things.
- gravypod 10y agoSo then how is it any different from what most people already do? We already use assets liberally in development, specify everything in documentation, and then use linting systems to tell us if we violate our rules? This just sounds like another name used by people to sound like they are doing something that was already being done in the professional. Edit: I'll read through that book, thanks!
- AstralStorm 10y agoIn how much of the code are you actually applying those best practices? Are you verifying interactions between all modules? True formal verification checks everything, because anything unchecked shows up clearly as a baseless assumption (axiom).