3 ms·
From the book: > dynamic checks (such as array bounds checks) provide verification that could not be done at compile time. Dynamic checks are performed at runt
by qznc 6y ago
From the book:
> dynamic checks (such as array bounds checks) provide verification that could not be done at compile time. Dynamic checks are performed at runtime, similar to what is done in Java.
- johnisgood 6y agoCheck out the table on https://docs.adacore.com/spark2014-docs/html/ug/en/usage_scenarios.html https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce.... > SPARK builds on the strengths of Ada to provide even more guarantees statically rather than dynamically. As summarized in the following table, Ada provides strict syntax and strong typing at compile time plus dynamic checking of run-time errors and program contracts. SPARK allows such checking to be performed statically. In addition, it enforces the use of a safer language subset and detects data flow errors statically.