Ada constraint error: Discriminant check failed. What does this mean?

Question

我已经尝试搜索文档和代码，但找不到这是什么，因此找不到如何更正它。

场景：

我正在使用 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）。

所以基本上我不知道如何解决这个问题；或者如何在未来发现这种情况。

Answer 1

您的分析是正确的。发生错误是因为您试图将空向量（即容量为 0 的向量）分配给容量为 Block_Vectors.Last_Count（看起来非零）的向量。

您实际上不需要显式初始化向量即可使用它。默认初始化（使用 <>，例如，参见 here）就足够了，如下面的示例所示。

但是，为了证明不存在运行时错误，您确实需要使用Clear明确清除向量。然后 Empty_Vector 函数可用于检查向量是否为空的断言，如下例所示。使用 gnatprove 可以证明该示例没有运行时错误。例如，在 GNAT Studio 中通过菜单 SPARK > Prove 打开证明设置，在“常规”部分（左上角）中选择“报告检查已移动”，然后通过选择“执行”（右下角）运行进行分析.

main.adb

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

Ada constraint error: Discriminant check failed. What does this mean?

Ada constraint error: Discriminant check failed. What does this mean?

ada

spark-ada