3 ms·
Doesn't ADA have some method of checking if the input/output of a function is within bound? Can't remember if its a runtime or compile check however. But the c
by mofosyne 2y ago
Doesn't ADA have some method of checking if the input/output of a function is within bound? Can't remember if its a runtime or compile check however.
But the concept of function contract verification would be interesting.
- carlmr 2y agoThe 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...