Início / coding / Perguntas / 77104592
Accepted
MogicFrog
Asked: 2023-09-14 19:47:30 +0800 CST

Um predicado estranho que não pode provar uma afirmação já definida no corpo

  • 772

Suponha que temos um tipo de dados chamado Treee uma função sizepara calcular seu tamanho

datatype Tree = Empty | Node(key: int, left: Tree, right: Tree)
function size(t: Tree): (s: nat)
{
  match t
  case Empty => 0
  case Node(_, l, r) => size(l) + size(r) + 1
}

Agora, por alguns motivos, quero deixar esta árvore ser de alguma forma “equilibrada”. Especificamente, isso é

predicate alpha_weight_balanced(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
{
  if t == Empty then true
  else
    size(t.left) as real <= alpha*(size(t) as real)
    && size(t.right) as real <= alpha*(size(t) as real)
    && alpha_weight_balanced(t.left,alpha)
    && alpha_weight_balanced(t.right,alpha)
}

Quando alpha_weight_balancedmantido, o tamanho de cada filho da árvore té menor que alpha*size(t). E naturalmente, este lema deve ser válido

lemma test(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
  requires alpha_weight_balanced(t, alpha)
  requires t != Empty
  ensures size(t.left) as real <= alpha*(size(t) as real)
{}

No entanto, Dafny não conseguiu provar esse lema “óbvio”. Eu até tentei embrulhar sizecomo

function f(a: int): int
// there is no implemetion for `f`

predicate alpha_weight_balanced(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
{
  if t == Empty then true
  else
    f(size(t.left)) as real <= alpha*f(size(t)) as real
    && f(size(t.right)) as real <= alpha*f(size(t)) as real
    && alpha_weight_balanced(t.left,alpha)
    && alpha_weight_balanced(t.right,alpha)
}

lemma test(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
  requires alpha_weight_balanced(t, alpha)
  requires t != Empty
  ensures     f(size(t.left)) as real <= alpha*f(size(t)) as real
              && f(size(t.right)) as real <= alpha*f(size(t)) as real
{
}

E Dafny prova isso com sucesso. Mas se eu modificar a funçãof

function f(a: int): int
ensures f(a) == a

A prova falhou novamente.

Estou tão confuso sobre isso, alguém sabe por quê?

verification

1 respostas

  1. Best Answer

    Uma maneira de evitar falhas na verificação é ocultar a multiplicação de números reais dentro da função. O motivo pelo qual você não exige isso ao fazer essa verificação em nat e int é que o dafny faz isso automaticamente para você.

    datatype Tree = Empty | Node(key: int, left: Tree, right: Tree)

function size(t: Tree): (s: nat)
{
  match t
  case Empty => 0
  case Node(_, l, r) => size(l) + size(r) + 1
}

function multiply(a: real, b: real): real { a * b }

predicate alpha_weight_balanced(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
{
  if t == Empty then true
  else
    size(t.left) as real <= multiply(alpha, size(t) as real)
    && size(t.right) as real <= multiply(alpha, size(t) as real)
    && alpha_weight_balanced(t.left,alpha)
    && alpha_weight_balanced(t.right,alpha)
}

lemma test(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
  requires alpha_weight_balanced(t, alpha)
  requires t != Empty
  ensures size(t.left) as real <= multiply(alpha, size(t) as real)
{}
    • 1

relate perguntas