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

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.