2 ms·
You don’t have to verify your whole application, just set SPARK_Mode => Off where you want to skip it. Alternatively, set the global default to Off and it becom
by synack 2y ago
You don’t have to verify your whole application, just set SPARK_Mode => Off where you want to skip it. Alternatively, set the global default to Off and it becomes an opt-in feature.
Proof levels depend on your goals, but most requirements are satisfied by proof of “Absence of Runtime Exceptions” (AoRTE), which is easier than a full formal proof.
- Ygg2 2y agoHow would you prove stuff about your code like memory safety.
- deleted 2y ago[deleted]
- synack 2y agoOut of bounds access would raise a runtime exception, so absence of runtime exceptions proves that cannot happen. Recent versions of SPARK add functionality similar to Rust’s borrow checker as well. You can find more information in the users guide. https://docs.adacore.com/spark2014-docs/html/ug/index.html https://docs.adacore.com/spark2014-docs/html/ug/index.html