sparre: thanks for the info. will try that out one day.
as I understand it, work is ongoing for the SPARK tools to accept static and dynamic predicates http://www.spark-2014.org/entries/detail/spark-2014-rationale-type-predicates
using such constructs in GNAT GPL 2015, the SPARK tools (gnatprove) says that predicates are not supported yet. That is different behavior compared to GNAT GPL 2014 where they were forbidden from SPARK