4 ms·
I think you’re looking at a program verification problem. With this tool: http://viper.ethz.ch/ http://viper.ethz.ch/ You essentially sprinkle your functions w
by red0point 5y ago
I think you’re looking at a program verification problem.
With this tool:
http://viper.ethz.ch/ http://viper.ethz.ch/
You essentially sprinkle your functions with pre- and post conditions (& loops), press „verify“ and it will verify the correctness of your program code.
There are multiple frontends you can use for different languages. Behind the scenes your code + annotations are converted from e.g. Python/Rust/Go to an intermediate language (Viper), which is then verified.
- agucova 5y agoIsn't this just an extension of design by contract? What advantages come from using a framework like this instead of traditional assertions for contracts?
- red0point 5y agoIt is indeed just an extension of that very idea, developed at the same institution where design-by-contract has been introduced a few decades ago. However, instead of crashing at runtime due to a failed assertion, you get a guarantee that your program will in fact not violate said assertions and behave correctly. It also entails a nice speed bonus, instead of checking the assertions all the time, which could be quite a complex feat for non-trivial post-conditions, you do it once, symbolically, for all possible executions.
- rramadass 5y agoDidn't know about this; looks interesting. Thanks for the pointer.