Verification Error (ghost vs non-ghost)

Apr 18, 2013 at 9:58 AM
HI Rustan,

thanks for recommendations and sorry for abstract question in previous thread. Please see my code below, where valid function is complaining to hold in add function. By looking with BVD i came to know that lengths for two sequences were never equal.


class BB<NAME(==), DATE(==)>
{


ghost var knownseq_a : seq<NAME>;
var names_c : seq<NAME>;
ghost var repr : set<object>

method Init()
modifies this;
ensures valid(); // ======here the function valid is okay======
{
knownseq_a := [];
names_c := [];

repr := repr + {this};
}


function valid():bool
reads this,repr;
{
//abstraction invariant
 forall i,j :: 0<= i < |knownseq_a| && 0 <= j < |names_c| ==> knownseq_a[i] == names_c[j]
}



method add(name:NAME, date:DATE)
modifies this, repr;
requires valid();
ensures valid() && fresh(repr - old(repr)); //=====Here it is complaining that valid() does not hold, because i added the objects in the sequences====

{
var b := new Data<NAME,DATE>;
b.name := name;
b.date := date;

knownseq_a := knownseq_a + [b.name];
names_c := names_c + [b.name];
repr := repr + {b};
}

} //end of the class
Coordinator
Apr 18, 2013 at 8:36 PM
Hi Asif,

Good, so BVD was of some help. You will then probably also notice that the quantifier you wrote in valid() says that knownseq_a and names_c consist of only one element. Here is a modification of your program--it may of may not be what you what, but it does verify. http://rise4fun.com/Dafny/NqYi

Rustan