DEV Community: Aaron Elligsen

Verified Ordered Set in Dafny

Aaron Elligsen — Thu, 14 Aug 2025 18:09:56 +0000

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:

The sorted set is still Valid().
New memory has been allocated (fresh(Repr - old(Repr))).
The sorted set is no longer full.
The underlying array is indeed larger.
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:

i < indexInsert: For elements before the insertion point, they should be unchanged.
i == indexInsert: This is where our new value was placed.
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.

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.
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.

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.
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.
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:

Defining behavior with ensures clauses on pure functions.
Proving properties about those functions with inductive lemmas.
Reasoning about state changes over time with twostate lemmas.
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?

Verifying Count Equal and Divisible Pairs in an Array

Aaron Elligsen — Fri, 15 Dec 2023 14:22:17 +0000

Verifying Leetcode question 2176. Count Equal and Divisible Pairs in an Array

Let's take a look at this leetcode problem.

We are asked to count pairs of indices, i and j where i < j, in the provided array that are equal and when multiplying them together are divisible by some integer k.

It is a fairly straight forward problem to solve but how do we prove that our solution is correct?

function countPairs(nums: number[], k: number): number {
   let count = 0;
   for(let i = 0; i < nums.length-1; i++) {
       for(let j = i+1; j < nums.length; j++) {
           if(nums[i] == nums[j] && (i*j) % k == 0) {
               count++;
           }
       }
   }
   return count;
}

First we define our functions and predicates that we can use to define our intended goal. We encapsulate the condition we are checking for as a predicate function. Predicates in Dafny are just functions which return a boolean and they are ubiquitous which is why they get their own keyword. Quite often when you define the right predicate many things fall into place easily for verifying programs.

Then we define the pairs function which returns a set which is basically as simple of a description of the intended goal as possible.

predicate satPairs(nums: seq<nat>, k: nat, a: nat, b: nat)
    requires k > 0
    requires a < b < |nums| 
{
    nums[a] == nums[b] && (a*b) % k == 0
}

function pairs(nums: seq<nat>, k: nat): set<(int, int)> 
    requires k > 0
{
    set x, y | 0 <= x < y < |nums| && satPairs(nums, k, x, y) :: (x,y)
}

The set notation of Dafny follows the convention of most math texts, where we can read it as saying the set of pairs (x,y) where x is less than y, and both are less than the length of nums and x and y satisfy the conditions for a pair.

Our specification of the problem begins like this.

method countPairs(nums: seq<nat>, k: nat) returns (count: nat) 
    requires k > 0
    requires |nums| >= 2
    ensures count == |pairs(nums,k)|
{
}

One issue with Dafny that beginners will run into is that it will not automatically determine the cardinality (aka the size) of a set. It really only focuses on if an item is or is not in a set. The size of a set must be determined inductively either with a lemma or in a method.

Similarly, when using a for or while loop some incremental progress is being made towards the goal. You need to show that inductively it builds towards your goal. To that end we can define two different helper functions to define what partial progress means in this problem.

PairsI represents all possible pairs that are less than the current i in the loop. In Dafny ghost variables are variables which do not exist at execution time but are there to help verify the intend properties. In this case we define cpairs to represent the set of pairs that we are building up.

function pairsI(nums: seq<nat>, k: nat, i: nat): set<(nat, nat)> 
    requires k > 0
    requires 0 <= i < |nums|
{
    set x: nat, y:nat | 0 <= x < i && x < y < |nums| && satPairs(nums, k, x, y) :: (x,y)
}

method countPairs(nums: seq<nat>, k: nat) returns (count: nat) 
    requires k > 0
    requires |nums| >= 1
    ensures count == |pairs(nums,k)|
{
    count := 0;
    ghost var cpairs: set<(nat, nat)> := {};
    for i : nat := 0 to |nums|-1 
        invariant cpairs == pairsI(nums, k, i)
        invariant count == |pairsI(nums, k, i)|
    {
    }
}

In the original program we had an inner for loop and we need to track the progress of that as well. The function pairsJ builds the set of pairs that match for the current i iteration of the outer loop and the jth iteration of the inner loop.


function pairsJ(nums: seq<nat>, k: nat, i: nat, j: nat): set<(nat, nat)> 
    requires 0 <= i < |nums|
    requires i < j
    requires k > 0
{
    set x: nat | i < x < j <= |nums| && satPairs(nums, k, i, x) :: (i,x)
}


method countPairs(nums: seq<nat>, k: nat) returns (count: nat) 
    requires k > 0
    requires |nums| >= 1
    ensures count == |pairs(nums,k)|
{
    count := 0;
    ghost var cpairs: set<(nat, nat)> := {};
    for i : nat := 0 to |nums|-1 
        invariant cpairs == pairsI(nums, k, i)
        invariant count == |pairsI(nums, k, i)|
    {
        ghost var occount := count;
        ghost var increment := 0;
        ghost var pairset: set<(nat, nat)> := {};
        for j := i+1 to |nums| 
            invariant i+1 <= j <= |nums|
            invariant pairset == pairsJ(nums,k, i,j)
            invariant increment == |pairsJ(nums,k,i,j)|
            invariant count == occount + increment
        {
            if satPairs(nums, k, i, j) {
                increment := increment + 1;
                pairset := pairset+{(i,j)};
                count := count + 1;
            }
        }
        cpairs := cpairs + pairset;
    }
    assert pairsI(nums,k, |nums|-1) == pairs(nums,k);
}

An important consideration in Dafny is that we can show pairsI(nums, k, i) + pairsJ(nums, k, i, |nums|) is equivalent to pairsI(nums, k, i+1).

We can show this with a lemma. Which Dafny immediately verifies.

lemma PairsIMaintenance(nums: seq<nat>, k: nat, i: nat) 
    requires k > 0
    requires 0 <= i <= |nums|-2
    ensures pairsI(nums, k, i+1) == pairsI(nums, k, i)+pairsJ(nums, k, i, |nums|)
{
}

Verifying Invert Binary Tree

Aaron Elligsen — Sat, 20 May 2023 14:46:08 +0000

Verifying LeetCode Problem: 266. Invert Binary Tree

Let's take a look at the problem

Given the root of a binary tree, invert the tree, and return its root.

A binary tree is defined by a root node and then between zero and two child nodes branching from it. These child nodes are themselves binary trees. Traditionally the child nodes are labeled the right and left child. What they mean by invert the binary tree is that the left child is swapped with the right child. However, the complication is that they want this done to every node in the tree.

Here is the definition of the data type provided.

 class TreeNode {
     val: number
     left: TreeNode | null
     right: TreeNode | null
     constructor(val?: number, left?: TreeNode | null, right?: TreeNode | null) {
         this.val = (val===undefined ? 0 : val)
         this.left = (left===undefined ? null : left)
         this.right = (right===undefined ? null : right)
     }
 }

An implementation

Here is how we can solve this in JavaScript/TypeScript.

function invertTree(root: TreeNode | null): TreeNode | null {
    if(root == null) return null;
    let leftChild = invertTree(root.left);
    let rightChild = invertTree(root.right);
    root.right = leftChild;
    root.left = rightChild;
    return root;
};

Recursive data structures like a tree are often solved with recursive functions. We start with the base case, where recursion stops. In this case, our function checks if the tree is null and returns null if so. Every branch of a tree will end with null leaves. It recursively inverts all child elements and then swaps the left and right child. This function modifies the tree in place and then returns the modified root.

There is quite a lot going on but lets see the function specification in Dafny to get an idea of what it is that the function does.

method  invertBinaryTree(root: TreeNode?) returns (newRoot: TreeNode?)
    modifies if root != null then root.repr else {}
    requires root != null ==> root.Valid()
    ensures root == null ==> newRoot == null
    ensures root != null ==> newRoot != null && newRoot.repr == old(root.repr) && newRoot.Valid()
    ensures root != null ==> newRoot == root && newRoot.right == old(root.left) && root.left == old(root.right)
    ensures root != null ==> forall node :: node in newRoot.repr ==> node.right == old(node.left) && node.left == old(node.right)
    decreases if root == null then {} else root.repr
{
    if root != null {
        var leftChild := invertBinaryTree(root.left);
        var rightChild := invertBinaryTree(root.right);
        root.right := leftChild;
        root.left := rightChild;
        return root;
    }else{
        return null;
    }
}

The basic problem definition boils down to this line.

ensures root != null ==> newRoot == root && newRoot.right == old(root.left) && root.left == old(root.right)

Dafny has a mechanism, the old() operator which for heap/mutable objects can refer to the value a variable had before it was changed at a certain point in the method. In this case we say the returned root has a left value which is equal to the old right value and likewise the right value is equal to the old left value.

Since this the goal of this method is to invert the entire binary tree we also must make sure that all nodes in the tree are inverted.

ensures root != null ==> forall node :: node in newRoot.repr ==> node.right == old(node.left) && node.left == old(node.right)

Classes in Dafny

To represent mutable data structures in Dafny classes are the preferred method and they have a couple of conventions that are intended to help specifications.

The first is the repr ghost property of a class instance, it represents the set of all objects held by the instance and the instance itself. It is a ghost variable which is not actually part of the compiled code but it is very convenient to use for verification.

ensures root != null ==> newRoot != null && newRoot.repr == old(root.repr) && newRoot.Valid()

If we look at this line of specification it tells us that after the method runs that the tree is still valid and all of the existing nodes are still in the tree and no new nodes were added.

The second is the Valid() method which is a predicate that ensures that each instance is well formed in some way.

class TreeNode {
    var val: int;
    var left: TreeNode?;
    var right: TreeNode?;
    ghost var repr: set<TreeNode>;

    constructor(val: int, left: TreeNode?, right: TreeNode?)
        requires left != null ==> left.Valid()
        requires right != null ==> right.Valid()
        requires left != null && right != null ==> left.repr !! right.repr
        ensures this.val == val
        ensures this.left == left
        ensures this.right == right
        ensures left != null ==> this !in left.repr
        ensures right != null ==> this !in right.repr
        ensures Valid()
    {
        this.val := val;
        this.left := left;
        this.right := right;
        var leftRepr := if left != null then {left}+left.repr else {};
        var rightRepr := if right != null then {right}+right.repr else {};
        this.repr := {this} + leftRepr + rightRepr;
    }

    ghost predicate Valid()
        reads this, repr
        decreases repr
    {
        this in repr &&
        (this.left != null ==>
            (this.left in repr
            && this !in this.left.repr
            && this.left.repr < repr
            && this.left.Valid())
        )
        && (this.right != null ==>
            (this.right in repr
            && this !in this.right.repr
            && this.right.repr < repr
            && this.right.Valid())
        ) && (this.left != null && this.right != null ==> this.left.repr !! this.right.repr && this.repr == {this} + this.left.repr + this.right.repr)
            && (this.left != null && this.right == null ==> this.repr == {this} + this.left.repr)
            && (this.right != null && this.left == null ==> this.repr == {this} + this.right.repr)
            && (this.right == null && this.left == null ==> this.repr == {this})
    }
}

The Valid method is a bit verbose but it is quite powerful and ensures that every tree instance in a valid tree is a contained only within one branch, and it's own subset of nodes, or repr is contained within the parent repr, and all of it's child instances are Valid themselves. It also ensures that no parent node is within the subset of it's child nodes.

This method is important for verification because it ensures that we cover all the relevant cases in our methods. Meaning either a node has no child elements, it has one child either on the left or right, or both children. Then it ensures that our method is not duplicating or reverting work it did earlier because it ensures that every node is only visited once.

Class Method

Although this method was described as a stand alone method, it could also have been implemented as a method of the class.

method  invertBinaryTree() returns (newRoot: TreeNode?)
    modifies this.repr
    requires this.Valid()
    ensures newRoot == this && newRoot.right == old(this.left) && newRoot.left == old(this.right)
    ensures newRoot.repr == old(this.repr) && newRoot.Valid()
    ensures forall node :: node in this.repr ==> node.right == old(node.left) && node.left == old(node.right)
    ensures newRoot.Valid()
    decreases repr
{
    var leftChild: TreeNode? := null;
    if left != null {
        leftChild := left.invertBinaryTree();
    }
    var rightChild: TreeNode? := null;
    if right != null {
        rightChild := right.invertBinaryTree();
    }
    right := leftChild;
    left := rightChild;
    return this;
}

Verify Climbing Stairs

Aaron Elligsen — Mon, 03 Apr 2023 06:48:40 +0000

Verify LeetCode Question: 70. Climbing Stairs

The question is a counting problem. It asks in how many ways can a person reach the top of n steps when they can either take 1 or 2 steps at a time.

Implementation

Here is how we could solve this in TypeScript.

function climbStairs(n: number): number {
    let steps = new Array(n+1);
    steps[0] = 0;
    steps[1] = 1;
    steps[2] = 2;
    for(let i = 3; i <= n; i++) {
        steps[i] = steps[i-1] + steps[i-2];
    }
    return steps[n];
};

We setup a steps array to contain the count of ways to reach a step x. We begin by filling the known values for the beginning steps. After that for every given step we add at the number of ways we could have reached the previous step and the step two below our current step.

Specifying the implementation

We begin translating the problem definition to a method, and predicates (functions that return true and false for some value).

datatype Steps = One | Two

function stepSum(xs: seq<Steps>): nat {
    if xs == [] then 0 else (match xs[0] {
        case One => 1
        case Two => 2
    } + stepSum(xs[1..]))
}

ghost predicate stepEndsAt(xs: seq<Steps>, n: nat) {
    stepSum(xs) == n
}

ghost predicate allEndAtN(ss: set<seq<Steps> >, n: nat) {
    forall xs :: xs in ss ==> stepEndsAt(xs, n)
}

method climbStairs(n: nat) returns (count: nat) 
    ensures exists ss: set< seq<Steps> > :: count == |ss| && allEndAtN(ss, n)
{
}

We define the action of taking steps with a datatype Steps. Given a sequence of steps we can sum them using the stepSum function. You could just as well imagine an array of number with just 1 or 2 but using a datatype eliminates the possibility of numbers other 1 or 1 being present.

We define the stepEndsAt predicate to ask "given a sequence of steps does it end at step n?"

Then if we are given a set of different sequences of steps allEndAtN asks "do all of these sequences of steps end at step n?"

Finally, with those definitions we can return to the problem. The method climbStairs is the program we are trying to verify. The method says that given a step n then it will return a count which is equal to the size of the set of sequences of steps which all end at n. n is a natural number meaning 0 or above in Dafny.

Verifying the implementation

There are some differences between the Dafny and TypeScript solution because JavaScript, which underlies TypeScript, is very lenient with array sizes because it has dynamically sized arrays. Dafny does not so there are some additional checks to satisfy the the compiler but the behavior is the same.

method climbStairs(n: nat) returns (count: nat) 
    ensures exists ss: set< seq<Steps> > :: count == |ss| && allEndAtN(ss, n)
{
    var steps := new nat[n+1];
    steps[0] := 0;
    if n > 0 {
        steps[1] := 1;
    }
    if n > 1 {
        steps[2] := 2;
    }
    stepBaseZero();
    stepBaseOne();
    stepBaseTwo();
    if n < 3 {
        return steps[n];
    }
    // assert steps[0] == 0;
    // assert steps[1] == 1;
    // assert steps[2] == 2;
    // assert forall k: nat :: k < 3 ==> exists ss: set< seq<Steps> > :: steps[k] == |ss| && allEndAtN(ss, k);
    var i := 3;
    while i <= n 
        invariant 3 <= i <= n+1
        invariant forall k: nat :: k < i ==> exists ss: set< seq<Steps> > :: steps[k] == |ss| && allEndAtN(ss, k)
    {   
        steps[i] := steps[i-1] + steps[i-2];
        stepSetsAdd(i, steps);
        i := i + 1;
    }
    return steps[n];
}

Proving the base cases

To show the bases cases of 0, 1, and 2 satisfy our specification for the count we can define lemmas in dafny to show that steps sets exists and exactly what they are.

lemma stepBaseZero() 
    ensures exists ss: set< seq<Steps> > :: allEndAtN(ss, 0) && |ss| == 0
{
    assert allEndAtN({[]}, 0);
}

lemma stepBaseOne() 
    ensures exists ss: set< seq<Steps> > :: allEndAtN(ss, 1) && |ss| == 1
{
    assert allEndAtN({[One]}, 1);
}

lemma stepBaseTwo() 
    ensures exists ss: set< seq<Steps> > :: allEndAtN(ss, 2) && |ss| == 2
{
    assert allEndAtN({[One,One], [Two]}, 2);
}

Proving the induction

We have to show that with in the loop we maintain the count for the given step. Dafny cannot prove this automatically, so we write some lemma's to show that it is true.

As induction traditionally goes, we assume that for all steps less than i, our property was true, which is the requirements specified in the lemma. Then we show that adding those values maintains the property.

lemma stepSetsAdd(i: nat, steps: array<nat>) 
    requires i >= 2
    requires steps.Length >= i+1
    requires forall k: nat :: k < i ==> exists ss: set< seq<Steps> > :: steps[k] == |ss| && allEndAtN(ss, k)
    ensures exists sp : set< seq<Steps> > :: |sp| == steps[i-1] + steps[i-2] && allEndAtN(sp, i)
{
    var oneStepBack :| steps[i-1] == |oneStepBack| && allEndAtN(oneStepBack, i-1);
    var twoStepBack :| steps[i-2] == |twoStepBack| && allEndAtN(twoStepBack, i-2);
    var stepForward := addOne(oneStepBack);
    var stepTwoForward := addTwo(twoStepBack);
    assert forall x :: x in stepForward ==> x[0] == One;
    // assert stepForward !! stepTwoForward;
    addOneSize(oneStepBack);
    addTwoSize(twoStepBack);
    var sumSet := stepForward + stepTwoForward;
    assert |sumSet| == steps[i-1]+steps[i-2];
}

We define two helper functions plusOne, and plusTwo. In Dafny version 4 ghost functions are functions which are only used in the verification context and are not compiled to executable code. These functions add either one or two steps to a sequence and return a longer sequence. We can then define addOne and addTwo to do this for our sets of sequences.

ghost function plusOne(x: seq<Steps>): seq<Steps> {
    [One]+x
}

ghost function plusTwo(x: seq<Steps>): seq<Steps> {
    [Two]+x
}

ghost function addOne(ss: set<seq<Steps>>): set<seq<Steps>> 
    ensures forall x :: x in ss ==> plusOne(x) in addOne(ss)
    ensures addOne(ss) == set x | x in ss :: plusOne(x)
{
    set x | x in ss :: plusOne(x)
}

ghost function addTwo(ss: set<seq<Steps>>): set<seq<Steps>> 
    ensures forall x :: x in ss ==> plusTwo(x) in addTwo(ss)
    ensures addTwo(ss) == set x | x in ss :: plusTwo(x)
{
    set x | x in ss :: plusTwo(x)
}

Lastly a key insight to help Dafny verify is the the set of sequences of steps incremented by either one or two steps is the same size as the original set.

lemma UnequalSeqs<T>(xs: seq<T>, ys: seq<T>, someT: T)
    requires xs != ys
    ensures [someT]+xs != [someT]+ys
{
    if |xs| < |ys| {} else if |ys| > |xs| {}
    else if i: nat :| i < |xs| && i <|ys| && xs[i] != ys[i] {
        assert ([someT]+xs)[i+1] != ([someT]+ys)[i+1];
    }
}

lemma plusOneNotIn(ss: set<seq<Steps>>, x: seq<Steps>)
    requires x !in ss
    ensures plusOne(x) !in addOne(ss)
{
    if x == [] {
        assert [] !in ss;
        assert [One]+[] !in addOne(ss);
    }
    if plusOne(x) in addOne(ss) {
        forall y | y in ss 
            ensures y != x
            ensures plusOne(y) in addOne(ss)
            ensures plusOne(y) != plusOne(x)
        {
            UnequalSeqs(x, y, One);
            assert plusOne(y) != [One]+x;
        }
        assert false;
    }
}

lemma addOneSize(ss: set<seq<Steps>>)
    ensures |addOne(ss)| == |ss|
{
    var size := |ss|;
    if x :| x in ss {
        assert |ss - {x}| == size - 1;
        addOneSize(ss - {x});
        assert |addOne(ss-{x})| == size - 1;
        assert addOne(ss) == addOne(ss-{x}) + {[One]+x};
        assert x !in ss-{x};
        plusOneNotIn(ss-{x}, x);
        assert plusOne(x) !in addOne(ss-{x});
        assert |addOne(ss)| == |addOne(ss-{x})| + |{[One]+x}|;
    }else{

    }
}

lemma plusTwoNotIn(ss: set<seq<Steps>>, x: seq<Steps>)
    requires x !in ss
    ensures plusTwo(x) !in addTwo(ss)
{
    if x == [] {
        assert [] !in ss;
        assert [Two]+[] !in addTwo(ss);
    }
    if plusTwo(x) in addTwo(ss) {
        forall y | y in ss 
            ensures y != x
            ensures plusTwo(y) in addTwo(ss)
            ensures plusTwo(y) != plusTwo(x)
        {
            UnequalSeqs(x, y, Two);
            assert plusTwo(y) != [Two]+x;
        }
    }
}

lemma addTwoSize(ss: set<seq<Steps>>)
    ensures |addTwo(ss)| == |ss|
{
    var size := |ss|;
    if x :| x in ss {
        // assert |ss - {x}| == size - 1;
        addTwoSize(ss - {x});
        // assert |addTwo(ss-{x})| == size - 1;
        assert addTwo(ss) == addTwo(ss-{x}) + {[Two]+x};
        // assert x !in ss-{x};
        plusTwoNotIn(ss-{x}, x);
        // assert plusTwo(x) !in addTwo(ss-{x});
        assert |addTwo(ss)| == |addTwo(ss-{x})| + |{[Two]+x}|;
    }
}

Sets and their usefulness

Aaron Elligsen — Sat, 10 Sep 2022 13:44:56 +0000

Sets

The most basic data structure, the beginning of them all, is the Set. It is one of the bases of Mathematics. A set is a simple collection of unique items. It has no other constraints.

A set can tell you one thing, whether an element is inside of it or not. There are a great many situations in software which come down to this question. However, the key property of a Set is uniqueness! If it contains an element it only contains one of those elements.

Looking at Sets in JavaScript will help us move from Sets as a mathematical concept to practical implementation. Any real world implementation of a theoretical concept will come with some limitations which we will discuss throughout. Before running the code blocks below I encourage you to guess what the output will be

A Container and its methods

In JavaScript Sets are a collection object. They contain values of other data. Sets were added to the language in JavaScript 2015. Sets make it easier and more efficient to test element membership.

Constructor

The JavaScript set constructor take an optional parameter of an iterable. Elements are added to this container object and the data structure steps through them. Frequently, arrays are used for Set construction but other sets are valid inputs as well, or any other custom data structure which implements the JavaScript iterable protocol. In any case, what you get at the end is a collection of unique elements.

let emptySet = new Set();
//create a new set containing 1, 2, and 3
let smallNumbers = new Set([1, 2, 3])
let copyNumbers = new Set(smallNumbers);
let someOtherSet = new Set(iterableCollection)

Add

JavaScript sets are mutable, or changeable, meaning we can add new unique elements to a set.

let smallNumbers = new Set([1, 2, 3])
smallNumbers.add(4) //set now contains [1,2,3,4]

Delete

The complement of add removes an element from a set.

let smallNumbers2 = new Set([1, 2, 3])
smallNumbers2.delete(3) //set now contains [1,2]

Has - the membership test

The most important method of a set, it will let you ask if a given element is in a particular set, returning either true or false. In most mathematical writing this method is called "in" and is written using the symbol ∈ and can be read as either "in" or "belongs to". In the case that it does not belong in the set, it can be written as "not in" or ∉. The behavior and sensitivity of has() is what sets it apart and is an improvement over JavaScript's standard objects.

let responseSet = new Set(["yes", "no"]);
responseSet.has("yes") // true 
responseSet.has("no") // true 
responseSet.has("maybe") //false

JavaScript Aside: the keyword `in`

in serves to test membership of string keys in a standard JavaScript object. However, it does not work with sets.

JavaScript objects consist of zero or more key value pairs. {key: value1, key2: value2, ...}. All keys are converted to strings upon object creation, unless they are a symbol. One important feature of Sets in JavaScript is that they can test membership of objects correctly, which is not the case for standard JavaScript objects.

const mySymbol = Symbol("bet you haven't seen these");
const yourSymbol = Symbol("Virgo?");

let node = {value: 10, next: null};
let otherNode = {value: 100, next: {value: 90, next: null}};

let exampleObj = {
  one: 1,
  two: 2,
  1: 0,
  true: "example",
  "undefined": "sort of undefined",
  "null": "not so null",
  [mySymbol]: "Symbols are a newish primitive type"
}
exampleObj[node] = "misleadingAssignment";
exampleObj[undefined] = "defined";
exampleObj[null] = "definitely null";
//After these last lines
//what do you expect the values of 
//exampleObj["undefined"] 
//exampleObj["null"] to equal?

"one" in exampleObj // true
"two" in exampleObj // true
"1" in exampleObj //true
1 in exampleObj //true - 1 is cast to a string
true in exampleObj //true - true is cast to a string
"true" in exampleObj //true
2 in exampleObj //false
undefined in exampleObj //true - undefined is cast to a string
"undefined" in exampleObj //true 
null in exampleObj // true - null is cast to a string
"null" in exampleObj //true
mySymbol in exampleObj // true
yourSymbol in exampleObj //false

node in exampleObj //returns true, but it is a lie
otherNode in exampleObj //returns true but it shouldn't.
"[object Object]" in exampleObj //returns true, but why?

We never added otherNode to the exampleObj. Unhelpfully, JavaScript converts node to the string '[object Object]'. This default behavior is provided by the .toString method inherited by all objects. You can override this behavior to try to return unique strings for an object but this can be incorrect as well.

As we can see JavaScript's old syntax for testing membership has several gotcha's and limitations. The Set has method improves the situation by no longer implicitly converting the element we want to test into a string. The has method does value comparison for primitive elements and reference comparison for objects (asking is it the same object in memory?). It does not do any casts or conversions. In the following code block, we can see how the set is not confused between primitive values and the string versions of those values. Importantly how it correctly answers the question of membership of objects like node and otherNode from the example above.

let betterSet = new Set([
  "one", 
  1, 
  true, 
  undefined, 
  null, 
  node, 
  mySymbol
])
betterSet.has("one") // true

betterSet.has("1") //false
betterSet.has(1) //true

betterSet.has(true) //true
betterSet.has("true") //false

betterSet.has(undefined) //true
betterSet.has("undefined") //false

betterSet.has(null) //true
betterSet.has("null") //false
betterSet.has(mySymbol) // true

betterSet.has(node) //true - correct
betterSet.has(otherNode) //false - correct

Mathematical Operations

Unfortunately, when JavaScript added sets to the language they did not provide the standard mathematical operators for sets as methods. MDN provides the following implementations of these operations.

Subset/Superset

A set can test if every element in that set is contained in another typically larger set. The former is called a subset and the latter is called the super set. In mathematics they use a sideways u symbol to indicate a set is a subset of another set, subset ⊆ set.

function isSuperset(set, subset) {
    for (let elem of subset) {
        if (!set.has(elem)) {
            return false
        }
    }
    return true
}

Equality

The superset operations provides a natural definition of set equality, that is if two sets are both supersets and subsets of each other then they are considered equal.

function setEqual(setA, setB) {
    return isSuperset(setA, setB) && isSuperset(setB, setA);
}

Union

This is the notion of combining two different sets.
Formally, this operation takes two sets to creates a new set which contains all elements that are contained in setA and setB. Mathematically, this operation is represented with a '∪'. It is easier to remember the symbol as part of the name 'U'nion.

function union(setA, setB) {
    let _union = new Set(setA)
    for (let elem of setB) {
        _union.add(elem)
    }
    return _union
}
union(new Set([1,2]), new Set([2,3,4])) //returns Set {1,2,3,4}

Intersection

The intersection of two sets is the set of all elements which the sets share in common. Formally, the intersection operation takes two sets and creates a new set which contains only elements that are both contained in setA and contained in setB. Mathematically, this operation is represented with '∩', like a large upside down U. I like to remember the symbol as i'n'tersection.

function intersection(setA, setB) {
    let _intersection = new Set()
    for (let elem of setB) {
        if (setA.has(elem)) {
            _intersection.add(elem)
        }
    }
    return _intersection
}
intersection(new Set([1,2]), new Set([2,3,4])) //returns Set {2}

Symmetric Difference

This operation takes two sets and create a new set which contains only elements which are only contained in setA and only contained in setB, but not both.

function symmetricDifference(setA, setB) {
    let _difference = new Set(setA)
    for (let elem of setB) {
        if (_difference.has(elem)) {
            _difference.delete(elem)
        } else {
            _difference.add(elem)
        }
    }
    return _difference
}
symmetricDifference(new Set([1,2]), new Set([2,3,4])) //returns Set {1,3,4}

Difference

This operation takes two sets to create a new set which contains only elements from the first set, excluding any elements from the second set. It is also sometimes called the relative complement.

function difference(setA, setB) {
    let _difference = new Set(setA)
    for (let elem of setB) {
        _difference.delete(elem)
    }
    return _difference
}

Complement

This operation returns everything that is not in the current set. In the traditional mathematical set logic this operation is usually represented with a bar over the set. Another piece of convention is that U is used to represent the Universe, meaning the maximal set, as in everything possible for that set.

We can consider it visually like this.

function complement(setA, universe) {
  return difference(universe, setA);
}

Mathematical Laws

Sets and their operation have a number of important laws governing their behavior. These are pieces of information that you know will be true that you can use to build programs.

Subset laws

∅ ⊆ A
A ⊆ A

Subsets have two follow two important laws. The empty subset is a subset of every set and every set is a subset of itself.

Identity Laws

Union and intersection both have special sets which act as an identity element for these operations, meaning you end up with what you started with.

Domination Laws

The domination laws say that if you union a set with everything you get everything and if you intersect a set with nothing you get nothing.

Idempotent Laws

Similar to the identity laws, in these situations you end up with what you started with.

Complementation Law

This is the formal notion that a double complement of a set is the set itself.

Commutative Laws

The Commutative laws is one of the most powerful laws of sets. It tells you that regardless of the order of the operations for two sets you end up with the same value. It is powerful because if you have a large number of sets that you need to union or intersect together then you do not need to be worried about the specific order in which you do operations.

Associative Laws

The Associative law is similarly powerful and can be used with the commutative law to process groups of sets in either multiple steps, multiple locations (as in distributed computing), or in different processing orders. It gives you tremendous flexibility in how you can process data.

Formally, it says that we can either take the union of three sets in either order A union (B union C first) or (A union B first) union C.

Distributive Laws

This law tells us how union and intersect interact together and what result to expect from the different combinations. They also provide alternative ways to calculate the answer we might be after.

De Morgan's Laws

De Morgan's laws, named for a famous mathematician, tell use how complement interacts with union and intersection.

Absorption Laws

The absorption laws are somewhat a retelling of the idempotent law. The tell yet another situation where we consistently end up where we started. These situations are helpful in software because they let us skips steps and go straight to the end without having to recalculate answer we already have.

Complement Laws

To finally round out our picture, we can say that if we union A with everything not in A, we get everything. Similarly, if we take A intersect with everything that is not in A, there is nothing in common, so we get the empty set.

Patterns

Commonly, you have multiple sets that you either need to union or intersect to get some result.

let mathClass = new Set(["Alice","Bob","Carl","Eve"]);
let litClass = new Set(["Jane","John","Bob","Eve"]);
let historyClass = new Set(["Jim","Bob","Leslye","Eve"]);

let allClasses = [mathClass, litClass, historyClass];

let allClassMates = allClasses.reduce(
(members, classSet) => union(members, classSet), new Set())

let commonStudents = allClasses.reduce(
(members, classSet) => intersection(members, classSet));

JavaScript Caveats

The biggest caveat in JavaScript is around object equality. Set of objects in JavaScript compare the objects by reference, meaning it checks if they are the same object in memory not if they are the same value. It should be obvious that the same object in memory is equivalent to itself, but if we expect {one: true, two: false} to be equivalent to another object with the same values the default behavior of javascript is unexpected. This is a weakness of the equality operators in JavaScript that is inherited by the Set implementation.

let example1 = {one: true, two: false}
let example2 = {one: true, two: false};

console.log(example1 == example1) //true
console.log(example1 == example2) //false - by reference

let sampleSet = new Set([example1]);
sampleSet.has(example1) // true as expected
sampleSet.has(example2) // false perhaps unexpected

JavaScript Alternatives

Writing lemmas in Dafny

Aaron Elligsen — Fri, 09 Sep 2022 05:19:04 +0000

Lemmas

Quite often you need to explain various mathematical facts to Dafny. The way you do this is by writing lemmas, which are basically ghost methods. Like any other function or method they can have input parameters, return values, preconditions, and postconditions. However, lemmas only exist in the specification context and do not compile to executable code.

There is a guide to writing lemmas here.

Direct Proof: An example on Relations

A Relation is a set of order pairs of objects of some other set. The most common example is the integer ordering relation, like less than or equal to. If we limit ourselves to just the integers 1-3 we can encode the it like so.

var lessThanEqual := {
(1,1),
(1,2),
(1,3),
(2,2),
(2,3),
(3,3)
};

We can say that 1 is less than or equal to 3 if the pair (1,3) is in the lessThanEqual set.

There are many types of relations. We can define these types in Dafny using predicate functions. We can create generic functions by parameterizing the input type as a type variable T.

predicate relationOnASet<T>(R: set<(T,T)>, S: set<T>) {
    forall ts :: ts in R ==> ts.0 in S && ts.1 in S
}

predicate reflexive<T>(R: set<(T,T)>, S: set<T>) 
    requires relationOnASet(R, S)
{
    forall s :: s in S ==> (s,s) in R
}

predicate symmetric<T>(R: set<(T,T)>, S: set<T>)
    requires relationOnASet(R, S)
{
    forall x: T, y:T :: x in S && y in S && (x,y) in R ==> (y, x) in R
}

predicate transitive<T>(R: set<(T,T)>, S: set<T>) 
    requires relationOnASet(R, S)
{
    forall a,b,c :: a in S && b in S && c in S && (a,b) in R && (b,c) in R ==> (a,c) in R
}

predicate equivalenceRelation<T>(R: set<(T,T)>, S: set<T>) 
    requires relationOnASet(R, S)
{
    reflexive(R, S) && symmetric(R, S) && transitive(R, S)
}

Union of relations?

Since a relation is just a set and we can combine sets using set union, what can we say about the union of certain kinds of relations? Dafny overloads + to mean set union when working with sets.

If we union two symmetric relations is the result still symmetric?We can prove it in Dafny like so.

lemma symmetricUnion<T>(R_1: set<(T,T)>, S_1: set<T>, R_2: set<(T,T)>, S_2: set<T>)
    requires |R_1| > 0
    requires |R_2| > 0
    requires |S_1| > 0
    requires |S_2| > 0
    requires relationOnASet(R_1, S_1)
    requires relationOnASet(R_2, S_2)
    requires symmetric(R_1, S_1)
    requires symmetric(R_2, S_2)
    ensures symmetric(R_1+R_2, S_1+S_2)
{
    forall x,y | x in S_1+S_2 && y in S_1+S_2 && (x,y) in R_1+R_2
        ensures (y,x) in R_1+R_2
    {
        if  x in S_1 && y in S_1 && (x,y) in R_1 {
            assert (y,x) in R_1+R_2;
        }else if  x in S_2 && y in S_2 && (x,y) in R_2 {
            assert (y,x) in R_1+R_2;
        }
    }
}

However, if we ask the same question about transitive relations we run into trouble. We can create a counter example.

lemma transitiveUnionCounterExample<T>()
  returns (
  R1: set<(T, T)>, S1: set<T>,
  R2: set<(T, T)>, S2: set<T>)
  ensures relationOnASet(R1, S1)
  ensures relationOnASet(R2, S2)
  ensures transitive(R1, S1)
  ensures transitive(R2, S2)
  ensures ! transitive(R1 + R2, S1 + S2)
{
  var a : T :| assume true;
  var b : T :| assume a != b;
  var c : T :| assume a != c && b != c;
  S1 := {a, b};
  S2 := {b, c};
  R1 := {(a, b)};
  R2 := {(b, c)};
}

lemma transitiveUnionNotAlwaysTransitive<T>()
  ensures !
  (forall S1 : set<T>, S2 : set<T>, R1 : set<(T,T)>, R2 : set<(T, T)> ::
  relationOnASet(R1, S1) &&
  relationOnASet(R2, S2) &&
  transitive(R1, S1) &&
  transitive(R2, S2)  ==> transitive(R1 + R2, S1 + S2)
  )
{
  var a, b, c, d := transitiveUnionCounterExample<T>();
}

Proofs by contradiction in Dafny

The creator of Dafny recommends the following template for a proof by contradiction.

lemma L(...)
  requires P
  ensures Q
{
  if !Q {
    ...
    assert !P;
    assert false;
  }
}

The goal here is that if we assume !Q for some proposition, then through some calculations or assertions we can show that implies !P, which is assumed to be true by the require precondition, then we have reached a contradiction.

Asserting false is an additional step which makes it clear we expect this branch to end in contradiction.

Verifying Valid Anagram

Aaron Elligsen — Tue, 06 Sep 2022 22:07:02 +0000

Verifying LeetCode Problem: 242. Valid Anagram

Let's look at the problem definition.

Given two strings s and t, return true if t is an anagram of s, and false otherwise.

An Anagram is a word or phrase formed by rearranging the letters of a different word or phrase, typically using all the original letters exactly once.

Theory

In mathematics, there is an object called a multiset. It is like a set in that it contains elements, but unlike a set not every element in a multiset is distinct. In other words, repeats are allowed in a multiset. We can ask the multiset how many copies of some element it contains, also called the multiplicity of the element.

{1,2,3} == {1,2,3,3} //sets discard duplicates

 //the numbers of 3 elements don't match so the multisets are not the same
multiset{1,2,3} != multiset{1,2,3,3}

A string is an anagram of another string if the multiset of the strings are equivalent.

Therefore, the problem is basically an equivalent of asking if the multiset of two strings are equal.

An implementation

Most languages don't natively support or provide a multiset object, but you can construct one with any sort of Map object. Basically, the element is the key, and the val is the count of the element in the multiset.

function toMultiset(s: string): Map<string, number> {
    const s_mset: Map<string, number> = new Map();
    for(let char of s) {
        if(s_mset.has(char)) {
            s_mset.set(char, s_mset.get(char)+1);
        }else{
            s_mset.set(char, 1);
        }
    }
    return s_mset;
}

function msetEqual(s: Map<string, number>, t: Map<string, number>): boolean {

    for(let [lchar,] of s) {
        if(!(s.get(lchar) === t.get(lchar))) {
            return false;
        }
    }

    for(let [rchar,] of t) {
        if(!(s.get(rchar) === t.get(rchar))) {
            return false;
        }
    }

    return true;
}

function isAnagram(s: string, t: string): boolean {
    return msetEqual(toMultiset(s), toMultiset(t));
};

Specifying the problem

It is a very quick method to specify, so we will work top to bottom. In Dafny the string type is defined as the type seq.

isAnagram

method isAnagram(s: string, t: string) returns (equal: bool)
    ensures (multiset(s) == multiset(t)) == equal
{
    var smset := toMultiset(s);
    var tmset := toMultiset(t);
    equal := msetEqual(smset, tmset);
}

toMultiset

Dafny does provide a native multiset object and methods. We will use these to verify our Typescript method is equivalent.

method toMultiset(s: string) returns (mset: multiset<char>)
    ensures multiset(s) == mset
{
    mset := multiset{};
    for i := 0 to |s| 
        invariant mset == multiset(s[0..i])
    {
        assert s == s[0..i] + [s[i]] + s[(i+1)..];
        mset := mset + multiset{s[i]};
    }
    assert s == s[0..|s|];
    return mset;
}

As we iterate through the loop the invariant is that the mset result is equal to the multiset of the slice of the string which we have visited so far. Verifying this method requires two assertions.

Dafny forgets what lists are equal to unless you can remind it with an assert (and again strings are lists in Dafny). Supposedly, this is done for performance reasons, but it is an absurdly frequent reason for problems verifying. Here we show Dafny that our string is the concatenation of the visited substring plus the current element plus the rest of the list.

Secondly, Dafny needs reminded that the slice from the 0th index up to but not including the length of the string is equal to the original string.

And to assert that our typescript implementation is equivalent to this I should say that:

mset := mset + multiset{s[i]};

is equivalent to adding and element to map and setting the multiplicity to 1 or adding 1 to the multiplicity of an element already in the multiset.

With that toMultiset verifies it is equal to the native method which takes a sequence of elements and returns a multiset.

msetEqual

Making a method in Dafny to assert two multiset are equal is a bit tricky. It's typically unnecessary since Dafny can do it directly but to verify our TypeScript implementation we must.

In TypeScript we cannot assert two maps are equal directly because JavaScript compares objects by reference rather than by value. This is why we created the msetEqual function in TypeScript.

To show the two maps are equals we iterate through all the elements/keys in the first map and then check if those keys are in the second map and the multiplicities/counts match.

Then we do the same for the second map to the first. This ensures that the sets are the same and one is not just a superset of the other containing exactly the firsts elements plus some others.

TypeScript/JavaScript provide a nice for-of syntax to iterate through all elements in a map.

Dafny provides no exact analogue but we can build it.

method msetEqual(s: multiset<char>, t: multiset<char>) returns (equal: bool)
    ensures s == t <==> equal
{
    ghost var sremoved: multiset<char> := multiset{};
    var scopy := s;
    while scopy != multiset{} 
        invariant s - sremoved == scopy
        invariant sremoved !! scopy
        invariant sremoved <= s
        invariant forall x :: x in sremoved ==> x in s && x in t && t[x] == s[x]
    {
        var x :| x in scopy;
        if !(x in t && s[x] == t[x]) {
           return false; 
        }
        var removed := multiset{};
        sremoved := sremoved + removed[x := s[x]];
        scopy := scopy - removed[x := s[x]];
    }

We create a copy of a given multiset s and a ghost var sremoved equal to an empty multiset.

In side the loop, we pick some x such that x is an char in scopy.

if x is not in t or the multiplicity of x in s is not equal to the multiplicity of x in t then we return false. The multisets are not equal.

Otherwise, we create a new multiset named removed to fill with x to the multiplicity of x in s. removed[x := s[x]]. We add this to the ghost var and remove it from scopy. Importantly, this is equivalent to fully removing x from scopy.

All four loop invariants are required to show that forall x :: x in s ==> x in t && s[x] == t[x] which is our real goal.

The first invariant invariant s - sremoved == scopy established a relationship between s, sremoved, and scopy. As scopy iterates towards the empty multiset, sremoved grows towards s.

invariant sremoved !! scopy is definitely the least understandable at a glance, but for multisets !! is the disjoint operator. As in, sremoved !! scopy is true if they have no elements in common. We need this to show the following.

invariant sremoved <= s starts out true since the empty multiset is a subset of any other multiset. Inductively, the only things Dafny knows about sremoved is that s - sremoved == scopy, if not for invariant 2. It could be that smremoved is some larger set that has some intersecting elements with S. As scopy goes to the empty set, it could be said that s is a subset of sremoved. However, the fact that sremoved and scopy are always disjoint means that eventually s == scopy + sremoved == multiset{} + sremoved.

Finally, the most important invariant, invariant forall x :: x in sremoved ==> x in s && x in t && t[x] == s[x], which actually asserts that some subset of t is equal to s.

We proceed with the other direction using the same logic and we show that the the opposite is true, which implies t == s.

Full definition

method msetEqual(s: multiset<char>, t: multiset<char>) returns (equal: bool)
    ensures s == t <==> equal
{
    ghost var sremoved: multiset<char> := multiset{};
    var scopy := s;
    while scopy != multiset{} 
        invariant s - sremoved == scopy
        invariant sremoved !! scopy
        invariant sremoved <= s
        invariant forall x :: x in sremoved ==> x in s && x in t && t[x] == s[x]
    {
        var x :| x in scopy;
        if !(x in t && s[x] == t[x]) {
           return false; 
        }
        var removed := multiset{};
        sremoved := sremoved + removed[x := s[x]];
        scopy := scopy - removed[x := s[x]];
    }
    //assert s <= sremoved
    assert s == sremoved;

    ghost var tremoved: multiset<char> := multiset{};
    var tcopy := t;
    while tcopy != multiset{} 
        invariant t - tremoved == tcopy
        invariant tremoved !! tcopy
        invariant tremoved <= t
        invariant forall x :: x in tremoved ==> x in s && x in t && t[x] == s[x]
    {
        var x :| x in tcopy;
        if !(x in t && s[x] == t[x]) {
           return false; 
        }
        var removed := multiset{};
        tremoved := tremoved + removed[x := s[x]];
        tcopy := tcopy - removed[x := s[x]];
    }
    //assert s <= sremoved
    assert t == tremoved;
    return true;
}

Final thoughts

When I said all four invariants are required, it turns out that is false. It is required to show that sremoved and tremoved are equal to s and t respectively, which is what you would intuitively expect from how we define the body of the loop.

However, you can still verify with just invariants 1 and 4 and removing the equality assertion after the loop. In this situation, the for loops really imply that forall x :: x in s ==> x in sremoved ==> x in s && s in t && t[x] == s[x] and for t respectively.

Best practices

Quite often Dafny is able to verify using fewer statements and constraints than I expect and so I usually go back through and comment out all invariants and assertions to see exactly which ones are really necessary.
There are many true statements about the state of variables during an algorithm. However, quite often they are unnecessary to prove that the algorithm does what you want it to.

One of the trickier aspects of Dafny is that there are multiple ways to write the same logical expression, and simultaneously Dafny has differing ability to handle automatically applying induction to different formulations, which means that is easier for it to verify some expressions than others. Part of the difficulty of verification is finding a valid logical/mathematical expression for your invariants, and then secondly writing it in such a way that Dafny is able to verify it easily.

Verify Path Sum

Aaron Elligsen — Tue, 06 Sep 2022 19:37:56 +0000

Verifying LeetCode Question: 112. Path Sum

Let's look at the problem definition.

Given the root of a binary tree and an integer targetSum, return true if the tree has a root-to-leaf path such that adding up all the values along the path equals targetSum.

A leaf is a node with no children.

An implementation

Here is how we can solve this in JavaScript/TypeScript.

function hasPathSum(root: TreeNode | null, targetSum: number): boolean {
    if(root == null) {
        return false;
    }
    if(root.val-targetSum == 0 && root.left == null && root.right == null) {
        return true;
    }
    return hasPathSum(root.left, targetSum-root.val) || hasPathSum(root.right, targetSum-root.val);
};

Tree problems are often easily solved with a recursive algorithm.

Breaking this down by cases:
if the current root is null then there is no path which matches the targetSum.

if the current node value matches the targetSum and the current node is a leaf node then we are done, a path exists.

If there is a path in the current nodes left child or if there is a path in the current node right child, minus the current value of this node, then the path exists.

Specifying the implementation

First we define a tree datatype.

datatype TreeNode = Nil | Tree(val: nat, left: TreeNode, right: TreeNode)

We translate the problem definition into two helper functions/predicates. In Dafny, the sequence type, seq is the type of an array like object (i.e it can be indexed into) and it is also like a linked list. assert path == [path[0]+path[1..];

predicate isPath(paths: seq<TreeNode>, root: TreeNode) {
    if |paths| == 0 then false else match paths[0] {
        case Nil => false
        case Tree(val, left, right) => if |paths| == 1 then root == paths[0] else root == paths[0] && (isPath(paths[1..], left) || isPath(paths[1..], right))
    }
}

We say that a path is a sequence of TreeNodes starting from the root. Then if the sequence is not empty and the first node is not Nil and the root is equal to the first node in the list, then if the rest of the list (removing the first element/root) is either a path starting with the roots left child or right child. It will return true or false if is a valid path in the tree.

function pathSum(paths: seq<TreeNode>): nat {
    if |paths| == 0 then 0 else match paths[0] {
        case Nil => 0
        case Tree(val, left, right) => val + pathSum(paths[1..])
    }
}

Given a path, we recursively break the list apart to the first element and the rest of the list, and then add the node value to the pathSum of the rest of the list.

Given these definitions we can translate the problem definition like so:

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) 
    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum
{
}

Again, we are able to verify the existence of some path p, that sums to the targetSum is the method returns true.

Verifying the implementation

This should be a simple conversion of the TypeScript code to Dafny.

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) 
    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum
{
    if root == Nil {
        return false;
    }

    if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {
        return true;
    }
    var leftPath := hasPathSum(root.left, targetSum-root.val);
    var rightPath := hasPathSum(root.right, targetSum-root.val);

    return leftPath || rightPath;
}

proving the induction to Dafny

Dafny is not immediately convinced of our ensures clause when we write this method. Convincing it is not too difficult but we have to use another Dafny feature.

first resolving the ending case.

if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {
  assert isPath([root], root) && pathSum([root]) == targetSum;
  return true;
}

We add an assertion showing that [root] is a valid path and it exists. Secondly if the root value == targetSum then the pathSum([root]) is equal to the targetSum too.

After doing this Dafny will approve of the return condition, but then it will complain about the recursive case.

We call the recursive calls and save the result into a variable, then we break it down into cases.

var leftPath := hasPathSum(root.left, targetSum-root.val);
var rightPath := hasPathSum(root.right, targetSum-root.val);

if leftPath {
  ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;
  assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
}
if rightPath {
  ghost var p: seq<TreeNode> :| isPath(p, root.right) && pathSum(p) == targetSum-root.val;
  assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
}

The new syntax here is a ghost var. A ghost var is a variable that Dafny can use to keep track of data useful to assertions, but it is not actually part of the code that actually runs when a method is run.

It is a variable that only exists in the specification context and not in the execution context of a program.

Secondly, we use the :| operator meaning such that, so basically we can read the following statement like so.

if leftPath {
  ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;
  assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
}

If the leftPath variable is true then inductively hasPathSum says there existed a path p starting at the roots left node and its path sum equals the targetSum-root.val. We assign that path to p. Then we show that if we add the root to that path then that is still a valid path and the pathSum is root.val+(targetSum-root.val) == targetSum. Following the same argument on the right the method verifies.

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) 
    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum
{
    if root == Nil {
        return false;
    }

    if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {
        assert isPath([root], root) && pathSum([root]) == targetSum;
        return true;
    }
    var leftPath := hasPathSum(root.left, targetSum-root.val);
    var rightPath := hasPathSum(root.right, targetSum-root.val);

    if leftPath {
        ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;
        assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
    }
    if rightPath {
        ghost var p: seq<TreeNode> :| isPath(p, root.right) && pathSum(p) == targetSum-root.val;
        assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
    }
    return leftPath || rightPath;
}

Verify Contains Duplicate II

Aaron Elligsen — Tue, 06 Sep 2022 18:27:08 +0000

Verify LeetCode Question: 219. Contains Duplicate II

Following from our last post, we look at slightly more complicated version of the problem.

Given an integer array nums and an integer k, return true if there are two distinct indices i and j in the array such that nums[i] == nums[j] and abs(i - j) <= k.

An implementation

Here is how we might solve this in JavaScript/TypeScript.

function containsNearbyDuplicate(nums: number[], k: number): boolean {
    let windowSet: Set<number> = new Set();
    const n = nums.length;
    if(k == 0) return false;
    for(let i = 0; i < n; i++) {
        if(windowSet.has(nums[i])) {
            return true;
        }
        if(i >= k) {
            windowSet.delete(nums[i-k]);
        }
        windowSet.add(nums[i]);
    }
    return false;
};

In short, we create a set of numbers again and add elements of the array to it as we iterate. However, once we have moved past the k-th index then we start removing the (i-k)-th elements from the list. If we do this every subsequent step it ensures that only the last k array elements are in the set and then if we encounter an element already in that set we know that it is a duplicate which is in an index position x such that x-i <= k.

Specifying the implementation

Again we convert the problem definition into the specification clause into specification clauses on our Dafny method.

Given an integer array nums and an integer k, return true if there are two distinct indices i and j in the array such that nums[i] == nums[j] and abs(i - j) <= k.

requires k <= |nums|
ensures containsDuplicate ==> exists i,j :: 0 <= i < j < |nums| && j-i <= k && nums[i] == nums[j]

The difference here from the definition is that we assume one index i will be less than the than the other matching index. Thus the difference j-i will always be positive, so we can skip using the absolute difference.

Requires

requires is another specification clause used by Dafny to impose limits on the inputs allowed for a given method/function. In this case we can read the LeetCode problem constraints and see that the value k provided never exceeds the maximum length of the array. Thus we encode it as a constraint in our method. It makes some logical sense as well in this problem.

Verifying the implementation

Here is a verifying implementation which is a straight forward conversion of the TypeScript code.

// {:verify true} is an attribute that lets us toggle 
//verifying the method until we are ready
method {:verify  true} containsNearbyDuplicate(nums: seq<int>, k: nat) returns (containsDuplicate: bool) 
    requires k <= |nums|
    ensures containsDuplicate ==> exists i,j :: 0 <= i < j < |nums| && j-i <= k && nums[i] == nums[j]
{
    var windowSet: set<int> := {};
    if k == 0 {
        return false;
    }

    for i: nat := 0 to |nums| 
        invariant i < k ==> forall x :: x in windowSet ==> x in nums[0..i] 
        invariant i >= k ==> forall x :: x in windowSet ==> x in nums[i-k..i]
        // invariant if i < k then forall x :: x in windowSet ==> x in nums[0..i] else forall x :: x in windowSet ==> x in nums[i-k..i]

    {
        if nums[i] in windowSet {
            return true;
        }
        windowSet := if i >= k then (windowSet -{nums[i-k]}) + {nums[i]} else windowSet + {nums[i]};
    }
    return false;
}

Loop invariants choices

Unlike the simpler version of the problem we have two regimes for our loop variable i, while it is less than k and when it is greater than or equal to k.

In Dafny you can specify multiple loop invariants, simply meaning they are additional facts that remain true as a loop iterates.

Here we can see in the loop invariant that we can write either. The loop invariant as two lines using implication.

invariant i < k ==> forall x :: x in windowSet ==> x in nums[0..i] 
invariant i >= k ==> forall x :: x in windowSet ==> x in nums[i-k..i]

invariant if i < k then forall x :: x in windowSet ==> x in nums[0..i] else forall x :: x in windowSet ==> x in nums[i-k..i]

These are both good definitions, but another good way to deal with complicated invariants is to move them into a predicate function. This is often a good strategy to try because of the concept of Triggers in Dafny, which often helps dafny recognize and prove quantifier expressions, like forall and exists.

predicate windowSetValid(nums: seq<int>, k: nat, i: nat, windowSet: set<int>) 
    requires 0 <= i <= |nums|
    requires 0 < k <= |nums|
{
    if i < k then forall x :: x in windowSet ==> x in nums[0..i]
    else forall x :: x in windowSet ==> x in nums[i-k..i]
}

Predicates

predicate functions are a subset of Dafny functions (with all the properties that entails) that only return a boolean value. Unlike a method or a function we do not need to specify a return type. The predicate keyword demands it be a bool.

However, if we replace our loop invariants with the following Dafny will no longer verify, even though the predicate function body on its own will verify.

invariant windowSetValid(nums, k, i, windowSet)

This is a case where Dafny's automatic induction fall down and we have to write a lemma to explain additional facts to Dafny.

Lemmas

lemma is like a function in Dafny, it can take parameters with require and ensure clauses, but it is only existing within the specification context and cannot be compiled to running code. It is technically a proof.

Here we specify all the things which should be true when we reach the positive if case in the loop. Then we show that if we assume those conditions are true then inside the lemma body we show that it implies the ensure clauses is true.

We can then call that lemma in other methods or functions or lemma when the required conditions are met and then Dafny can show that the ensure conditions are valid. This is basically just implication, P(x) ==> Q(x), and P(x) is true then Q(x).

lemma windowSetValidIsSufficient(nums: seq<int>, k: nat, i: nat, windowSet:set<int>)  
    requires 0 <= i < |nums|
    requires 0 < k <= |nums|
    requires windowSetValid(nums, k, i, windowSet)
    requires nums[i] in windowSet
    ensures exists i,j :: 0 <= i < j < |nums| && j-i <= k && nums[i] == nums[j]
{
    if i < k {
        assert nums[i] in windowSet;
        assert forall x :: x in windowSet ==> x in nums[0..i];
    }else{
        assert nums[i] in windowSet;
        assert forall x :: x in windowSet ==> x in nums[i-k..i];
    }
}

Assert

One of the most important tools in developing a Dafny specification is the assert operator. This has two purposes, the first is to query Dafny and see what it believes is true at a given point in a specification. Secondly, it can show Dafny that something is true and then it can use that fact to make other deductions.

Use assert often to see if what should be obvious actually is. Quite frequently Dafny will not believe you unless you show something is true using a sequence of assertions, or a calculation (another syntax construct), or a lemma.

In the above lemma, we assert the conclusions of the windowSetValid predicate being true and then Dafny sees ensure condition is valid and our method verifies when we call the lemma in the method.

This version of the method verifies using the predicate and lemma.


method {:verify  true} containsNearbyValid(nums: seq<int>, k: nat) returns (containsDuplicate: bool) 
    requires k <= |nums|
    ensures containsDuplicate ==> exists i,j :: 0 <= i < j < |nums| && j-i <= k && nums[i] == nums[j]
{
    var windowSet: set<int> := {};
    if k == 0 {
        return false;
    }

    for i: nat := 0 to |nums| 
        invariant windowSetValid(nums, k, i, windowSet)
    {
        if nums[i] in windowSet {
            windowSetValidIsSufficient(nums, k, i, windowSet);
            return true;
        }
        windowSet := if i >= k then (windowSet -{nums[i-k]}) + {nums[i]} else windowSet + {nums[i]};
    }
    return false;
}

Verify Contains Duplicate I

Aaron Elligsen — Tue, 06 Sep 2022 16:56:29 +0000

Verify LeetCode Question: 217. Contains Duplicate

Let's look at problem definition listed here

Given an integer array nums, return true if any value appears at least twice in the array, and return false if every element is distinct.

A basic implementation

Here is how we might solve it in JavaScript/TypeScript.

function containsDuplicate(nums: number[]): boolean {
    let numSet: Set<number> = new Set();
    for(let elem of nums) {
        if(numSet.has(elem)) {
            return true;
        }
        numSet.add(elem);
    }
    return false;
};

As we iterate through the array of numbers, we add each element into a set object. We check if that element has already been added and if that is true then there exists an element which is a duplicate in the array.

Verifying our implementation

There are two primary ways of defining code in Dafny, methods and functions. You can define a method that will allow multiple statements, mutable state, references to objects or classes, or calling other methods. Most code we write in traditional software development would fall under the category of a method. Methods cannot be used in specification clauses.

A function is more limited, they only allow a single expression (this is a simplification), but they can be used in specification clauses.

Verification vs implementation

When we verify a program in Dafny there are some statements which are what the code is doing. Typically traditional statements, expressions, math operations, loops, method calls, object and class instantiation found in most languages.

The real innovation and power of Dafny is that it includes specification clauses which allow us to describe what the code is intended to do! Even more importantly, it verifies that these clauses are true based on our implementation!

Contains Duplicate verification

If we look back at the LeetCode problem definition we can actually incorporate it into our specification.

An ensure clause on a function or method informs Dafny (and us) about what will be true about a value returned by it. These must be written between the function/method signature and the body.

// seq is an array-like list object
// I will use the term sequence and array interchangeably 

method containsDuplicateI(nums: seq<int>) returns (containsDuplicate: bool)

ensures containsDuplicate ==> exists i,j :: 0 <= i < j < |nums| && nums[i] == nums[j]
{
// |nums| is the length of the array/sequence
}

We can read this as, if containsDuplicate returns true that implies that there are two different indices inside the array which have the same value, aka are duplicates.

It is incredibly powerful that, not only does Dafny prove that our code is correct, it leaves us with more information about what method returning a value actually means.

To break it down further, containsDuplicate is the boolean value we are returning. The ==> symbol is the implication operator basically meaning if the expression on the left is true then the expression on the right should be true.

In this case containsDuplicate ==> exists x,y :: 0 <= x < y < |nums| && nums[x] == nums[y] we use the existential quantifier to specify what a duplicate means. The expression can be read like this: there exists an x and a y such that ::, x and y are numbers/indices between 0 and the length of the array and num[x] equals num[y].

Contains Duplicate I Verification

The Dafny code is a straightforward translation of the TypeScript version. The syntax has a few differences naturally.

method containsDuplicate(nums: seq<int>) returns (containsDuplicate: bool)

ensures containsDuplicate ==> exists i,j :: 0 <= i < j < |nums| && nums[i] == nums[j]
{
    var numSet: set<int> := {};
    for i:= 0 to |nums|
        invariant forall x :: x in numSet ==> x in nums[0..i]
    {
        if nums[i] in numSet {
            return true;
        }
                //+ is overloaded to set union
        numSet := numSet + {nums[i]};  
    }
    return false;
}

In the for loop, between the loop condition and the body, we assert another specification clause called a loop invariant. A loop invariant is an expression which must be true before the loop starts, after every step of the loop, and after it is finished.

In this case, it says that everything in numSet is from the values in the slice of the array which starts from 0 up to but not including i, so nums[i] is not included.
Clearly, this tracks with our intuition which is that everything in array which is less than the current index is in the set.

If we do encounter an element nums[i] which is already in the numSet, then we know that there is some index x, less than our current index i, which has the same value in the array nums. If we make it all the way through the array but do not find a matching element in the set then we return false.

Tricky details of invariants

This is a simple coding problem in most languages and in Dafny, but the loop invariant forall x :: x in numSet ==> x in nums[0..i] is carefully chosen to create a connection between numSet and nums.

The converse forall x :: x in nums[0..i] ==> x in numSet seems equally valid but it is not and it will not verify. This direction of implication tells us only about some things in numSet, there could be more elements in numSet that came from before the loop or some other step. In other words if something was in numSet, we couldn't guarantee that it was also in nums.

When evaluating loop invariants Dafny uses induction, it assumes the loop invariant was true of the last loop. It then runs the body and checks if logically the invariant was maintained. Dafny does not do a brute force exhaustive check of all possible program states.

Creating useful loop invariants is difficult. It is definitely a skill to be learned and not every true invariant about a problem will be automatically provable to Dafny. Quite often you may need to provide extra logic to Dafny to convince it that it is true.

Dafny programming language and software verification system

Aaron Elligsen — Tue, 06 Sep 2022 16:54:50 +0000

What is Dafny?

Dafny is a programming language which is designed to help developers prove that their software is correct. Most consider this the domain of mission critical software where there are serious costs or consequences of software errors, but it can be used on everyday software as well!

If you are interested in learning why your software is correct or why it works, verifying it with Dafny will make it clear. It helps take your intuition about a program and make it rigorous.

Quite a lot of programming can be done with trial and error, but often it can be long and frustrating when you don't understand a system well and seemingly random permutations result in working code or not. Often, it can lead to doubt about whether a particular solution is always correct. Unit tests can help, but they can only prove the presence of bugs on specific examples.

A verified program is mathematically guaranteed to be correct on all valid input.

Why Dafny?

Dafny was developed by Rustan Leino, formerly of Microsoft Research. It is still under active development.

It has a similar syntax to C# or TypeScript or many other C inspired languages. It is a huge language with many powerful constructs that map to common situations and patterns in most common programming languages used today.

It's a practical language

There are other formal verification languages which are based on functional programming languages or type theory and pure logic. These languages can and are used to verify software, but if you want to verify a small piece of your web application you have to learn a completely different paradigm and syntax before you can get to doing something useful.

I find Dafny very approachable and familiar as a professional web developer.

Challenges ahead

As mentioned Dafny is still under development and the documentation is a bit lacking still. In that vain this series intends to provide many examples and explain how to verify different programs.

Familiarity with mathematics

Dafny can prove many things but often we must explain non-trivial properties to help Dafny verify our software. This is based on mathematical logic and induction. Dafny has a system and syntax specially designed to allows us to prove things to Dafny.

Unfortunately, Dafny cannot prove everything we want automatically and there are many sharp edges when we write our proofs in Dafny. However, it is a powerful system which beautifully brings the world of mathematics into an approachable and understandable context of software development.

Getting Started

Dafny is now easily packaged into a Visual Studio Code extension. Installing the extension and then creating a file with the .dfy extension will immediate set you into a dafny environment and you can begin writing and verifying your algorithm.

Go read and tryout the Dafny Getting Started Guide

Learning Dafny

After reading the guide, it is time to start practicing verification on simple coding problems. Here in this series we will implement and verify a large number of algorithms and coding problems.

DEV Community: Aaron Elligsen

Verified Ordered Set in Dafny

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

The Big Picture: What Are We Building?

The Foundation of Correctness: The Valid() Predicate

Implementing the Methods: From Specification to Proof

IncreaseSize(): Making Room for More

AddValue(): The Main Event

Defining and Proving Properties of Pure Functions

The Function and Its Specification

Proving a Property: The ToSetConcat Lemma

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

The Proof of Equivalence

From Specification to Implementation: Writing a Provably Correct Binary Search

Step 1: Defining the Contract

Step 2: The Implementation and the Loop Invariant

How Dafny Proves It

Conclusion: Code That Proves Itself

What's next?

Verifying Count Equal and Divisible Pairs in an Array

Verifying Leetcode question 2176. Count Equal and Divisible Pairs in an Array

Verifying Invert Binary Tree

Verifying LeetCode Problem: 266. Invert Binary Tree

An implementation

Classes in Dafny

Class Method

Verify Climbing Stairs

Verify LeetCode Question: 70. Climbing Stairs

Implementation

Specifying the implementation

Verifying the implementation

Proving the base cases

Proving the induction

Sets and their usefulness

Sets

A Container and its methods

Constructor

Add

Delete

Has - the membership test

JavaScript Aside: the keyword in

Mathematical Operations

Subset/Superset

Equality

Union

Intersection

Symmetric Difference

Difference

Complement

Mathematical Laws

Subset laws

Identity Laws

Domination Laws

Idempotent Laws

Complementation Law

Commutative Laws

Associative Laws

Distributive Laws

De Morgan's Laws

Absorption Laws

Complement Laws

Patterns

JavaScript Caveats

JavaScript Alternatives

Links

Writing lemmas in Dafny

Lemmas

Direct Proof: An example on Relations

Union of relations?

Proofs by contradiction in Dafny

Verifying Valid Anagram

Verifying LeetCode Problem: 242. Valid Anagram

Theory

An implementation

Specifying the problem

isAnagram

toMultiset

msetEqual

Full definition

Final thoughts

The Foundation of Correctness: The `Valid()` Predicate

`IncreaseSize()`: Making Room for More

`AddValue()`: The Main Event

Proving a Property: The `ToSetConcat` Lemma

JavaScript Aside: the keyword `in`