Added some spec. Sadly, local borrower of an access obect is not yet …

…supported.
mkf · Jan 13, 2020 · 3fc0770 · 3fc0770
1 parent f9ca384
commit 3fc0770
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 1 deletion.
diff --git a/asdinve/src/asdinvelib.adb b/asdinve/src/asdinvelib.adb
@@ -12,6 +12,20 @@ is
       c : slrarr := (null, null);
    end record;
 
+   function naive_result (A : arr) return Natural
+   is
+      t : Natural := 0;
+   begin
+      for i in A'Range loop
+         for j in A'Range loop
+            if i<j and A(i)>A(j) then
+               t := t + 1;
+            end if;
+         end loop;
+      end loop;
+      return t;
+   end naive_result;
+
    function result (A : arr) return Natural
    is
       t : Natural := 0;

diff --git a/asdinve/src/asdinvelib.ads b/asdinve/src/asdinvelib.ads
@@ -2,5 +2,7 @@ package AsdinveLib with
 SPARK_Mode
 is
    type arr is array (Positive range <>) of Positive;
-   function result(A : arr) return Natural;
+   function naive_result(A : arr) return Natural with Ghost;
+   function result(A : arr) return Natural with
+      Post => result'Result = naive_result(A);
 end AsdinveLib;