getting counterexamples

Apr 14, 2016 at 9:50 PM
Is it possible to get counterexamples from the web interface? I am having trouble realizing why the following code does not check out:
class KV 
{
  var key : int;
  var value : int;
  constructor (k: int, v: int) modifies this
  {
    this.key := k;
    this.value := v;
  }
}

method mapper (s: seq<int>) returns (l: seq<KV>)
ensures |s| == |l|
ensures forall i: int :: 0 <= i < |s|  ==> 
   l[i] != null && l[i].key == 0
{  
  if |s| == 0 
  { l := []; }
  else 
  {
    var v := new KV(0, 0);
    var v2 := mapper(s[1..]);
    l := [v] + v2; 
  } 
}
Thanks!
Marked as answer by gropherd on 4/14/2016 at 6:07 PM
Apr 15, 2016 at 1:07 AM
Got it. Please ignore.