Dafny Big-Step- 断言违规

Question

我对 Dafny 有点陌生。我正在尝试的是在 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 t 会打印那个地图 [Id.a := 1, Id.b := 2, Id.m := 3 ] 但我无法断言...

我也尝试用 while 循环来做到这一点，但它似乎不适用于断言

Answer 1

Dafny 验证者愿意在做证明时扩展函数定义，但在一定范围内。如果它没有，那么当你要求它证明一些不成立的东西时，它不能给你快速的周转。将验证器视为扩展您编写一次的函数的每次出现可能会有所帮助。它实际上做得更多。例如，当函数的参数是文字时，验证器可能会将函数扩展到正常限制之外。（如果您对此 "dual-rail encoding" 的详细信息感兴趣，请参阅 Amin、Leino 和 Rompf，TAP 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 的所有参数都是文字，因此自动验证断言。

鲁斯坦

Dafny Big-Step- 断言违规

Dafny Big-Step- Assert violation

dafny