3 ms·
> Assertions belong in the program source, and in the same syntax as the language of the program. They're mostly written by the people writing the code. The pro
by MaxBarraclough 1y ago
> Assertions belong in the program source, and in the same syntax as the language of the program. They're mostly written by the people writing the code. The proof of correctness work can and should be integrated with development.
SPARK Ada takes this approach, what do you make of it?
- Animats 1y agoLooking around for examples. Google can't find anything non-trivial. Do you know of something I can look at?
- MaxBarraclough 1y agoPerhaps the Ironclad kernel [0] and SPARKNaCl? [1] Here's a search of the Alire packages for 'spark' [2]. Merely using SPARK doesn't mean full formal verification of all correctness properties, as SPARK can be used at different 'assurance levels' from stone (no real formal verification but you restrict yourself to the SPARK subset of Ada) to platinum (full verification). [3] [0] https://ironclad-os.org/ https://ironclad-os.org/ [1] https://github.com/rod-chapman/SPARKNaCl https://github.com/rod-chapman/SPARKNaCl [2] https://alire.ada.dev/search/?q=spark https://alire.ada.dev/search/?q=spark [3] https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...