Comment on Dafny is a verification-aware programming languageparentComments−mofosyne2yDoesn'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.−carlmr2yThe 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 [2] https://docs.adacore.com/spark2014-docs/html/ug/en/source/as...
Comments
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.
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 [2] https://docs.adacore.com/spark2014-docs/html/ug/en/source/as...