Software Specification: Structural Induction, Lemmas (cont.), and Dafny/C#

Software Specification, MEIC @ IST, 2019/20

João F. Ferreira

Algebraic Inductive Datatypes

• We have already seen an example:

  datatype Colour = Red | White | Blue

• A more interesting example is:

  datatype Nat = Zero | Succ(n: Nat)

• The values of inductive datatypes can be seen as finite trees where the leaves are values of basic types, numeric types, etc.
  • Zero, Succ(Zero), Succ(Succ(Zero)), etc.

Algebraic Inductive Datatypes

• Values of inductive datatypes can be compared using Dafny’s well-founded < ordering.
  • Example: Zero < Succ(Zero) < Succ(Succ(Zero))
• Values of algebraic datatypes can be analysed using pattern matching:

  function add(n1: Nat, n2: Nat): Nat 
  {
      match n1
          case Zero    => n2
          case Succ(n) => Succ(add(n, n2))
  }
  

Lemmas and Calculations

• We may express properties of our programs using lemmas. Lemmas are implicitly ghost methods (i.e. methods that are not compiled into the executable).

  lemma add_unit(n: Nat)
      ensures add(n, Zero) == n
      ensures add(Zero, n) == n
  {} 
  
  lemma add_succ(n1: Nat, n2: Nat)
      ensures Succ(add(n1,n2)) == add(n1, Succ(n2))
  {}
  

• Note that if we don't include the {}, then it's an axiom (i.e., we assume it to be true).

Lemmas and Calculations

• The previous lemmas are proved automatically by Dafny. However, there are cases where Dafny needs our assistance. For example:

  lemma add_commutative(n1: Nat, n2: Nat)
      ensures add(n1, n2) == add(n2, n1)
  {}
  

Induction over Natural Numbers

• Recall the principle of induction over natural numbers: If we want to show that $P$ holds for all numbers $n$, we:
  1. show that $P(0)$ holds;
  2. show that, for any $n'$, if $P(n')$ holds, then so does $P(Succ(n'))$;

Lemmas and Calculations

• We prove the lemma using induction on the first argument:

lemma {:induction n1} add_commutative(n1: Nat, n2: Nat)
    ensures add(n1, n2) == add(n2, n1)
{
    match n1
        case Zero =>
            calc {
                add(Zero, n2);
                == // def. add
                n2;
                == { add_unit(n2); }
                add(n2, Zero);
            }
        case Succ(n) => 
          // Inductive hypothesis: add(n, n2) == add(n2, n)
}

Lemmas and Calculations

• Inductive step:

case Succ(n) =>
            // Inductive hypothesis: add(n, n2) == add(n2, n)
            calc {
                add(n1, n2);
                == // n1 == Succ(n)
                add(Succ(n), n2);
                == // def. add
                Succ(add(n,n2));
                == // IH: add(n, n2) == add(n2, n)
                Succ(add(n2,n));
                == { add_succ(n2, n); }
                add(n2, Succ(n));
                == // Succ(n) == n1
                add(n2, n1);
            }

Activity: Let's define together a functional library to manipulate Lists.

datatype List = ...

Structural Induction

• To prove that $P(x)$ holds for all values $x$ of a recursively-defined datatype $T$, we prove:
  1. $P(b)$ holds for each base case $b \in T$
  2. $P(c(x))$ for each constructor, $c$, assuming induction hypothesis $P(x)$

Structural Induction (For Lists)

• To prove that $P(x)$ holds for all values $x$ of the type List, we prove:
  1. $P(Nil)$
  2. $P(Cons(h,x))$ assuming induction hypothesis $P(x)$ (and for arbitrary $h$)

Structural Induction (For Lists)

lemma reverse_append<T>(l1: List<T>, l2: List<T>)
  ensures reverse(append(l1, l2)) == 
          append(reverse(l2), reverse(l1))

1. First, prove the property for the base case Nil          

   reverse(append(Nil, l2)) == append(reverse(l2), reverse(Nil))

2. Second, prove property for Cons(h,x)

   reverse(append(Cons(h,x), l2)) == 
   append(reverse(l2), reverse(Cons(h,x)))

assuming that the property is valid for x

reverse(append(x, l2)) == append(reverse(l2), reverse(x))

Lemmas

• We have been writing lemmas about functional code and we have been writing calculations to provide manual proofs
• But lemmas can be used with imperative code, too.
• And our proofs can be written using annotated code!
• To illustrate this, let's consider a very simple searching algorithm: finding zeros in a specific class of arrays.

Example: Searching for Zero

• We will consider a somewhat contrived example: searching for zero in an array. What makes this problem interesting is that the array we are searching in has two special properties:
  1. all elements are non-negative, and
  2. each successive element decreases by at most one from the previous element
• As before, our program should return an index of where zero occurs; a negative index if there are no zeros.

Linking Dafny and C# code

• Dafny can be extended by binding trusted Dafny interfaces to C# code
• Useful to enable IO computations, such as reading command-line arguments and file manipulation
• For the second project, we provide classes to deal with the filesystem and command line arguments.

Linking Dafny and C# code: First Example

Consider the following C# code:

using System.Numerics;

namespace _module
{
    public partial class SoftSpecExample 
    {
        public static void sum2(BigInteger x, 
                                BigInteger y, 
                                out BigInteger r)
        {
            r = x + y;
        }
    }
}

Linking Dafny and C# code: First Example

We can create a trusted interface in Dafny:

class SoftSpecExample 
{
  static method {:extern} sum2(x: int, y: int) returns (r: int)
     requires 0 <= x <= y
     ensures r == x + y
}

• Note that there is no implementation. The {:extern} attribute means that the implementation is defined externally.
• Crucially, it provides the contract of the C# code.

Linking Dafny and C# code: First Example

We can now interact with the method sum2:

include "sumInterface.dfy"

method Main()
{
    var x := SoftSpecExample.sum2(20, 30);
    assert x == 50;
    print "Sum: ", x, "\n";
}

• To compile this program, we need to pass the C# file as an argument. Example:

  dafny sum.dfy sumNative.cs

Demo

Let's use the files provided with Project 2 to write a program that executes the verified "Dutch Flag algorithm" with a string of letters received as command-line argument.

Example:

./dsort.exe RWBBBWWRWRWBWRWRW
RRRRRWWWWWWWWBBBB

Credits

• These slides use the framework reveal.js and were produced using vim and Ubuntu.
• Some slides and examples are based on material available online by Rustan Leino. Some material is taken from Dafny's tutorial.