Verification Error (ghost vs non-ghost)

Apr 18, 2013 at 10: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>; := name; := date;

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

} //end of the class
Apr 18, 2013 at 9: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.