This is the code for Bulls and Cows game, simply it just we have 2 array a[] and b[] with the same length, if a[i] == b[i] then Bulls = 1, if a[i] in b && a[i] != b[i] then Cows = 1.

I have written the Bulls and Cows function, but the method BullCows have some problem when calculate it, it make my assert fail.

`

function bullspec(s:seq<nat>, u:seq<nat>): nat
  requires |s| > 0
  requires |u| > 0
  requires |s| == |u|
{
  var index:=0;
  if |s| == 1 then (
    if s[0]==u[0] 
    then 1 else 0
  ) else (
    if s[index] != u[index] 
    then bullspec(s[index 1..],u[index 1..]) 
    else 1 bullspec(s[index 1..],u[index 1..])
    )
}

function cowspec(s:seq<nat>, u:seq<nat>): nat
  requires |s| > 0
  requires |u| > 0
  requires |s| <= |u|
{
  var extra:= |u|-|s|;
  var index:=0;
  if |s| == 1 then (
    if s[0] in u 
    then 1 else 0
  ) else(
    if s[index] in u && s[index]!=u[extra]
    then (1  cowspec(s[index 1..],u)) 
    else cowspec(s[index 1..],u)
  )
}

method BullsCows (s:seq<nat>, u:seq<nat>) returns (b:nat, c:nat)
  requires |s|>0 && |u|>0 &&|s|==|u|
  // No duplicates in array
  requires forall i, j | 0 <= i < |s| && 0 <= j < |s| && i != j :: s[i] != s[j]
  requires forall i, j | 0 <= i < |u| && 0 <= j < |u| && i != j :: u[i] != u[j]

  ensures forall k :: 0 <= k < |s| && s[k] !in u ==> b == c == 0
  ensures forall k :: 0 <= k < |s| && s[k] in u ==> (c   b) > 0
{
  var index := 0;
  b := 0;
  c := 0;
  while(index<|s|)
    invariant index <= |s|
    invariant forall k :: 0 <= k < index && s[k] in u ==> (b   c) > 0
    {
      if s[index] in u {
        if s[index] == u[index]{
          b:=b 1;
        } else {
          c:=c 1;
        }
      }
      index:=index   1;
    }
}


method NotMain()
{
  var sys:seq<nat> := [4,2,9,3,1];
  var usr:seq<nat> := [1,2,3,4,5];

  assert bullspec(sys, usr) == 1; //True
  assert cowspec(sys, usr) == 3; //True

  var b:nat, c:nat := BullsCows(sys, usr);
  assert b == 1; //Not true
  assert c == 3; //Not true
}

` The method NotMain said that assert b == 1; and assert c==3; are not true, this is Dafny language, please could someone help me with this logical, I'm banging my head.

I try put on many ensures in the BullsCows method but there's nothing happen

CodePudding user response：

The problem is that the postcondition on BullsCows() is not strong enough to prove the final two assertions. In particular, there is no connection between the operation of BullsCows() and the specifications bullspec() and cowspec(). You need to connect these things together.

To illustrate I'm going to use a simpler example which is easier to follow. As for your example above, the final assertion fails in the following:

function sumspec(xs: seq<nat>, i: nat) : nat
requires i <= |xs| {
    if |xs| == 0 || i == 0 then 0
    else sumspec(xs,i-1)   xs[i-1]
}

method sum(s:seq<nat>) returns (r:nat) {
    r := 0;
    for i := 0 to |s| {
        r := r   s[i];
    }
    return r;
}

method main() {
    assert sumspec([1,2,3],3) == 6;
    var r := sum([1,2,3]);
    assert r == 6;
}

Whilst sumspec() is a valid specification for sum() we have not connected these two things. As such, Dafny assumes that sum() can return any value for r!

To connect the specification (sumspec) with its implementation (sum) we need a stronger postcondition:

method sum(s:seq<nat>) returns (r:nat) 
ensures r == sumspec(s,|s|) {
    r := 0;
    for i := 0 to |s|
    invariant r == sumspec(s,i) {
        r := r   s[i];
    }
    return r;
}

Here, r == sumspec(s,|s|) connects the specification with the result of our implementation. We also added a loop invariant to help Dafny show this postcondition holds.