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;
    
    
    Run

Again, 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.

Reply via email to