Let me add to the above. The following program passes SPARK 2014 checks:
with Ada.Text_IO; use Ada.Text_IO;
procedure Test_Contract with Spark_Mode is
procedure Test(a: Integer) with Pre => (a > 5) is
begin
if a > 5 then Put_Line("Oops!"); end if;
end Test;
subtype AtLeastSix is Integer range 6..Positive'Last;
a: AtLeastSix := 6;
begin
Test(a);
end Test_Contract;
RunAgain, let me know if there's a way to do that with Nim at compile time. If it can, I'd like to know that.
