I’m trying to learn SPARK by implementing a Euclidean Ring package. (Don’t let the mathematics scare you; it’s not really relevant.) The package is generic, with several parameters that needs specification. Among these are a
Size function, a
Zero function, and a
If SPARK is to have any prayer at all of proving correctness, the
rem function needs a constraint along these lines:
generic -- a bunch of stuff omitted with function "rem" ( Dividend, Divisor : Ring_Element ) return Ring_Element is <> with Pre => Divisor /= Zero, Post => ( "rem"'Result /= Zero or else Size ( "rem"'Result ) < Size ( Divisor ) ) ;
…and the compiler chokes on the contracts:
euclidean.ads:39:13: incorrect placement of aspect "Pre" euclidean.ads:40:13: incorrect placement of aspect "Post"
Originally I tried placing it before the
is <> but that didn’t work, either.
So… where does one specify constraints for the parameters to a generic?