问题描述
我是 Ada 菜鸟,正在编写一个简单的函数,该函数接受一个整数列表并将每个元素递减 1。我的青铜模式证明通过了,但尝试在 main 中实际使用该函数以查看它是否真的做它应该做的事证明是一场斗争。我不确定如何初始化数组并分配值(应该是 0..10)。我也不确定我是否可以仅使用一个递减函数而不是递减(整数)和递减列表(ArrayOfNumbers)函数来实现这一点。或者,如果我做对了。任何帮助都是王牌,我没有找到任何好的文档,所以我觉得我应该猜测我的方式。该包称为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
再次非常感谢任何帮助。 TIA
解决方法
Ada 是不区分大小写的语言。因此,数字和数字是相同的。将 numbers 更改为 numbers_array 怎么样。
,这是一个可见性问题,为什么初学者应该避免use <package>
。了解可见性是了解 Ada 的关键。避免使用包子句会让您考虑可见性并帮助您理解它。
您有 2 个名为 Numbers
的事物,全名分别为 Flip_Coin.Numbers
和 Main.Numbers
。在 Main
中,本地名称 Numbers
对 Numbers
隐藏了使用可见的 Flip_Coin
。它仍然可以引用为 Flip_Coin.Numbers
。
关于 Ada 可见性的最佳介绍是 Ada Distilled。