The pre/postconditions in Ada are runtime checks [1]. GNATprove can be used to statically check these though in the SPARK subset of Ada [2]. [1] https://www.ad

The pre/postconditions in Ada are runtime checks [1]. GNATprove can be used to statically check these though in the SPARK subset of Ada [2]. [1] https://www.adacore.com/gems/gem-31 https://www.adacore.com/gems/gem-31 [2] https://docs.adacore.com/spark2014-docs/html/ug/en/source/assertion_pragmas.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/as...