ada - Ada 约束错误:判别检查失败。这是什么意思?
问题描述
我已经尝试搜索文档和代码,但我无法找到这是什么以及如何更正它。
设想:
我正在使用 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
定义似乎导致问题的原因Capacity
。0
现在我不确定如何处理Capacity
似乎在类型定义中的问题(已经查看过a-cofove.ads
)。
所以基本上我被困在如何解决这个问题上;或者相当如何发现未来发生的这种情况。
解决方案
你的分析是正确的。发生错误是因为您尝试将空向量(即容量为 0 的向量)分配给具有容量的向量Block_Vectors.Last_Count
(似乎非零)。
您实际上不需要显式初始化向量即可使用它。默认初始化(使用<>
,例如,参见此处)就足够了,如下面的示例所示。
但是,为了证明不存在运行时错误,您确实需要使用Clear
. 然后,该Empty_Vector
函数可用于检查向量是否为空的断言,如下例所示。该示例可以显示为没有运行时错误,使用gnatprove
. 例如,通过 GNAT Studio 中的菜单 SPARK > Prove 打开证明设置,在“常规”部分(左上角)选择“报告检查已移动”,然后通过选择“执行”(右下角)运行分析。
主文件
with Ada.Text_IO; use Ada.Text_IO;
with Ada.Containers.Formal_Vectors;
procedure Main with SPARK_Mode is
package My_Vectors is new Ada.Containers.Formal_Vectors
(Index_Type => Natural,
Element_Type => Integer);
use My_Vectors;
type Object is record
Data : Vector (Capacity => 10); -- Max. # of elements: 10
Value : Integer;
end record;
-- Initialize with default value (i.e. <>), no explicit initialization needed.
Obj : Object :=
(Data => <>,
Value => 42);
begin
-- Clear the vector, required for the assertions to be proven.
Clear (Obj.Data);
-- Assert that the vector is not empty.
pragma Assert (Obj.Data = Empty_Vector);
-- Populate the vector with some elements.
Append (Obj.Data, 4);
Append (Obj.Data, 5);
Append (Obj.Data, 6);
-- Assert that the vector is populated.
pragma Assert (Obj.Data /= Empty_Vector);
-- Show the contents of Obj.Data.
Put_Line ("Contents of Obj.Data:");
for I in Natural range 0 .. Natural (Length (Obj.Data)) - 1 loop
Put_Line ("[" & I'Image & "]" & Element (Obj.Data, I)'Image);
end loop;
New_Line;
-- or, alternatively using an iterator ...
declare
I : Extended_Index := Iter_First (Obj.Data);
begin
while Iter_Has_Element (Obj.Data, I) loop
Put_Line ("[" & I'Image & "]" & Element (Obj.Data, I)'Image);
I := Iter_Next (Obj.Data, I);
end loop;
end;
New_Line;
-- Show the contents of Obj.Value.
Put_Line ("Contents of Obj.Value:");
Put_Line (Obj.Value'Image);
New_Line;
end Main;
输出
Contents of Obj.Data:
[ 0] 4
[ 1] 5
[ 2] 6
[ 0] 4
[ 1] 5
[ 2] 6
Contents of Obj.Value:
42
推荐阅读
- scala - 无法使用 Intellij 导入 spark.implicit._
- excel - 用递增值填充列单元格的公式 (LibreOffice)
- hyperledger-fabric - 无法在超级账本作曲家中执行交易
- c++ - Kinect 的 Xbox 360
- wpf - WPF - 清除 TabControl 的所有 TabItem 中的所有文本框
- ios - 从另一个应用程序打开 Safari 的深层链接
- python - 将 utf-8 参数作为参数传递给 python 文件
- c - C 中的嵌套 While 循环
- android - 片段中的 Asynctask 未到达 onPostExecute
- javascript - Jquery FullCalendar 通过 jquery events 获取事件 id