I'm translating an exercise I made in Dafny into SPARK, where one verifies a tail recursive function against a recursive one. The Dafny source (censored, because it might still be used for classes)...

I have the following program: procedure Main with SPARK_Mode is F : array (0 .. 10) of Integer := (0, 1, others => 0); begin for I in 2 .. F'Last loop F (I) := F (I - 1) + F (I - 2); end lo...

New to Spark, and new to Ada, so this question may be overly broad. However, it's asked in good faith, as part of an attempt to understand Spark. Besides direct answers to the questions below, I we...