Verified example of code for a newsletter

_README.md

For the newsletter at: FILL IN

Run with Dafny 4.6.0, with the flag --standard-libraries.

v1.dfy

import opened Std.Collections.Seq
import opened Std.Wrappers

method FindPredecessor(s: seq<int>, x: int) returns (r: Option<int>)
ensures if r.None? then x !in s
        else s[IndexOf(s, r.value)+1] == x
{
  var index := IndexOfOption(s, x);
  if index == None {
    return None;
  }
  else
  {
    var v := index.Extract();
    return Some(s[v-1]);
  }

}

v1_errors.txt

(7,18): Error: index out of range
  |
7 |              else s[IndexOf(s, r.value)+1] == x
  |                    ^^^^^^^^^^^^^^^^^^^^^^^
(7,20): Error: function precondition could not be proved
  |
7 |              else s[IndexOf(s, r.value)+1] == x
  |                     ^^^^^^^^^^^^^^^^^^^

DafnyStandardLibraries.dfy(6627,13): Related location
     |
6627 |     requires v in xs
     |              ^^^^^^^

(19,4): Error: a postcondition could not be proved on this return path
   |
19 |     return Some(s[v-1]);
   |     ^^^^^^

(7,18): Related location: this is the postcondition that could not be proved
  |
7 |              else s[IndexOf(s, r.value)+1] == x
  |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

(19,16): Error: index out of range    
   |
19 |     return Some(s[v-1]);

v2.dfy

    
import opened Std.Collections.Seq
import opened Std.Wrappers

method FindPredecessor(s: seq<int>, x: int) returns (r: Option<int>)
ensures if r.None? then x !in s
            else if r.value == |s|-1 then s[0] == x
            else s[IndexOf(s, r.value)+1] == x
{
  var index := IndexOfOption(s, x);
  if index == None {
    return None;
  }
  else if index.Extract() == 0 {
    return Some(s[|s|-1]);
  }
  else
  {
    var v := index.Extract();
    return Some(s[v-1]);
  }

}

v2_errors.txt

(7,42): Error: index out of range
  |
7 |             else if r.value == |s|-1 then s[0] == x
  |                                            ^^^

(8,17): Error: index out of range     
  |
8 |             else s[IndexOf(s, r.value)+1] == x
  |                   ^^^^^^^^^^^^^^^^^^^^^^^

(8,19): Error: function precondition could not be proved
  |
8 |             else s[IndexOf(s, r.value)+1] == x
  |                    ^^^^^^^^^^^^^^^^^^^

DafnyStandardLibraries.dfy(6627,13): Related location
     |
6627 |     requires v in xs
     |              ^^^^^^^

(15,4): Error: a postcondition could not be proved on this return path
   |
15 |     return Some(s[|s|-1]);
   |     ^^^^^^

(8,17): Related location: this is the postcondition that could not be proved
  |
8 |             else s[IndexOf(s, r.value)+1] == x
  |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

(20,4): Error: a postcondition could not be proved on this return path
   |
20 |     return Some(s[v-1]);
   |     ^^^^^^

(7,42): Related location: this is the postcondition that could not be proved
  |
7 |             else if r.value == |s|-1 then s[0] == x
  |                                           ^^^^^^^^^