Dafny Big-Step- Утверждают нарушение

Я новичок в Дафни. Я пытаюсь дать исполняемую спецификацию семантики больших шагов для CinK в Dafny.

Итак, вот мой код

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, но, похоже, это не сработает с утверждениями.


dafny
person exces97    schedule 12.01.2020    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Верификатор Дафни готов расширить определения функций при выполнении доказательства, но в некоторых пределах. Если бы это было не так, то он не мог бы дать вам быстрый ответ, когда вы просите его доказать что-то, что не соответствует действительности. Может быть полезно думать о верификаторе как о расширении каждого экземпляра функции, которую вы пишете один раз. На самом деле делает больше. Например, когда аргументы функции являются литералами, верификатор может расширить функцию за пределы обычных пределов. (См. Amin, Leino, and 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 являются литералами, поэтому утверждение проверяется автоматически.

Рустан

person Rustan Leino    schedule 13.01.2020
comment
спасибо! Я пытался сделать это с помощью цикла while и пытался использовать этот рекурсивный метод, чтобы проверить время. Теперь я всегда буду помнить разницу между последовательностью и массивом - person exces97; 14.01.2020
comment
учитывая, что я хочу изменить один элемент в stmts, чтобы он был Assg(m,Plus(Var(a),Int(2)) что, очевидно, выведет ту же карту map[Id.a:= 1, Id.b:= 2 , Id.m := 3] опять же в ассертах не получится даже с seq... Что тут делать? - person exces97; 14.01.2020