title: Verifying Account Transfer in Dafny
body: <p>I'm trying to verify a simple account transfer in Dafny, and this is what I came up with:</p>
  <pre><code>function sum(items: seq&lt;int&gt;): int
  decreases |items| {
      if items == []
      then 0
      else items[0] + sum(items[1..])
  }
  
  method transfer(accounts: array&lt;int&gt;, balance: int, from: int, to: int)
  requires from &gt;= 0 &amp;&amp; from &lt; accounts.Length;
  requires to &gt;= 0 &amp;&amp; to &lt; accounts.Length;
  requires accounts.Length &gt; 0;
  requires sum(accounts[..]) == balance;
  ensures sum(accounts[..]) == balance;
  modifies accounts;
  {
      accounts[from] := accounts[from] - 1;
      accounts[to] := accounts[to] + 1;
      return;
  }
  </code></pre>
  <p>I'm just transferring one token at a time here (though actually I want to transfer an arbitrary amount).  Eitherway, it doesn't verify.  I'm wondering what else I need to do?</p>