时间戳

首页 > 解决方案 > 达芙妮。另一种调用情况可​​能违反上下文的修改子句

dafny - 达芙妮。另一种调用情况可​​能违反上下文的修改子句

问题描述

我在这里和维基上阅读了很多关于此的问题，但我无法解决这个“调用可能违反上下文的修改子句”的情况。你可以帮帮我吗？我正在尝试将问题的实例从主方法发送到“求解器”，当我调用该solve()方法时，我收到了这个错误，我不明白为什么。https://rise4fun.com/Dafny/53q6

class Stack {
  var x : array<int>;

  constructor()
    ensures fresh(x); 
  {
    x := new int[10];
  }
}

class Formula {
  var stack : Stack;

  constructor()
    ensures fresh(stack);
    ensures fresh(stack.x);
  {
    stack := new Stack();
  }
}

class Solver {
   var f : Formula;

  constructor(f' : Formula)
  {
    this.f := f';
  }

  method solve()
    modifies f.stack;

    ensures old(f.stack.x) == f.stack.x;
  {}
}

method Main() {
  var f := new Formula();
  var a := new Solver(f);
  assert fresh(f);
  assert fresh(f.stack);
  assert fresh(f.stack.x);
  assert fresh(a);
  a.solve();
}

标签： dafny

解决方案

您缺少后置条件

ensures f == f'

在类的构造函数上Solver。

（由于构造函数是方法，Dafny 在推理其他方法时不会“查看内部”它们的主体，因此您需要这个后置条件来暴露主体。）

推荐阅读