Verified Ordered Set in Dafny

Building a Provably Correct Dynamic Ordered Set in Dafny: A Step-by-Step Guide

In the world of software development, we spend countless hours writing tests to prevent bugs. But what if we could prove, with mathematical certainty, that our code is free of entire classes of errors? This is the promise of formal verification, and tools like Dafny are making it more accessible than ever.

In this post, we'll take a deep dive into a Dafny program that implements a GrowableSortedSet—essentially a dynamically-sized, sorted set of unique integers. We won't just look at the code; we'll dissect the specifications and assertions to understand why they are there and how they help Dafny prove our code is correct. Working with classes and mutable data structures in Dafny requires a few different techniques to verify.

If we look at this chart of types in Dafny. We can see there is a missing type in the language. This module will fill it in.

Here is the full module we will be analyzing, which is based on the thesis "Specifica di ADT e verifica dell' implementazione con Dafny" of Stefano Oppedisano at the University of Turin:

You can also download the following code here. SortedSet.dfy

module SortedSet {
    //Based on the work of Stefano Oppesisano
    class GrowableSortedSet {

        ghost var Repr: set<object>
        ghost var elems: seq<int>

        // Fields
        var arr: array<int> 
        var nElems: int // Number of elements in array

        // Implementations
        constructor (size: int)
            requires size > 0
            ensures Valid() && fresh(Repr - {this})
            ensures nElems == |elems| == 0
            ensures arr.Length == size
        {
            arr := new int[size](i => -1);
            nElems := 0;
            elems := [];
            Repr := {this, arr};
        }

        ghost predicate Valid()
            reads this, Repr
        {
            this in Repr 
            && arr in Repr
            && 0 <= nElems <= arr.Length // The number of elements is always in a valid range
            && 0 < arr.Length // The array has a valid length
            && nElems == |elems| // The array and its ghost counterpart are aligned in number of elements...
            && (forall i :: 0 <= i < nElems ==> arr[i] == elems[i]) // ... and value of elements
            && (forall i :: 0 < i < nElems ==> arr[i] > arr[i-1]) // The array is ordered
        }

        predicate IsFull()
            requires Valid()
            reads this, Repr, arr
            ensures IsFull() ==> nElems == arr.Length // If the predicate body is true then it means that nElems is equal to the array length
        {
            nElems == arr.Length
        }

        method GetValue(index: int) returns (value: int)
            requires Valid()
            requires 0 <= index < nElems
            ensures Valid()
        {
            value := arr[index];
        }

        method HasValue(value: int) returns (result: bool)
            requires Valid()
            ensures result ==> exists i :: 0 <= i < nElems && arr[i] == value
            ensures !result ==> forall i :: 0 <= i < nElems ==> arr[i] != value
        {
            OrderedImpliesSorted(arr, nElems);
            var low, high := 0, nElems;
            while low < high
                invariant 0 <= low <= high <= nElems 
                invariant forall i :: 0 <= i < nElems && !(low <= i < high) ==> arr[i] != value 
            {
                var mid := (low + high) / 2; 
                if arr[mid] < value { 
                    low := mid + 1; 
                } else if value < arr[mid] { 
                    high := mid; 
                } else { 
                    return true; 
                } 
            }
            return false; 
        }

        method IncreaseSize() returns ()
            requires Valid()
            modifies this, arr
            ensures Valid() && fresh(Repr - old(Repr))
            ensures !IsFull()
            ensures arr.Length > old(arr.Length)
            ensures arr[..nElems] == old(arr[..nElems])
        {   
            var newArr := new int[arr.Length*2];
            forall i | 0 <= i < arr.Length { newArr[i] := arr[i]; }
            forall i | arr.Length <= i < newArr.Length {newArr[i] := -1; }
            arr := newArr;
            this.Repr := this.Repr + {newArr};
            assert forall i :: 0 <= i < nElems ==> arr[i] == elems[i] by {
                forall i | 0 <= i < nElems
                    ensures arr[i] == elems[i]
                {
                    assert i < nElems;
                }
            }
        }

        method AddValue(value: int) returns (ghost index: int)
            requires Valid()
            requires value !in elems
            modifies Repr, this, arr
            ensures Valid() && fresh(Repr - old(Repr))
            ensures value in elems
            ensures 0 <= index <= old(nElems)
            ensures nElems == old(nElems) + 1
            ensures arr[index] == value
            ensures elems == old(elems[..index]) + [value] + old(elems[index..])
        {
            if IsFull() {
                IncreaseSize();
            }

            assert !IsFull();

            // Find insertion point
            var indexInsert := 0;
            while indexInsert < nElems && arr[indexInsert] < value
                invariant 0 <= indexInsert <= nElems
                invariant forall i :: 0 <= i < indexInsert ==> arr[i] < value
            {
                indexInsert := indexInsert + 1;
            }

            assert arr[..nElems] == elems by {
                forall i | 0 <= i < |elems| 
                    ensures arr[i] == elems[i]
                {
                    assert elems[i] == arr[i];
                }
            }
            elems := elems[..indexInsert] + [value] + elems[indexInsert..];
            label LoopStart: 
            // Shift elements to the right
            var j := nElems;
            while j > indexInsert
                invariant indexInsert <= j <= nElems
                invariant 0 <= j < arr.Length
                invariant arr[..j] == old(arr[..j]) // Array won't change up to indexInsert
                invariant arr[j+1..nElems+1] == old(arr[j..nElems]) // The element at j is the one at j-1
                modifies arr
                decreases j
            {
                arr[j] := arr[j-1];
                assert arr[j] == old(arr[j-1]);
                ArrayShift@LoopStart(arr, j, nElems);
                j := j - 1;
            }
            assert j == indexInsert;
            assert arr[indexInsert+1..nElems+1] == old(arr[indexInsert..nElems]);
            assert old(arr[indexInsert..nElems]) == elems[indexInsert+1..];


            // Increase the nElems as the elements are shifted to the right
            nElems := nElems + 1;

            // Insert the new value
            arr[indexInsert] := value;
            assert forall i :: 0 <= i < |elems| ==> arr[i] == elems[i] by {
                forall i | 0 <= i < |elems| 
                    ensures arr[i] == elems[i]
                {
                    assert i < nElems;
                    if i < indexInsert {
                        assert arr[i] == old(arr[i]);
                        assert elems[i] == arr[i];
                    } else if i == indexInsert {
                        assert elems[i] == arr[i];
                    } else {
                        assert i >= indexInsert+1;
                        assert elems[i] == arr[i];
                    }
                }
            }
            return indexInsert;
        }

        method AppendValue(value: int)
            requires Valid()
            requires value !in elems
            requires forall x :: x in elems ==> x < value
            modifies Repr, this, arr
            ensures Valid() && fresh(Repr - old(Repr))
            ensures value in elems
            ensures nElems == old(nElems) + 1
            ensures arr[nElems - 1] == value
            ensures elems == old(elems[..nElems]) + [value]
        {
            if IsFull() {
                IncreaseSize();
            }

            assert !IsFull();

            elems := elems + [value];
            // Increase the nElems as a new element was added
            nElems := nElems + 1;

            // Insert the new value
            arr[nElems-1] := value;
            if nElems == 1 {

            }else {
                assert elems[nElems-2] in old(elems);
                assert elems[nElems-2] < value;
            }
        }


        method UnionSlow(ss: GrowableSortedSet) returns (result: GrowableSortedSet)
            requires Valid()
            requires ss.Valid()
            // ensures forall x :: x in this.elems[..nElems] ==> x in result.elems
            // ensures forall x :: x in ss.elems[..ss.nElems] ==> x in result.elems
            ensures ToSet(result.elems) == ToSet(this.elems[..nElems])+ToSet(ss.elems[..ss.nElems])
            ensures result.Valid()
        {
            OrderedImpliesSorted(this.arr, nElems);
            OrderedImpliesSorted(ss.arr, ss.nElems);
            result := new GrowableSortedSet(ss.arr.Length + this.arr.Length);
            assert ss.nElems + this.nElems <= ss.arr.Length + this.arr.Length;
            ghost var sumSet: set<int>  := {};
            for i := 0 to this.nElems
                invariant result.Valid()
                invariant fresh(result.Repr)
                invariant ToSet(this.elems[..i]) !! ToSet(this.elems[i..nElems])
                invariant forall x :: x in this.elems[i..nElems] ==> x !in result.elems
                invariant sumSet == ToSet(this.elems[..i])
                invariant ToSet(result.elems) == sumSet
            {
                result.AppendValue(this.arr[i]);
                assert this.elems[i] == this.arr[i];
                assert this.elems[..i+1] == this.elems[..i]+[this.arr[i]];
                ToSetConcat(this.elems[..i], [this.arr[i]]);
                sumSet := sumSet + {this.arr[i]};
            }

            for i := 0 to ss.nElems
                invariant result.Valid()
                invariant fresh(result.Repr)
                invariant ToSet(ss.elems[..i]) !! ToSet(ss.elems[i..ss.nElems])
                invariant ToSet(result.elems) == sumSet
                invariant sumSet == ToSet(this.elems[..this.nElems]) + ToSet(ss.elems[..i])
            {
                ghost var oldElems := result.elems;
                var has_value := result.HasValue(ss.arr[i]);
                if !has_value {
                    var index := result.AddValue(ss.arr[i]);
                    ElementInserted(oldElems, sumSet, this.elems, this.nElems, ss.elems, ss.nElems, i, index);
                    assert 0 <= i < ss.nElems;
                    assert ss.arr[i] == ss.elems[i];
                    ToSetConcat(ss.elems[..i], [ss.arr[i]]);
                    ToSetConcat(this.elems[..this.nElems], ss.elems[..i+1]);
                    SetsCombined(sumSet, this.elems, this.nElems, ss.elems, ss.nElems, i);
                    sumSet := sumSet + {ss.arr[i]};
                }else{
                    assert 0 <= i < ss.nElems;
                    assert ss.arr[i] == ss.elems[i];
                    assert ss.arr[i] in sumSet;
                    assert ss.elems[i] in sumSet;
                    SetsCombined2(sumSet, this.elems, this.nElems, ss.elems, ss.nElems, i);
                }
                SortedArrayIsDisjoint(ss.arr, ss.nElems, ss.elems, i+1);
            }
            assert sumSet == ToSet(this.elems[..this.nElems]) + ToSet(ss.elems[..ss.nElems]);
            // SetsCombinedImplies(result.elems, this.elems, nElems, ss.elems, ss.nElems);
            // assert ToSet(result.elems) == sumSet;


        }

        method {:isolate_assertions} Union(ss: GrowableSortedSet) returns (result: GrowableSortedSet)
            requires Valid()
            requires ss.Valid()
            // ensures forall x :: x in this.elems[..nElems] ==> x in result.elems
            // ensures forall x :: x in ss.elems[..ss.nElems] ==> x in result.elems
            ensures ToSet(result.elems) == ToSet(this.elems[..nElems])+ToSet(ss.elems[..ss.nElems])
            ensures result.Valid()
        {
            OrderedImpliesSorted(this.arr, nElems);
            OrderedImpliesSorted(ss.arr, ss.nElems);
            result := new GrowableSortedSet(ss.arr.Length + this.arr.Length);
            assert ss.nElems + this.nElems <= ss.arr.Length + this.arr.Length;
            ghost var sumSet: set<int>  := {};
            var i := 0;
            var j := 0;
            while i + j < ss.nElems + this.nElems
                invariant 0 <= i <= this.nElems
                invariant 0 <= j <= ss.nElems
                invariant fresh(result.Repr)
                invariant ToSet(result.elems) == sumSet
                invariant i < this.nElems ==> forall x :: x in result.elems ==> x < this.elems[i]
                invariant j < ss.nElems ==> forall x :: x in result.elems ==> x < ss.elems[j]
                invariant sumSet == ToSet(this.elems[..i] + ss.elems[..j])
                invariant result.Valid()
            {
                OrderedImpliesSorted(result.arr, result.nElems);
                if i < this.nElems && j < ss.nElems {
                    if this.arr[i] == ss.arr[j] {
                        assert this.elems[..i+1] == this.elems[..i]+[this.arr[i]];
                        assert ss.elems[..j+1] == ss.elems[..j]+[ss.arr[j]];
                        ToSetConcat(this.elems[..i], [this.arr[i]]);
                        ToSetConcat(ss.elems[..j], [ss.arr[j]]);
                        ToSetConcat(this.elems[..i+1], ss.elems[..j]);
                        ToSetConcat(this.elems[..i+1], ss.elems[..j+1]);
                        result.AppendValue(this.arr[i]);
                        sumSet := sumSet + {this.arr[i]};
                        i := i + 1;
                        j := j + 1;
                    }else if this.arr[i] < ss.arr[j] {
                        assert this.elems[..i+1] == this.elems[..i]+[this.arr[i]];
                        ToSetConcat(this.elems[..i], [this.arr[i]]);
                        ToSetConcat(this.elems[..i+1], ss.elems[..j]);
                        result.AppendValue(this.arr[i]);
                        sumSet := sumSet + {this.arr[i]};
                        i := i + 1;
                    }else{
                        assert j < ss.nElems;
                        var has_value := result.HasValue(ss.arr[j]);
                        assert ss.elems[..j+1] == ss.elems[..j]+[ss.arr[j]];
                        ToSetConcat(ss.elems[..j], [ss.arr[j]]);
                        ToSetConcat(this.elems[..i], ss.elems[..j+1]);
                        result.AppendValue(ss.arr[j]);
                        sumSet := sumSet + {ss.arr[j]};
                        j := j + 1;
                    }
                }else if i < this.nElems {
                    assert this.elems[..i+1] == this.elems[..i]+[this.arr[i]];
                    ToSetConcat(this.elems[..i], [this.arr[i]]);
                    ToSetConcat(this.elems[..i+1], ss.elems[..j]);
                    result.AppendValue(this.arr[i]);
                    sumSet := sumSet + {this.arr[i]};
                    i := i + 1;
                }else {
                    assert j < ss.nElems;
                    assert ss.elems[..j+1] == ss.elems[..j]+[ss.arr[j]];
                    ToSetConcat(ss.elems[..j], [ss.arr[j]]);
                    ToSetConcat(this.elems[..i], ss.elems[..j+1]);
                    result.AppendValue(ss.arr[j]);
                    sumSet := sumSet + {ss.arr[j]};
                    j := j + 1;
                }
            }
            assert i == this.nElems;
            assert j == ss.nElems;
            ToSetConcat(this.elems[..this.nElems], ss.elems[..ss.nElems]);
        }

        method UnionMut(ss: GrowableSortedSet)
            requires Valid()
            requires ss.Valid()
            requires this.Repr !! ss.Repr
            modifies Repr, this, arr
            ensures ToSet(this.elems) == ToSet(old(this.elems))+ToSet(ss.elems[..ss.nElems])
            ensures Valid() && fresh(Repr - old(Repr))
        {
            OrderedImpliesSorted(ss.arr, ss.nElems);
            ghost var sumSet: set<int>  := ToSet(this.elems);
            for i := 0 to ss.nElems
                invariant this.Valid()
                invariant fresh(this.Repr-old(this.Repr))
                invariant ToSet(ss.elems[..i]) !! ToSet(ss.elems[i..ss.nElems])
                invariant sumSet == ToSet(old(this.elems)) + ToSet(ss.elems[..i])
                invariant ToSet(this.elems) == sumSet
            {
                var has_value := this.HasValue(ss.arr[i]);
                assert ss.elems[..i+1] == ss.elems[..i]+[ss.arr[i]];
                ToSetConcat(ss.elems[..i], [ss.arr[i]]);
                if !has_value {
                    var index := this.AddValue(ss.arr[i]);
                    sumSet := sumSet + {ss.arr[i]};
                    assert sumSet == ToSet(old(this.elems)) + ToSet(ss.elems[..i+1]);
                }
            }
        }


    }

    method Main()
    {
        var gs := new GrowableSortedSet(5);
        assert gs.nElems == 0;
        var foo := gs.AddValue(5);
        assert 5 in gs.elems;
        foo := gs.AddValue(10);
        assert 10 in gs.elems;
        assert |gs.elems| == 2;
        foo := gs.AddValue(3);
    }

    function ToSet<A>(xs: seq<A>): set<A>
        ensures forall x :: x in ToSet(xs) ==> x in xs
        ensures forall x :: x !in ToSet(xs) ==> x !in xs
    {
        if xs == [] then {} else {xs[0]}+ToSet(xs[1..])
    }

    lemma ToSetConcat<T>(xs: seq<T>, ys: seq<T>)
        ensures ToSet(xs+ys) == ToSet(xs) + ToSet(ys)
    {

    }

    twostate lemma ArrayShift(arr: array<int>, index: nat, nElems: nat)
        requires 0 < index <= nElems < arr.Length
        requires arr[index+1..nElems+1] == old(arr[index..nElems])
        requires arr[index] == old(arr[index-1])
        ensures arr[index..nElems+1] == old(arr[index-1..nElems])
    {
    }

    lemma GrowableSetSize(gs: GrowableSortedSet)
        requires gs.Valid()
        ensures |ToSet(gs.elems)| == gs.nElems
    {
        if gs.nElems == 0 {
            assert gs.elems == [];
        }else{
            OrderedImpliesDistinct(gs.arr, gs.elems, gs.nElems);
            DistinctToSetSize(gs.elems, gs.nElems);
        }
    }

    predicate OrderedArray(arr: array<int>, nElems: nat) 
        requires nElems <= arr.Length
        reads arr
    {
        forall i :: 0 < i < nElems ==> arr[i-1] < arr[i]
    }

    predicate SortedArray(arr: array<int>, nElems: nat) 
        requires nElems <= arr.Length
        reads arr
    {
        forall j,k :: 0 <= j < k  < nElems ==> arr[j] < arr[k]
    }

    lemma SortedArrayIsDisjoint(arr: array<int>, nElems: nat, elems: seq<int>, i: nat)
        requires nElems <= arr.Length
        requires SortedArray(arr, nElems)
        requires nElems == |elems|
        requires forall i: nat :: i < nElems ==> arr[i] == elems[i]
        requires i <= nElems
        ensures ToSet(elems[..i]) !! ToSet(elems[i..nElems])
    {

    }

    lemma SetsCombined(ss: set<int>, thisElems: seq<int>, nElems: nat, ssElems: seq<int>, ssNelems: nat, i: nat)
        requires |thisElems| == nElems
        requires i < ssNelems
        requires |ssElems| == ssNelems
        requires ssElems[i] !in ss
        requires ss == ToSet(thisElems[..nElems]) + ToSet(ssElems[..i])
        requires ss+{ssElems[i]} == ToSet(thisElems[..nElems]) + ToSet(ssElems[..i+1])
    {

    }

    lemma SetsCombined2(ss: set<int>, thisElems: seq<int>, nElems: nat, ssElems: seq<int>, ssNelems: nat, i: nat)
        requires |thisElems| == nElems
        requires i < ssNelems
        requires |ssElems| == ssNelems
        requires ssElems[i] in ss
        requires ss == ToSet(thisElems[..nElems]) + ToSet(ssElems[..i])
        requires ss == ToSet(thisElems[..nElems]) + ToSet(ssElems[..i+1])
    {

    }

    lemma SetsCombinedImplies(res: seq<int>, thisElems: seq<int>, nElems: nat, ssElems: seq<int>, ssNelems: nat)
        requires |thisElems| == nElems
        requires |ssElems| == ssNelems
        requires ToSet(res) == ToSet(thisElems[..nElems]) + ToSet(ssElems[..ssNelems])
        ensures forall x :: x in thisElems[..nElems] ==> x in res
        ensures forall x :: x in ssElems[..ssNelems] ==> x in res
    {

    }

    lemma ElementInserted(resultElems: seq<int>, ss: set<int>,  thisElems: seq<int>, nElems: nat, ssElems: seq<int>, ssNelems: nat, i: nat, index: nat)
        requires |thisElems| == nElems
        requires i < ssNelems
        requires |ssElems| == ssNelems
        requires ssElems[i] !in ss
        requires ss == ToSet(thisElems[..nElems]) + ToSet(ssElems[..i])
        requires index <= |resultElems|
        requires ToSet(resultElems) == ToSet(thisElems[..nElems]) + ToSet(ssElems[..i])
        ensures ToSet(resultElems[..index]+[ssElems[i]]+resultElems[index..]) == ss+{ssElems[i]}
    {

    }


    lemma IncreasingIndexIsGreater(arr: array<int>, nElems: nat, i: nat, j: nat)
        requires nElems <= arr.Length
        requires OrderedArray(arr, nElems)
        requires i < j < nElems
        ensures arr[i] < arr[j]
    {
        if j == i + 1 {
            assert arr[i] < arr[j];
        }else{
            IncreasingIndexIsGreater(arr, nElems, i, j-1);
            assert arr[i] < arr[j-1] < arr[j];
        }
    }


    lemma OrderedImpliesSorted(arr: array<int>, nElems: nat)
        requires nElems <= arr.Length
        requires OrderedArray(arr, nElems)
        ensures SortedArray(arr, nElems)
    {
        forall i, j | 0 <= i < j < nElems
            ensures arr[i] < arr[j]
        {
            IncreasingIndexIsGreater(arr, nElems, i, j);
        }
    }

    predicate Distinct<T(==)>(ss: seq<T>) {
        forall i, j :: 0 <= i < j < |ss| ==> ss[i] != ss[j]
    }

    lemma OrderedImpliesDistinct(arr: array<int>, elems: seq<int>, nElems: nat)
        requires nElems <= arr.Length
        requires nElems == |elems|
        requires OrderedArray(arr, nElems)
        requires forall i :: 0 <= i < nElems ==> arr[i] == elems[i]
        ensures Distinct(elems)
    {
        forall i, j | 0 <= i < j < nElems
            ensures elems[i] != elems[j]
        {
            IncreasingIndexIsGreater(arr, nElems, i, j);
        }
    }

    lemma DistinctToSetSize(elems: seq<int>, nElems: nat)
        requires nElems == |elems|
        requires Distinct(elems)
        ensures |ToSet(elems)| == nElems
    {
        if nElems == 0 {

        }else{
            DistinctToSetSize(elems[1..], nElems-1);
        }
    }
}

The Big Picture: What Are We Building?

First, let's clarify what our GrowableSortedSet class does. It's a more specialized data structure that maintains a sorted array of unique integers. It can grow in size automatically when it becomes full.

The class has two main concrete fields:

• arr: array<int>: The underlying array that stores our integers.
• nElems: int: The current number of elements stored in the array.

And two ghost fields:

• ghost var Repr: set<object>: A "representation set" that tracks all memory locations (the class object itself and its array) that are part of this component's state. This is crucial for proving that methods only modify the memory they are supposed to.
• ghost var elems: seq<int>: A ghost sequence that represents the "true" contents of our sorted set.

Why use a ghost sequence (elems)?
Reasoning about mutable arrays is hard. When you change arr[i], the verifier has to track a complex change. Immutable sequences, on the other hand, are a verifier's best friend. They are much easier to reason about (e.g., slicing and concatenation like s[..i] + [x] + s[i..]). The ghost elems acts as a simplified, mathematical model of our data structure, and a core part of our proof is ensuring the concrete arr always matches this model.

The Foundation of Correctness: The Valid() Predicate

The heart of any verified class in Dafny is its invariant—a condition that must always be true for any instance of the class (except during a method's execution). In our code, this is the Valid() predicate. Every method that modifies the sorted set must start in a Valid state and ensure it ends in a Valid state.

Let's break it down line by line:

ghost predicate Valid()
    reads this, Repr
{
    // The object and its array are part of the Repr set
    this in Repr && arr in Repr

    // The number of elements is within the array's bounds
    && 0 <= nElems <= arr.Length 

    // The ghost sequence and concrete element count are in sync
    && nElems == |elems| 

    // The values of the concrete array and ghost sequence match
    && (forall i :: 0 <= i < nElems ==> arr[i] == elems[i])

    // The array is sorted in ascending order
    && (forall i :: 0 < i < nElems ==> arr[i] > arr[i-1]) 
}

This predicate is our "definition of correct." If Valid() holds, we know our data structure isn't corrupted.

Implementing the Methods: From Specification to Proof

Now, let's see how our methods maintain this Valid state.

IncreaseSize(): Making Room for More

This method is called when our array is full. It creates a new, larger array and copies the old elements over.

method IncreaseSize() returns ()
    requires Valid()
    modifies this, arr
    ensures Valid() && fresh(Repr - old(Repr))
    ensures !IsFull()
    ensures arr.Length > old(arr.Length)
    ensures arr[..nElems] == old(arr[..nElems])
{   
    var newArr := new int[arr.Length*2];
    forall i | 0 <= i < arr.Length { newArr[i] := arr[i]; }
    // ... rest of the method

The postconditions (ensures) promise that after the call:

1. The sorted set is still Valid().
2. New memory has been allocated (fresh(Repr - old(Repr))).
3. The sorted set is no longer full.
4. The underlying array is indeed larger.
5. The actual elements (arr[..nElems]) are preserved.

Why the assertion?

    assert forall i :: 0 <= i < nElems ==> dic[i] == elems[i] by {
        //...
    }
}

After we execute arr := newArr, Dafny knows the arr field has changed. It doesn't automatically assume that the properties of the old arr (like being sorted or matching elems) have transferred to the new arr. This assert statement is our way of guiding the verifier. We are explicitly telling it: "Hey Dafny, I just copied all the elements. Please verify that the properties from the Valid predicate that depend on arr's values still hold for the new arr." Without this, Dafny would complain that it cannot prove ensures Valid().

---

AddValue(): The Main Event

This is the most complex method. It has to find the correct insertion spot, shift elements to the right, and insert the new value, all while keeping the array sorted.

Step 1: Find the Insertion Point

var indexInsert := 0;
while indexInsert < nElems && arr[indexInsert] < value
    invariant 0 <= indexInsert <= nElems
    invariant forall i :: 0 <= i < indexInsert ==> arr[i] < value
{
    indexInsert := indexInsert + 1;
}

This while loop finds the first index where the element is not less than value. The loop invariants are crucial:

• invariant 0 <= indexInsert <= nElems: This proves that indexInsert never goes out of bounds.
• invariant forall i :: ... ==> arr[i] < value: This is the core logic. It tells Dafny that every element we've scanned so far is less than the new value, which is essential for proving the array remains sorted after insertion.

Step 2: The Ghostly Shift
Before we touch the concrete array, we update our "model" state:

// These two asserts are crucial!
assert forall i :: 0 <= i < |elems| ==> elems[i] > -1;
assert arr[..nElems] == elems;

// Now, update the ghost sequence
elems := elems[..indexInsert] + [value] + elems[indexInsert..];

Why these assertions? We are about to modify the ghost variable elems. The assert statements serve as a "lemma" for Dafny. They re-establish facts that are true from the Valid() predicate right at the point where they are needed. By asserting arr[..nElems] == elems, we give Dafny a concrete link between the array and the sequence right before the sequence changes, which helps it reason about the state after the change.

Step 3: The Physical Shift and the ArrayShift Lemma
Now we shift the elements in the real array to make space.

var j := nElems;
while j > indexInsert
    invariant indexInsert <= j <= nElems
    invariant arr[j+1..nElems+1] == old(arr[j..nElems])
    // ...
{
    arr[j] := arr[j-1];
    ArrayShift@LoopStart(arr, j, nElems); // <- The special helper!
    j := j - 1;
}

The key invariant here is arr[j+1..nElems+1] == old(arr[j..nElems]). This captures the essence of the shift: the segment of the array from j+1 onwards now contains the elements that were previously in the segment from j onwards.

What is ArrayShift?

twostate lemma ArrayShift(arr: array<int>, index: int, nElems: int)
    requires arr[index+1..nElems+1] == old(arr[index..nElems])
    requires arr[index] == old(arr[index-1])
    ensures arr[index..nElems+1] == old(arr[index-1..nElems])
{
}

This is a twostate lemma. It's a pure piece of logic that helps Dafny connect two states of an array (old(arr) and arr). It says:

• IF the elements from index+1 to the end are what used to be from index to the end...
• AND the element at index is what used to be at index-1...
• THEN you can conclude that the entire block from index to the end is what used to be the block from index-1 to the end.

This might seem obvious to us, but it's a reasoning step about array indices and slices that the verifier needs help with. Inside the loop, we call ArrayShift to help Dafny maintain the loop invariant and ultimately prove that the entire shift from indexInsert to nElems works as expected.

You might also notice the curious piece of syntax @LoopStart appended to the ArrayShift lemma. The @ symbol combined with a label is how to specify at which point in time to compare mutable values in the past using the old() operator.

Step 4: The Final Assertion
After shifting and inserting the value, we have one final, critical assertion:

arr[indexInsert] := value;
assert forall i :: 0 <= i < |elems| ==> arr[i] == elems[i] by {
    forall i | 0 <= i < |elems| 
        ensures arr[i] == elems[i]
    {
        if i < indexInsert { ... } 
        else if i == indexInsert { ... } 
        else { ... }
    }
}

This is the grand finale of the proof for AddValue. We are forcing Dafny to prove that our modified concrete array arr now matches our modified ghost sequence elems. We do this by considering three cases:

1. i < indexInsert: For elements before the insertion point, they should be unchanged.
2. i == indexInsert: This is where our new value was placed.
3. i > indexInsert: These are the elements that were shifted to the right.

By proving this correspondence for all three cases, we successfully re-establish the most important part of our Valid() invariant, and Dafny can now conclude the entire method is correct.

Of course! This is an excellent set of examples that illustrates some of the most common and powerful patterns in Dafny. Here is a blog post explaining them, written to be accessible to someone new to formal verification.

---

Defining and Proving Properties of Pure Functions

Let's start with something simple: converting a sequence (seq) to a set (set). Sequences have duplicates and order, while sets do not. How can we define a "correct" conversion?

The Function and Its Specification

function ToSet<A>(xs: seq<A>): set<A>
    // The output set contains ONLY elements from the input sequence.
    ensures forall x :: x in ToSet(xs) ==> x in xs
    // The output set contains ALL elements from the input sequence.
    ensures forall x :: x !in ToSet(xs) ==> x !in xs
{
    if xs == [] then {} else {xs[0]} + ToSet(xs[1..])
}

This is a classic recursive function, but the magic is in the ensures clauses. They form the function's contract.

1. ensures forall x :: x in ToSet(xs) ==> x in xs: This says, "For any element x, if it's in the output set, it must have been in the input sequence." This prevents our function from inventing new elements.
2. ensures forall x :: x !in ToSet(xs) ==> x !in xs: This is the other direction. "If an element x is not in the output set, it must not have been in the input sequence."

Together, these two clauses guarantee that ToSet(xs) contains exactly the elements of xs, no more and no less.

Proving a Property: The ToSetConcat Lemma

Once we have a function, we often want to prove properties about how it behaves. For example, we'd expect that converting the concatenation of two sequences to a set is the same as converting each to a set and then taking their union. A lemma is how we state and prove such a property in Dafny.

lemma ToSetConcat<T>(xs: seq<T>, ys: seq<T>)
    ensures ToSet(xs+ys) == ToSet(xs) + ToSet(ys)
{
    // The proof is by induction on the sequence `xs`, written out explicitl
    if xs == [] {
        // Base Case: xs is empty. The property holds trivially.
        // ToSet([] + ys) == ToSet(ys)
        // ToSet([]) + ToSet(ys) == {} + ToSet(ys) == ToSet(ys)
    } else {
        // Inductive Step: Assume the property holds for xs[1..].
        // We need to prove it for xs.
        // Let's expand the left-hand side (LHS) of the ensures clause:
        // ToSet(xs + ys) 
        //   == ToSet([xs[0]] + (xs[1..] + ys))                 (by seq properties)
        //   == {xs[0]} + ToSet(xs[1..] + ys)                   (by ToSet definition)
        //   == {xs[0]} + (ToSet(xs[1..]) + ToSet(ys))           (by the induction hypothesis!)
        //   == ({xs[0]} + ToSet(xs[1..])) + ToSet(ys)           (set union is associative)
        //   == ToSet(xs) + ToSet(ys)                           (by ToSet definition)
        // This matches the RHS. QED.
        ToSetConcat(xs[1..], ys); // This call provides the induction hypothesis to Dafny.
    }
}

Dafny proves this lemma automatically! The recursive call ToSetConcat(xs[1..], ys); triggers the induction, and the verifier handles the rest. This lemma is a reusable building block for more complex proofs.

---

Proving Equivalence: "Local" vs. "Global" Properties

A common task in verification is to prove that a simple, "local" property implies a more powerful, "global" one. Let's look at two different ways to define a sorted array.

Definition 1: The "Local" Property (OrderedArray)
An array is ordered if every element is strictly greater than its immediate predecessor. This is easy to check in a loop.

predicate OrderedArray(arr: array<int>, nElems: nat)
    requires nElems <= arr.Length
    reads arr
{
    forall i :: 0 < i < nElems ==> arr[i-1] < arr[i]
}

Definition 2: The "Global" Property (SortedArray)
An array is sorted if every element is strictly greater than any of its preceding elements. This is what we usually mean by "sorted."

predicate SortedArray(arr: array<int>, nElems: nat)
    requires nElems <= arr.Length
    reads arr
{
    forall j,k :: 0 <= j < k  < nElems ==> arr[j] < arr[k]
}

Clearly, SortedArray is a stronger property. But is OrderedArray enough to guarantee it? Yes! And we can prove it.

The Proof of Equivalence

First, we need a helper lemma that uses induction to bridge the gap from "adjacent" to "any."

// Proves that in an OrderedArray, an element at a higher index is always greater.
lemma IncreasingIndexIsGreater(arr: array<int>, nElems: nat, i: nat, j: nat)
    requires nElems <= arr.Length
    requires OrderedArray(arr, nElems)
    requires i < j < nElems
    ensures arr[i] < arr[j]
    decreases j - i // Dafny needs to know the proof is making progress.
{
    if j == i + 1 {
        // Base Case: j is adjacent to i. This is the definition of OrderedArray.
        assert arr[i] < arr[j];
    } else {
        // Inductive Step: Assume the property holds for (i, j-1).
        IncreasingIndexIsGreater(arr, nElems, i, j-1);
        // We know arr[i] < arr[j-1] (from induction)
        // and arr[j-1] < arr[j] (from OrderedArray).
        // By transitivity, arr[i] < arr[j].
        assert arr[i] < arr[j-1] < arr[j];
    }
}

// Now, the main proof is trivial.
lemma OrderedImpliesSorted(arr: array<int>, nElems: nat)
    requires nElems <= arr.Length
    requires OrderedArray(arr, nElems)
    ensures SortedArray(arr, nElems)
{
    // To prove `ensures SortedArray(...)`, we must prove its body:
    // `forall i, j :: 0 <= i < j < nElems ==> arr[i] < arr[j]`
    // Our helper lemma does exactly that!
    forall i, j | 0 <= i < j < nElems
        ensures arr[i] < arr[j]
    {
        IncreasingIndexIsGreater(arr, nElems, i, j);
    }
}

It proves that if you write a loop that correctly maintains the simple OrderedArray property, you can be certain that the final result satisfies the more powerful SortedArray property.

---

From Specification to Implementation: Writing a Provably Correct Binary Search

We've seen how to define and prove abstract properties about arrays. Now for the ultimate test: can we use these properties to write a real, provably correct algorithm?

Let's implement one of the most fundamental search algorithms: binary search. It's famously easy to get wrong. Off-by-one errors in low, high, or mid can lead to infinite loops or incorrect results. With Dafny, we can eliminate that entire class of bugs.

Step 1: Defining the Contract

First, what does it mean for a search method to be "correct"? We can capture this perfectly in Dafny's ensures clauses. Our method, HasValue, will be part of a class that encapsulates an array and a count of its elements (nElems).

class GrowableSortedSet {
    var arr: array<int>
    var nElems: nat

    // Predicate to check that the array is sorted.
    predicate Valid() 
        reads this, arr 
    {
        nElems <= arr.Length && OrderedArray(arr, nElems)
        ...
    }

    method HasValue(value: int) returns (result: bool)
        // The method can only be called on a valid, sorted collection.
        requires Valid()
        // If it returns true, the value must exist in the array.
        ensures result ==> exists i :: 0 <= i < nElems && arr[i] == value
        // If it returns false, the value must not exist in the array.
        ensures !result ==> forall i :: 0 <= i < nElems ==> arr[i] != value
    {
        // ... implementation coming soon ...
    }
}

This contract is airtight. It specifies exactly what the method guarantees for both true and false return values. There's no ambiguity. Our only job now is to write an implementation that the Dafny verifier can prove satisfies this contract.

Step 2: The Implementation and the Loop Invariant

We will use the standard binary search algorithm. The real challenge in verification is not writing the code, but writing the loop invariant. A loop invariant is a property that is true at the beginning of every single iteration of a loop. It's the key that unlocks the proof.

What do we know during our search? The core idea of binary search is that at every step, we shrink the "window" of indices ([low, high)) where the value could possibly be. This means we can be certain that the value is not in the parts of the array we've already discarded.

This is our main invariant:
forall i :: 0 <= i < nElems && !(low <= i < high) ==> arr[i] != value

Let's put it all together.

method HasValue(value: int) returns (result: bool)
    requires Valid()
    ensures result ==> exists i :: 0 <= i < nElems && arr[i] == value
    ensures !result ==> forall i :: 0 <= i < nElems ==> arr[i] != value
{
    // First, let's bring in our powerful `SortedArray` property.
    // Our helper lemma from before makes this a one-liner!
    OrderedImpliesSorted(arr, nElems);

    var low := 0;
    var high := nElems;

    while low < high
        // This invariant keeps track of our search window's bounds.
        invariant 0 <= low <= high <= nElems
        // This is the key: the value cannot be outside our search window.
        invariant forall i :: 0 <= i < nElems && !(low <= i < high) ==> arr[i] != value
    {
        var mid := (low + high) / 2;

        if arr[mid] < value {
            // If arr[mid] is too small, the value can only be in the upper half.
            // We can now discard the entire lower half, including mid.
            low := mid + 1;
        } else if value < arr[mid] {
            // If arr[mid] is too big, the value can only be in the lower half.
            // We can discard the upper half, but mid itself might still be the smallest
            // value greater than `value`, so we keep it in the window.
            high := mid;
        } else {
            // We found it! The first ensures clause is now satisfied.
            return true;
        }
    }
    // If the loop finishes, low == high, the window is empty.
    // The invariant tells us the value is nowhere to be found.
    // The second ensures clause is now satisfied.
    return false;
}

How Dafny Proves It

The verifier does a remarkable amount of work for us, all guided by our invariant.

1. Before the Loop: It checks that the invariant holds true when low = 0 and high = nElems. In this case, the window [0, nElems) covers the whole array, so the condition !(low <= i < high) is always false, making the forall statement trivially true.

2. During the Loop (Maintenance): For each path inside the loop (if, else if), Dafny assumes the invariant was true at the start of the iteration and proves it's still true after low or high is updated.

   • For example, in the arr[mid] < value branch, Dafny uses the SortedArray property to deduce that for all i <= mid, arr[i] <= arr[mid] < value. Therefore, it's safe to discard the entire range [low, mid] by setting low := mid + 1, and the invariant will be maintained.

3. After the Loop: When the loop terminates, we know two things: the loop condition low < high is false (so low >= high) and the loop invariant is true.

   • Since low <= high (from the first invariant) and low >= high, it must be that low == high.
   • This means our search window [low, high) is empty. The second invariant now simplifies to forall i :: 0 <= i < nElems ==> arr[i] != value.
   • This is exactly the ensures clause for returning false! The proof is complete.

By providing the right contract and the right invariant, we have successfully guided the Dafny verifier to a complete, formal proof of correctness for our binary search. No more off-by-one bugs. No more infinite loops. Just provably correct code.

Conclusion: Code That Proves Itself

As we've seen, writing verifiable code in Dafny is a dialogue with the verifier. The code says what it does, and the specifications (requires, ensures, invariant) state the properties it must uphold. The assertions are our way of providing hints, lemmas, and intermediate steps to guide the verifier through the more complex parts of the proof.

While it may seem like extra work, the payoff is enormous: a guarantee that your GrowableSortedSet will never have an out-of-bounds error, will always remain sorted, and will never fail to insert an element correctly. It's not just tested code; it's provably correct code. And that is a very powerful thing indeed.

We've just scratched the surface, but these patterns are the bread and butter of writing provably correct code in Dafny:

1. Defining behavior with ensures clauses on pure functions.
2. Proving properties about those functions with inductive lemmas.
3. Reasoning about state changes over time with twostate lemmas.
4. Proving that simple, local properties imply powerful, global ones.

By mastering these concepts, you can move from hoping your code is correct to proving it.

What's next?

The methods provided includes a mutable and immutable version of the union operation. This class could be extended to provide the mutable and immutable versions of the standard set operations difference, intersection, and others. Can you leverage the structure of a sorted set to implement these methods in efficent time?