如何确保File_Reader中记录的判别式值与另一记录组件值相等？

我需要实现一个包含File和Buffer两个记录的File_Reader，要求初始化时必须保证Data_File.IO_Buffer_Size等于Data_In.Size。目前直接在记录初始化里引用Data_In.Size会报错，尝试过静态谓词但未成功，动态谓词在LightRuntime环境下无法正常工作。我可以给File_Reader添加Buffer_Size判别式，但想探索其他替代方案；另外因为记录通过未展示的表示子句做了内存映射，必须保留现有布局。

给出的代码结构：

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); -- 此处无法正常工作
   end record;

1. 工厂函数封装初始化逻辑 #

既然无法在记录默认初始化里直接引用同记录的其他组件，最直接的方式是写一个工厂函数创建File_Reader实例，从根源保证两个值一致，同时完全保留原有记录布局：

function Create_File_Reader(
   Name : String;
   Buffer_Size : Buffer_Size := 300) return File_Reader is
begin
   return Result : File_Reader(Name) do
      Result.Data_In := Buffer'(Size => Buffer_Size, others => <>);
      Result.Data_File := (Name => Name, IO_Buffer_Size => Buffer_Size);
   end return;
end Create_File_Reader;

所有创建File_Reader的操作通过该函数进行，即可确保Data_File.IO_Buffer_Size与Data_In.Size始终匹配。

2. 固定默认大小场景的同步初始化 #

如果大部分场景使用默认的300大小，可以直接在记录定义中同步默认值：

type File_Reader(Name : String) is 
   record        
       Data_In      : Buffer(Size => 300);    
       Data_File    : File := (Name, 300); -- 与Data_In的默认Size保持一致
   end record;

这种方式仅适用于默认大小固定的场景，动态指定大小仍推荐使用工厂函数。

3. 显式按顺序初始化（需谨慎） #

Ada允许后续记录组件引用已初始化的前置组件，可通过显式初始化顺序保证一致性，但依赖外部操作的正确性，容易出现人为失误：

-- 记录定义去掉Data_File的默认初始化
type File_Reader(Name : String) is 
   record        
       Data_In      : Buffer;    
       Data_File    : File;
   end record;

-- 创建实例时严格按顺序初始化
declare
   Reader : File_Reader("test.txt");
begin
   Reader.Data_In := Buffer'(Size => 500, others => <>);
   Reader.Data_File := (Name => Reader.Name, IO_Buffer_Size => Reader.Data_In.Size);
end;

• 所有方案均未修改原有记录的布局结构，适配内存映射的要求。
• 静态谓词失效是因为Data_In.Size是运行时确定的判别式值，编译期无法验证约束，因此静态谓词无法覆盖该场景。
• 工厂函数是最可靠的替代方案，既保证约束，又不依赖LightRuntime不支持的动态谓词检查。

内容的提问来源于stack exchange，提问作者ATL_DEV