Нахождение минимума набора результатов рекурсии - PullRequest
Новая
       26

Нахождение минимума набора результатов рекурсии

0 голосов
/ 14 января 2020

Я кодирую редактируемое уравнение расстояния в Дафни.

Я думаю Я получил подтверждение, но мне любопытно, если есть более сжатое способ представления выбора, который повторение выбирает из трех вариантов редактирования: 

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

В Dafny: 

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

Полный источник здесь .

1 Ответ

1 голос
/ 15 января 2020

Если вы определите 

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, min(b, c)) <= b; 
  assert min(a, min(b, c)) <= c; 
  assert min(a, min(b, c)) == a || min(a, min(b, c)) == b || min(a, min(b, c)) ==c;

Вы говорите, что, как вы думаете, вы подтвердили это. Но то, что я вижу, - это файл Dafny, содержащий только определение функции и несколько тестов. В этом случае проверяется только четко определенная индуктивная функция и эти несколько тестовых случаев. Вы имели в виду, что проверкой, или у вас также есть реализация, которая сверяется с этой функцией?

...