Perguntas[verification](coding)

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ê?

Eu gostaria de contar os elementos em um Dafny que são definidos abaixo de um limite, mas não consigo descobrir o 'garantir'.

method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
  ensures count == |{i in numbers | i < threshold}|
{
  count := 0;
  var ss := numbers;
  while ss != {}
    decreases |ss|
  {
    var i: int :| i in ss;
    ss := ss - {i};
    if i < threshold {
      count := count + 1;
    }

  }
}

method Main()
{
  var s: set<int> := {1, 2, 3, 4, 5};
  var c: int := CountLessThan(s, 4);
  print c;
  // assert c == 3;

}

O erro é:this operator chain cannot continue with an ascending operator