Verification Failing

Apr 30, 2013 at 10:48 AM
Edited May 1, 2013 at 11:32 AM
Hi Rustan,

can you please tell me why this simple code is not being verified. I am adding an element in to sequence and array and then trying to compare the length and elements of these two.
many thanks !

ghost var names_a: seq<A>;
ghost var dates_a: seq<B>;
ghost var Repr: set<object>;
ghost var elems: seq<Data<A,B>>;

//initialize function
method Init(name:array<A>,date:array<B>,name_date:array<Data<A,B>>)
requires name_date != null && name != null && date != null;
requires name_date.Length >= 0 && name.Length == date.Length && name_date.Length == name.Length;
modifies this;
ensures fresh(Repr - {this});
ensures Valid(name,date,name_date);
{

names_a := name[..];
dates_a := date[..];
Repr := {this};
elems := name_date[..];
}



//validity function
function Valid(name:array<A>,date:array<B>,names_c:array<Data<A,B>>) : bool
reads this, Repr, names_c, name, date, elems;
requires name != null && date != null && names_c != null;
requires name.Length == date.Length && name.Length == names_c.Length;
{
this in Repr &&
|names_a| == |dates_a| && |elems| == |names_a| &&
names_c.Length == |elems| &&    //here it is giving error that these two are not equal
(forall i :: 0 <= i && i < |names_a| ==>
   name[i] == names_a[i] && 
   date[i] == dates_a[i] &&
   elems[i] == names_c[i])
}


//add method
method Add(name: NAME, date: DATE, namearr:array<NAME>,datearr:array<DATE>,names_c:array<Data<NAME,DATE>>, index:int)
requires names_c != null && namearr != null && datearr != null;
requires names_c.Length >= 0 && namearr.Length == datearr.Length && names_c.Length == namearr.Length;
requires Valid(namearr,datearr,names_c);
requires 0<= index < names_c.Length;
modifies this, Repr, names_c;
ensures Valid(namearr,datearr,names_c); //this post condition is failing

{
 var h := new Data<A,B>;
 h.name := name;  
 h.date := date;  
 names_a := [name] + names_a;  
 dates_a := [date] + dates_a;
 elems := [h] + elems;
 names_c[index] := h;
 Repr := Repr + {h};      //adding the objects in the set    
}

class Data<A,B>
{
var a : A;
var b : B;
}
May 5, 2013 at 9:23 PM
Hi Rustan,

any help !

thanks
-asif