[haetze]

Doesn't Ada have a sort of arbitrary computation on assignment? I think I remember that there are rules when predicates on types are checked. (Depending on the Assertion_Policy of course) I'm not sure how that works on assignment though.

[MaxBarraclough]

Good point, Ada's runtime range checks mean that an assignment can raise an exception. [0] Part of what SPARK Ada does is to prove the absence of such constraint errors. [1]

I don't think Ada supports arbitrary user-specified constraints, but I'm no expert.

[0] https://gcc.gnu.org/onlinedocs/gcc-10.2.0/gnat_ugn/Run-Time-...

[1] https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...

[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.