KeY prover无法验证数组元素交换为原数组排列的问题排查

问题背景 #

参考《KeY textbook》第16章SortPerm类实现插入排序拆分时，遇到swap方法验证的核心问题：

• 注释的ensures \dl_seqPerm(seqa, \old(seqa))无法被KeY prover证明，且出现反例
• 使用\dl_array2seq(a)的同逻辑约束（ensures \dl_seqPerm(\dl_array2seq(a), \old(\dl_array2seq(a)))）可正常证明
• 即使约束输入为[0,1]且i≠j，添加seqa的排列约束后仍失败，同时无法理解反例格式

一、为何ensures \dl_seqPerm(seqa, \old(seqa))证明失败 #

1. 序列变量与数组的绑定缺失
   如果seqa是方法内维护的独立序列变量，且没有显式的不变式约束（比如seqa == \dl_array2seq(a)），KeY无法自动推导seqa的状态变化与数组swap操作的关联。而\dl_array2seq(a)直接基于数组状态生成序列，\old(\dl_array2seq(a))明确对应数组交换前的序列，prover能直接匹配数组元素交换对排列性的保持规则。

2. 快照捕获的逻辑差异
   \old(seqa)捕获的是方法执行前seqa的初始状态，但如果seqa在swap执行过程中被直接修改（而非同步数组a的变化），prover无法确认这种修改是否符合排列规则。而\dl_array2seq(a)的快照完全依赖数组的状态，swap操作对数组的修改是明确的元素交换，prover能直接验证其排列性。

3. 元素域的隐式不一致
   \dl_seqPerm的排列验证依赖序列元素域的一致性，若seqa的元素域（比如允许null、额外元素）与\dl_array2seq(a)的隐式域（仅数组内的元素）存在差异，prover无法匹配排列规则，导致证明失败。

二、KeY反例的解读方式 #

KeY生成的反例是一组违反约束的状态赋值，核心是展示prover找到的“约束不成立的场景”，格式通常包含以下部分：

• 初始状态：方法参数（数组a、索引i/j）、序列变量seqa的初始值
• 执行后状态：数组a、序列变量seqa的最终值

举个典型反例场景：

初始状态：a = [0, 1]，i=0，j=1，seqa = [0, 0]（与数组状态不一致）
执行后状态：a = [1, 0]，seqa = [1, 1]
此时\dl_seqPerm(seqa, \old(seqa))不成立，因为[1,1]和[0,0]并非排列关系——这就是prover找到的反例，本质是因为你没有约束seqa与a的同步关系，prover会枚举所有可能的初始状态，包括两者不一致的情况。

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