Дафни Биг-Степ- Утверждение нарушения - PullRequest
Новая
       12

Дафни Биг-Степ- Утверждение нарушения

0 голосов
/ 12 января 2020

Я новичок в Дафни. Я пытаюсь дать исполняемую спецификацию семантики большого шага для 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];

}

Если вы запустите это, вы увидите эта печать t напечатает эту карту [Id.a: = 1, Id.b: = 2, Id.m: = 3], но я не могу достичь этого ни одним утверждением ...

Я пытался также сделайте это с while l oop, но, похоже, он не будет работать с утверждениями

1 Ответ

0 голосов
/ 13 января 2020

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

Rustan

...