gnatprove_13.2.1_28fc3583/share/examples/spark/gnatprove_by_example/ug__recursive_subprograms-structural/recursive_subprograms.ads

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
with Ada.Numerics.Big_Numbers.Big_Integers;
use  Ada.Numerics.Big_Numbers.Big_Integers;

package Recursive_Subprograms with SPARK_Mode is
   type Cell;
   type List is access Cell;
   type Cell is record
      Value : Integer;
      Next  : List;
   end record;

   function Length (L : List) return Big_Natural is
     (if L = null then Big_Natural'(0) else Length (L.Next) + 1)
   with Subprogram_Variant => (Structural => L);
end Recursive_Subprograms;