如何确保一条记录的判别值等于另一个记录组件的值？

Question

我有一个由两个记录组成的File_Reader，File和Buffer。我想确保两个记录在初始化时始终具有有效的缓冲区大小，即Data_File.IO_Buffer_Size等于Data_In.Size。

我找不到用另一个记录的组件值或判别式初始化记录组件的值的方法，所以我想我至少会应用一个不成功的静态谓词。使用动态谓词作为替代方案会在 LightRuntime 环境中带来问题。

我可以轻松地将 Buffer_Size 判别式添加到 File_Reader，但我想探索替代解决方案。最后，必须保留记录布局，因为它们是使用未显示的表示子句进行内存映射的：

type File is 
   record
      Name           : String;
      IO_Buffer_Size : Buffer_Size;
   end record; 

type Buffer(Size : Buffer_Size := 300)  is         
   record
      Pos   : Buffer_Size := 0;
      Value : String(1 .. Size);
   end record;

type File_Reader(Name : String) is 
   record        
       Data_In      : Buffer;    
       Data_File    : File := (Name, Data_In.Size); -- Won't work
   end record;

Answer 1

您显示的代码还有一些其他错误，因此如果您的实际代码只有您所说的错误，那么它就不可能是您的实际代码。

首先，类型 File 无效，因为组件 File.Name 是一个 String，这是一个不受约束的数组类型，不允许用于记录的组件。您可能希望将其替换为某些有界 String 子类型或 Unbounded_String （但尝试为 Unbounded_String 创建表示子句会很困难并且似乎没有意义）。

其次，File_Reader 类型无效，因为它具有 String 类型的判别式 (File_Reader.Name)，这是复合类型，因此不允许用于判别式。

现在谈谈您的实际问题。如果您不为 File_Reader 提供 Buffer_Size 判别式，则缓冲区 (File_Reader.Buffer) 的大小将始终为 300（或 Buffer.Size 的默认值），因此您也可以将该值定义为常量，在 Buffer 类型和初始化 File_Reader.Data_File.IO_Buffer_Size 中使用它。 （顺便说一句，我不明白 File.IO_Buffer_Size 的用途：您无法从文件访问缓冲区（您需要 File_Reader），那么 File.IO_Buffer_Size 可以用来做什么？）

总而言之，我的建议是向 File_Reader 添加 Buffer_Size 判别式。