CODEWITHSUNDEEP
algorithmproofdafny
Pablo Fernandez
Pablo Fernandez

Reputation: 105220

Dafny simple proof about giving change not working

I want to prove that the following code returns a given amount (money) in 5 and 3 bills/coins:

function sum(ns: seq<nat>): nat
{
  if |ns| == 0 then
    0
  else
    ns[0] + sum(ns[1..])
}

method Change(amount: nat)
  returns (result: seq<nat>)
  requires amount >= 8
  ensures forall i :: 0 <= i <= |result| - 1 ==> result[i] == 3 || result[i] == 5
  ensures sum(result) == amount
{
  if amount == 8 {
    result := [3, 5];
    assert sum(result) == amount;
  } else if amount == 9 {
    result := [3, 3, 3 ];
    assert sum(result) == amount;
  } else if amount == 10 {
    result := [5, 5];
    assert sum(result) == amount;
  } else {
    var tmp := Change(amount - 3);
    assert sum(tmp) == amount - 3; # this works
    var x := [3];
    assert sum(x) == 3; # this works
    result :=  tmp + x;
    assert sum(x) + sum(tmp) == sum(result); # this fails :(
  }
}

The base cases seem to work just fine (Dafny can assert that sum([3, 5]) == amount, for example), but it's struggling with the recursive case.

I've added additional assertions to make the failure clear, in the end what I want to assert is the ensures clause, that assert sum(result) == amount it's true for the recursive case.

Upvotes: 0

Views: 81

Answers (1)

Hath995
Hath995

Reputation: 1300

You need a lemma to explain to Dafny mathematical facts about functions which seem obvious to us but are not obvious to Dafny.

lemma sumConcat(xs: seq<nat>, ys: seq<nat>) 
    ensures sum(xs) + sum(ys) == sum(xs + ys)
{
    if xs == [] {
        assert xs + ys == ys;
        assert sum(xs) == 0;
        assert sum(xs) + sum(ys) == sum(xs + ys);
    }else {
        assert xs == [xs[0]] + xs[1..];
        assert xs + ys == [xs[0]] + xs[1..]+ys;
        sumConcat(xs[1..] , ys);
        assert sum([xs[0]]) == xs[0];
        assert (xs+ys)[1..] == xs[1..]+ys;
        assert sum(xs) + sum(ys) == sum(xs + ys);
    }
}
method Change(amount: nat)
  returns (result: seq<nat>)
  requires amount >= 8
  ensures forall i :: 0 <= i <= |result| - 1 ==> result[i] == 3 || result[i] == 5
  ensures sum(result) == amount
{
  if amount == 8 {
    result := [3, 5];
    assert sum(result) == amount;
  } else if amount == 9 {
    result := [3, 3, 3 ];
    assert sum(result) == amount;
  } else if amount == 10 {
    result := [5, 5];
    assert sum(result) == amount;
  } else {
    var tmp := Change(amount - 3);
    assert sum(tmp) == amount - 3;
    var x := [3];
    assert sum(x) == 3;
    result :=  tmp + x;
    sumConcat(tmp, x);
    assert sum(x) + sum(tmp) == sum(result);
  }
}

Upvotes: 1

Related Questions