abstraction relation (ghost with Non-ghost fields)

Apr 16, 2013 at 12:04 PM
Hi Rustan,

Please can you tell why the below code is not being verified. Please note that knownseq_a is the abstract sequence (ghost) and known_c is the concrete sequence (non-ghost). I am trying to define the abstraction relation between these two.

"forall i,j :: 0<= i < |knownseq_a| && 0 <= j < |known_c| ==> knownseq_a[i] == known_c.knownseq_a[i] "

many thanks !
-asif
Coordinator
Apr 16, 2013 at 11:10 PM
Hi asif,

I don't understand what you're asking. First off, what is the type of "known_c"? The fact that you ask for its length (with the vertical bars) suggests that it is a sequence, but then you ask for its "knownseq_a" component (with the dot). Also, why do you quantify of j -- it seems that j is not used anywhere.

Here's one way to change your example to make it type check:
class MyClass {
  var knownseq_a: seq<int>;
  method M(known_c: MyClass)
    requires known_c != null && |knownseq_a| == |known_c.knownseq_a|;
  {
    assert forall i :: 0 <= i < |knownseq_a| ==> knownseq_a[i] == known_c.knownseq_a[i];
  }
}
Is this what you intended? This program does not verify, and there seems to be no reason to think that it would.

I'm thinking that you're doing an example that is too difficult for you. I suggest you may try to follow the Dafny Guide, to get some practice on programs that use simple types like integers and booleans. I expect that you'll be able learn something about reasoning about programs that way. Once you get a firm grip on what it means for a boolean condition to hold, then you may try some more advanced examples.

Rustan
Apr 17, 2013 at 3:28 PM
HI Rustan,

thanks for recommendations and sorry for abstract question. 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