我的目标是证明霍纳法则是正确的。为此，我将 Horner 当前计算的值与“实数”多项式的值进行比较。
所以我做了这段代码：
package body Poly with SPARK_Mode is
function Horner (X : Integer; A : Vector) return Integer is
Y : Integer := 0;
Z : Integer := 0 with Ghost;
begin
for I in reverse A'First .. A'Last loop
pragma Loop_Invariant (Y * (X ** (I - A'First + 1)) = Z);
Y := A(I) + Y * X;
Z := Z + A(I) * (X ** (I - A'First));
end loop;
pragma Assert (Y = Z); …我需要有关 Ada SPARK 的帮助。我想将像“1”这样的字符串保存到整数变量中。背景：我想从命令行输入读取数字并将它们作为整数处理，并使用 SPARK Prove 检查程序。这是一个最小的例子：
with Ada.Strings.Unbounded; use Ada.Strings.Unbounded;
procedure Main is
pragma SPARK_Mode;
test_string : Unbounded_String;
identifier : Integer;
begin
test_string := To_Unbounded_String("1");
identifier := Integer'Value(To_String(test_string));
end Main;
当我执行 SPARK Prove 时，我收到以下消息：“中：前提条件可能失败”。我已经实现了一个函数来检查 test_string 是否包含 0 - 9 的字符，但它没有解决问题。有谁有解决问题的方法吗？
我写了一个非常简单的程序，但未能证明它的功能正确。它使用项目列表，每个项目都有一个字段指示它是免费还是已使用：
type t_item is record
used : boolean := false;
value : integer := 0;
end record;
type t_item_list is array (1 .. MAX_ITEM) of t_item;
items : t_item_list;
还有一个计数器，指示使用的元素数：
used_items : integer := 0;
该append_item程序检查used_items柜台看看，如果列表已满。如果不是，则将第一个空闲条目标记为已使用，并且used_items计数器增加：
procedure append_item (value : in integer; success : out boolean)
is
begin
if used_items = MAX_ITEM then
success := false;
return;
end if;
for i in items'range loop
if not items(i).used then
items(i).value := value;
items(i).used := true; …代码如下所示：
规格：
type Some_Record_Type is private;
procedure Deserialize_Record_Y(Record: in out Some_Record_Type)
with Post => (
if Status_OK then (
...
other postconditions
...
and then
Record_Field_X_Count(Record) = Record_Field_X_Count(Record'Old)
and then
Record_Field_X(Record) = Record_Field_X(Record'Old)
)
);
function Record_Field_X(Record: Some_Record_Type) return X_Unbounded_Array_Type;
function Record_Field_X_Count(Record: Some_Record_Type) return Natural;
身体：
type Some_Record_Type is
record
X_Count: Natural;
X : X_Bounded_Array_Type;
Y_Count: Natural;
Y : Y_Bounded_Array_Type;
...
end record;
function Record_Field_X(Record: Some_Record_Type) return X_Unbounded_Array_Type
is (
...
a bit of logic based on values of other …我有一个大约的数据结构（我无法分享完整的源代码，但可以根据要求提供其他信息）如下：
generic
type Item_Type is private;
package Util.Pool is
type Pool is limited new Ada.Finalization.Limited_Controlled with private;
procedure Get_Available (From: in out Pool; Available: out Natural);
overriding procedure Finalize (Object: in out Pool);
private
type Item_Array is array (Positive range <>) of Item_Type;
type Item_Array_Access is access all Item_Array;
Null_Item_Array: constant Item_Array_Access := null;
protected type Protected_Pool is
function Get_Available return Natural;
private
Available: Natural := 0;
Items: Item_Array_Access := Null_Item_Array;
end Protected_Pool;
type Pool is limited new Ada.Finalization.Limited_Controlled with …在Learning Ada的第 22.1 章中，尝试构建示例。
它期望安装 GNATprove。我使用的是 Ubuntu 18.04 LTS，但没有看到任何提供它的软件包。当我尝试查找主存储库时，我发现的只是Open Do中的内容，当我单击下载按钮时，它似乎是一个损坏的链接。Google 几乎没有提供有关 GNATprove 的信息，这有点令人担忧。
我是 Ada 新手，所以我真的不知道应该使用什么，所以如果 GNATprove 不正确，请告诉我。我通常也期望有一个免费的软件工具链——这是一个合理的期望还是我应该期望需要“专业”版本来了解 Ada/SPARK 的全部内容？
我正在使用 GNAT 构建我的 Ada/SPARK 项目，并且使用链接器脚本。以下是摘录：
SECTIONS
{
.code :
{
. = ALIGN(0x4);
*(.text.section1)
_end_of_section1 = .;
*(.text.section2)
...
}
}
符号 _end_of_section1 是两个节之间的地址。我希望能够在我的 Ada 代码中访问它。我知道在 C 中使用extern char _end_of_section1[];. 在 Ada 中可以做这样的事情吗？如果没有，是否有其他方法可以在代码中获取该地址？
我正在使用 Ravenscar 配置文件构建一个利用任务的应用程序。
举一个简单的例子，我有一个任务有一个屏障，因此它仅在屏障为 True 时执行。
但是，我注意到，如果主控制线程正在执行，然后屏障设置为 true（从而释放），则任务将阻止主线程的执行，直到屏障再次关闭。
我正在研究 NRF52840 芯片。我应该注意，每当我将应用程序（没有修改）定位到 Native 时，这个问题就不会发生，并且任务不会阻止执行。
为了在嵌入式设备上启用 ravenscar（完整）RTS 的并行执行，我需要做些什么吗？
一些额外的颜色：如果我向任务循环添加延迟，它确实允许主控制线程运行。
这可能是优先级上限协议的问题吗？板上的处理器只有一个核心，所以我想知道这是否可能是问题所在——也就是说，该任务不允许主任务抢占，除非它正在休眠。
我尝试搜索文档和代码，但我无法找到这是什么以及如何纠正它。
设想：
我正在使用 Ada SPARK 矢量库，并且有以下代码：
package MyPackage
with SPARK_Mode => On
is
package New_Vectors is new Formal_Vectors (Index_Type => test, Element_Type => My_Element.Object);
type Object is private;
private
type Object is
record
Data : New_Vectors.Vector (Block_Vectors.Last_Count);
Identifier : Identifier_Range;
end record;
当代码调用时我收到错误：
function Make (Identifier : Identifier_Range) return Object is
begin
return (
Data => New_Vectors.Empty_Vector,
Identifier => Identifier);
end Make;
指向Empty_Vector。困难在于Empty_Vector定义似乎导致问题的“ Capacityas” 。0现在我不确定如何处理似乎Capacity在类型定义中的情况（已查看a-cofove.ads）。
所以基本上我不知道如何解决这个问题；或者如何在未来发现这种情况发生。
我目前正在大学实时编程语言课程中学习 Ada，并且有一个关于 SPARK 的问题。
我正在开发一个项目，其任务是监视离网电源。这项任务对于机器安全至关重要，因此应该尽可能没有错误，经过 SPARK 验证。
我收到这个奇怪的错误，我无法找到修复方法11:14 tasking in SPARK requires sequential elaboration (SPARK RM 9(2)) violation of pragma SPARK_Mode
原始代码有点长，但我能够通过一个最小的示例得到相同的错误。
规格：
pragma Profile (Ravenscar);
pragma SPARK_Mode;
with System;
package simple_monitoring is
function sign (val : in Float) return Float
with Pre => val >= 10.0;
task type myTask is
end myTask;
end simple_monitoring;
实施：
pragma Profile (Ravenscar);
pragma SPARK_Mode;
with Ada.Real_Time; use Ada.Real_Time;
with Ada.Text_IO; use Ada.Text_IO;
package body simple_monitoring is
function sign (val : in Float) …我可以理解这段代码中前置条件的含义和目的，但在理解后置条件的含义和目的方面遇到问题。我知道Push这部分在推入整数后增加指针（Pointer = Pointer~ +1）。我理解Pop这部分是在弹出整数后减少指针（Pointer=Pointer~ - 1）。
package Stack
--# own S, Pointer;
--# initializes S, Pointer;
with SPARK_Mode
is
pragma Elaborate_Body(Stack);
Stack_Size : constant := 100;
subtype Pointer_Range is Integer range 0 .. Stack_Size;
subtype Index_Range is Pointer_Range range 1..Stack_Size;
type Vector is array(Index_Range) of Integer;
S : Vector;
Pointer : Pointer_Range;
function isEmpty return Boolean;
--# global in Pointer;
procedure Push(X : in Integer);
--# global in out S, Pointer;
--# derives S from S, …