[haetze]

You are right that SPARK tries to prove the absence of these errors. In that case you don't need these checks and turn them off. If you don't they are still run.

Ada has Dynamic_Predicate(s) which "can be any Boolean expression". [0] So, I'm guessing, you can write a pointless Predicate which does not terminate in some cases or takes unreasonably long.

[0] http://www.ada-auth.org/standards/12rat/html/Rat12-2-5.html

[MaxBarraclough]

Thanks, I wasn't aware of that feature, I think you're right.

> In the case of Dynamic_Predicate, the expression can be any Boolean expression.

Ada functions are permitted to have side-effects (although this is disallowed in SPARK), so I imagine it would be possible to make a real mess if you wanted to.