Dafny大步断言违规

Question

我对达夫尼来说是个新手。我试图为Dafny中的CinK提供一个可执行的大步语义规范。

下面是我的代码

datatype Id = a | b | c |d |m

//expresions
datatype Exp =
Int(i: int)
| Var(x: Id)
| Bool(b:bool)
| Plus(e1: Exp, e2: Exp)

//statements
datatype Stmt =
Assg(x: Id, e: Exp)



// evaluation of expressiosn
function method val(e: Exp, state: map<Id, int>) : int
decreases  e, state
{
match (e) {
case Int(i) => i
case Bool(b) => if b== true then 1 else 0
case Var(a) => if a in state then state[a] else 0
case Plus(e1, e2) => val(e1, state) + val(e2, state)
}
}


lemma Lemma1(state: map<Id, int>)
requires state == map[a := 2, b := 0]
ensures val(Plus(Var(a), Int(5)), state) == 7
{
}


// statement evaluation
function method bigStep(s: Stmt, state: map<Id, int>) : map<Id, int>
decreases s,state
{
match (s) {
case Assg(x, e) => state[x := val(e, state)]
}

}

function method bigStepStmtlist(s: seq<Stmt>, state: map<Id, int>,pos:int) : map<Id, int>
requires 0 <=pos <= |s|
decreases |s|-pos
{

if(pos==|s|) then state else bigStep(s[pos],bigStepStmtlist(s,state,pos+1)) 

}


method Lemma2(state: map<Id, int>)
{
var state := map[a := 2, b := 0,c:=3,d:=5];
assert bigStep(Assg(b, Plus(Var(a), Int(5))), state) == map[a := 2, b := 7,c:=3,d:=5];
assert bigStep(Assg(b, Int(8)), state) == map[a := 2, b := 8,c:=3,d:=5];

}


method Main() {
var state := map[a := 2, b := 1,m:=0];

var Stmt1 :=Assg(a,Int(1));
var Stmt2 :=Assg(b,Int(2));
var Stmt3 :=Assg(m,Int(3));

var Stmts:= new Stmt[3];
Stmts[0]:=Stmt1;
Stmts[1]:=Stmt2;
Stmts[2]:=Stmt3;

var t:= bigStepStmtlist(Stmts[..],state,0); 

print t;// this will print map[Id.a := 1, Id.b := 2, Id.m := 3]

assert t== map[Id.a := 1, Id.b := 2, Id.m := 3];

}

如果运行此命令，您将看到print测试将打印mapId.a := 1、Id.b := 2、Id.m := 3，但我无法通过任何断言...

我也尝试过使用while循环来实现这一点，但是它似乎不适用于断言

Answer 1

Dafny验证器愿意在进行证明时扩展函数定义，但在一定范围内。如果它没有，那么当你要求它证明一些不成立的东西时，它就不能给你快速的周转。将验证器看作是扩展您编写一次的函数的每个事件，这可能是有帮助的。它实际上做得更多。例如，当函数的参数是文字时，验证器可能会将函数扩展到超出正常限制的范围。(如果您对这种“双轨编码”的细节感兴趣，请参阅Amin、Leino和Rompf，点击2014。)

为了证明你的断言，你必须帮助验证者。在断言之前添加以下证明计算，您的程序将进行验证：

calc {
  bigStepStmtlist(Stmts[..], state, 0);
==  // def. bigStepStmtlist
  bigStep(Stmts[0], bigStepStmtlist(Stmts[..], state, 1));
==  // def. bigStepStmtlist
  bigStep(Stmts[0],
    bigStep(Stmts[1], bigStepStmtlist(Stmts[..], state, 2)));
==  // def. bigStepStmtlist
  bigStep(Stmts[0],
    bigStep(Stmts[1],
    bigStep(Stmts[2], bigStepStmtlist(Stmts[..], state, 3))));
==  // def. bigStepStmtlist
  bigStep(Stmts[0],
    bigStep(Stmts[1],
    bigStep(Stmts[2], state)));
==  // def. Stmts and state
  bigStep(Assg(a, Int(1)),
    bigStep(Assg(b, Int(2)),
    bigStep(Assg(m, Int(3)), map[a := 2, b := 1, m := 0])));
==  { assert bigStep(Assg(m, Int(3)), map[a := 2, b := 1, m := 0])
          == map[a := 2, b := 1, m := 0][m := 3]
          == map[a := 2, b := 1, m := 3]; }
  bigStep(Assg(a, Int(1)),
    bigStep(Assg(b, Int(2)), map[a := 2, b := 1, m := 3]));
==  { assert bigStep(Assg(b, Int(2)), map[a := 2, b := 1, m := 3])
          == map[a := 2, b := 1, m := 3][b := 2]
          == map[a := 2, b := 2, m := 3]; }
  bigStep(Assg(a, Int(1)), map[a := 2, b := 2, m := 3]);
==  { assert bigStep(Assg(a, Int(1)), map[a := 2, b := 2, m := 3])
          == map[a := 2, b := 2, m := 3][a := 1]
          == map[a := 1, b := 2, m := 3]; }
  map[a := 1, b := 2, m := 3];
}

这是一个详细的证明。您只需要提供前几个步骤，验证器就可以完成其余的工作。

我在上面说过，当使用文字参数调用函数时，验证器愿意超出其正常限制。这不适用于calc语句中的第一个表达式，因为该表达式用子表达式Stmts[..]解除了对堆的引用。如果不需要堆提供的数组，那么使用数学序列会更容易。事实上，在这个项目中

var stmts := [Assg(a,Int(1)), Assg(b,Int(2)), Assg(m,Int(3))];
assert bigStepStmtlist(stmts, state, 0) == map[a := 1, b := 2, m := 3];

bigStepStmtList的所有参数都是文字，因此断言是自动验证的。

鲁斯坦