1

私は Ada noob であり、整数のリストを取り、各要素を 1 ずつ減らす単純な関数を作成しています。私のブロンズ モードの証明は問題ありませんが、実際にメインで関数を使用して、実際に何をしているかを確認しようとしています。闘争を証明することになっています。配列を初期化して値を割り当てる方法がわかりません（0..10であるはずです）。また、decrement(integer) 関数と decrementList(ArrayOfNumbers) 関数ではなく、1 つの decrement 関数だけでこれを実装できたかどうかもわかりません。または、私がそれを正しく行っている場合。私が見つけた良いドキュメントがないので、自分の道を推測することになっているように感じます。このパッケージは、以前のタスクの一部であるため、flip_coin と呼ばれます。コインの反転に関連するものは無視できます。

仕様ファイルは次のとおりです。

package flip_coin with SPARK_Mode is

    type Coin is (Heads, Tails);

    type Index is range 0 .. 10;
  
    type Numbers is array (Index) of Integer;

    function flip (x : Coin) return Coin with
 
     Post => flip'Result /= x;

    procedure flipCoin (x : in out Coin);

    function decrement (i : Integer) return Integer;
    
    procedure decrementList (n : in out Numbers);

 end flip_coin;

本体ファイルは次のとおりです。

package body flip_coin with SPARK_Mode is

    function flip (x : Coin) return Coin
    is
      begin
        if x = Heads then return Tails; else return Heads; end if;
    end flip;

    procedure flipCoin (x : in out Coin)
    is
    begin
      x := flip(x);
   end flipCoin;

   function decrement (i : Integer) return Integer
   is
   begin
      return i-1;
   end decrement;

   procedure decrementList (n : in out Numbers) is

      a : Index := n'First;
      b : Index := n'Last;
   begin
      for i in a..b loop
         n(i) := decrement(n(i));
      end loop;
   end decrementList;



end flip_coin;

ここにメインファイルがあります：

with flip_coin; use flip_coin;
with Ada.Text_IO; use Ada.Text_IO;

procedure Main is
   newCoin : Coin := Heads;
   numbers : Numbers := (0,1,2,3,4,5,6,7,8,9,10);
 begin
   Put_Line("Element 9, before decrement:");
   Put_Line(numbers(9)'Image);
   decrementList(numbers);
   Put_Line("Element 9, after decrement:");
   Put_Line(numbers(9)'Image);
   Put_Line("Coin before flip:");
   Put_Line(newCoin'Image);
   flipCoin(newCoin);
   Put_Line("Coin after flip:");
   Put_Line(newCoin'Image);
end Main;

実行しようとしたときのエラーは次のとおりです。

main.adb:6:14: object "Numbers" cannot be used before end of its declaration

どんな助けでも大歓迎です。ティア

4

2 に答える 2