SPARK功能正确性证明：CR类型问题与后置条件修改咨询

一、CR类型导致SPARK证明失败的原因 #

• CR类型的不变式约束未被充分描述：如果CR是带不变式的自定义类型（比如要求内容长度在特定范围），而操作CR的函数后置条件未明确保证操作后仍满足该不变式，SPARK验证器无法自动推导这一点，导致证明失败。
• 函数合约的后置条件缺失关键关联：比如处理CR类型的填充函数，若未明确输出与输入的内容关联（如原始内容保留、填充字符的范围），SPARK无法确认功能正确性，会因“无法证明某属性成立”报错。
• CR类型的内部字段依赖未被建模：如果CR包含多个关联字段（如内容字符串和长度字段），函数操作时未同步更新这些字段，或后置条件未说明字段间的一致性，SPARK会认为存在状态不一致的风险。

二、修改后置条件以完成SPARK证明的方法 #

假设你的函数是为CR类型的内容填充至最小长度，以下是具体修改方向：

1. 明确长度约束：在后置条件中直接关联输入输出的长度，例如：

   function Pad_CR(Input : CR) return CR is
   begin
      -- 填充逻辑
   end Pad_CR;
   

   后置条件需补充：

   with
     Post => Pad_CR'Result.Length >= Minimum_Length
     and then (if Input.Length >= Minimum_Length then Pad_CR'Result = Input);
   

2. 描述内容一致性：明确原始内容被完整保留，填充部分为指定字符，使用for all量化语句：

   with
     Post => (for all I in 1 .. Input.Length =>
               Pad_CR'Result.Content(I) = Input.Content(I))
     and then (for all I in Input.Length+1 .. Pad_CR'Result.Length =>
               Pad_CR'Result.Content(I) = ' ');
   

3. 绑定类型不变式：如果CR类型有不变式（如CR'Class的Valid属性），需在后置条件中保证结果满足不变式：

   with
     Post => Pad_CR'Result.Valid;
   

4. 细化前置条件：若函数仅需处理长度不足的输入，可补充前置条件缩小验证范围，降低证明难度：

   with
     Pre => Input.Length < Minimum_Length,
     Post => Pad_CR'Result.Length = Minimum_Length;
   

三、输入需至少220个字符的原因 #

• 类型不变式强制要求：若CR类型的定义中，不变式明确要求内容长度≥220，输入长度不足会直接违反前置条件，导致SPARK验证不通过。
• 填充逻辑的边界适配：可能你的填充逻辑依赖特定长度阈值（如220是内存对齐、协议要求或业务规则规定的最小长度），当输入小于该值时，填充后的结果需要触发特定分支，而SPARK在证明该分支的正确性时，需要输入满足一定长度才能完成推导。
• 测试或合约的遗留约束：220可能是初始测试用例中设定的阈值，后续未调整，导致输入长度要求被固化在函数的前置条件或类型定义中。

内容的提问来源于stack exchange，提问作者Jeffrey R. Carter