3 ms·
Runtime checks are compiler implementation issue rather than language issue itself. With static analysis compiler could eliminate redundant runtime checks. For
by xentropy 6y ago
Runtime checks are compiler implementation issue rather than language issue itself. With static analysis compiler could eliminate redundant runtime checks.
For example, if SPARK (Ada subset) is used and absense of runtime errors can be proved by GNATprove, then runtime check generation can be disabled in Ada compiler.
- Kototama 6y agoThanks for clarification. Which underlying (type) theory is used in GNATprove?
- xentropy 6y agoI don't know details. GNATprove generates verification conditions (conjectures) from SPARK code and assertations. Then it feeds these verification conditions to proof tool (Why3, Alt-Ergo, CVC4 or Z3). https://github.com/AdaCore/spark2014 https://github.com/AdaCore/spark2014