CODEWITHSUNDEEP
dafny
exces97
exces97

Reputation: 13

Dafny Big-Step- Assert violation

I'm kind of new to Dafny. What I'm trying to is to give an executable specification of the big-step semantics for CinK in Dafny .

So here is my code 

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];

}

If you run this you will see that print t will print that map[Id.a := 1, Id.b := 2, Id.m := 3] but I cannot reach that by any assertion...

I tried to also do this with while loop but seems it won't work with the assertions

Upvotes: 0

Views: 178

Answers (1)

Rustan Leino
Rustan Leino

Reputation: 2087

The Dafny verifier is willing to expand function definitions when doing a proof, but within some limits. If it did not, then it could not give you quick turnaround when you ask it to prove something that doesn't hold. It may be helpful to think of the verifier as expanding each occurrence of a function that you write once. It actually does more. For example, when the arguments to a function are literals, then the verifier may expand a function beyond the normal limits. (See Amin, Leino, and Rompf, TAP 2014, if you're interested in the details of this "dual-rail encoding".)

To prove your assertion, you'll have to help the verifier along. Add the following proof calculation before the assertion and your program will verify:

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];
}

This is a detailed proof. You only need to supply the first couple of steps, and the verifier can do the rest.

I said above that the verifier is willing to exceed its normal limits when a function is invoked with literal arguments. That doesn't apply to the first expression in the calc statement, because that expression dereferences the heap with the subexpression Stmts[..]. If you don't need the arrays that the heap provides, then it's easier to work with mathematical sequences. Indeed, in the program

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];

all arguments to bigStepStmtList are literals, so the assertion is verified automatically.

Rustan

Upvotes: 1

Related Questions