找到一组递归结果中的最小值

2024-05-19 • 问答

我正在用Dafny编码edit distance递归方程。

我认为我已经对其进行了验证，但是我很好奇是否存在一种更简洁的方式来表示重复发生在三个编辑选择中的选择：

E(i,j) := min { 1 + E(i-1,j),1 + E(i,j-1),diff(i,j) + E(i-1,j-1) }

在达夫尼：

if 1 + recEdDist'(a,b,ai+1,bi) < 1 + recEdDist'(a,ai,bi+1) 
        && 1 + recEdDist'(a,bi) < diff(a[ai],b[bi]) + recEdDist'(a,bi+1)
then 1 + recEdDist'(a,bi) else
if 1 + recEdDist'(a,bi+1) < 1 + recEdDist'(a,bi) 
        && 1 + recEdDist'(a,bi+1) < diff(a[ai],bi+1) else
diff(a[ai],bi+1)

完整source here。

如果您定义

function min(a: int,b: int) : int
{ if a < b then a else b }

以下表达式给出了三个参数中的最小值：

min(1 + E(i-1,j),(min(1 + E(i,j-1),diff(i,j) + E(i-1,j-1))

如果您担心，达夫妮会向您证明这样的事情：

  assert min(a,min(b,c)) <= a; 
  assert min(a,c)) <= b; 
  assert min(a,c)) <= c; 
  assert min(a,c)) == a || min(a,c)) == b || min(a,c)) ==c;

您说您认为自己已通过验证。但是我看到的是一个仅包含函数定义和一些测试的Dafny文件。然后验证的只是归纳函数的明确定义和这几个测试用例。您的意思是通过验证，还是您也有针对此功能进行验证的实现？

找到一组递归结果中的最小值

ygzboy 回答：找到一组递归结果中的最小值

大家都在问