Software Specification: Classes, Class Invariants, and Dynamic Frames

Software Specification, MEIC @ IST, 2019/20

jff

### At the end of this session, you should be able to: - Define new classes in Dafny - Define class invariants - Describe and implement the standard idiom for using dynamic frames in Dafny - Verify OOP code in a modular way

## A brief review of last session...

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)

datatype List = Nil | Cons (head: T, tail: List)

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)

Example (from last week's lab):

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

First, prove the property for the base case Nil

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

Second, prove property for Cons(h,x)

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

x

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

Exercise

Use Dafny to prove this lemma.

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

Classes in Dafny

class Cell {
    var data: int;

    constructor ()
        ensures data == 0
    { data := 0; this.data := 0; }

    method setValue(v: int)
        ensures data == v
        modifies this
    { data := v; }

    method Main() {
        var c1 := new Cell(); c1.setValue(5);
    }
}

Familiar, but...

The ability to write predicates and assertions is new and increases confidence in our code.

Class invariants

Class invariants are properties that must hold at the entry and exit point of every method, for every instance of a class
They often express properties about the consistency of the internal representation of an object
They are typically transparent to clients of an object
They are sometimes also called object invariants or instance invariants.

Example: An Odd Stack

Let us implement a stack that can only contain odd integers.

The Problem with Class Invariants

In the previous example, the invariant was defined directly on the internal representation.

However, in Dafny, it's very common to define class invariants in terms of so-called ghost variables.

Ghost variables are declared with the modifier ghost, and are used only at verification time; they are not compiled into variables that are allocated and updated when the program is run, so we do not need to worry about the impact on performance that manipulating these variables would otherwise have.

Example: A Simple Counter

Let us look at the simple counter in Counter.dfy, where the invariant also uses a ghost variable.

Dynamic memory allocation

The simple counter is not that different from the stack example that we saw before. However, things are not so easy when dealing with dynamic memory...

Let's see what happens if we change incs and decs to be references to some object in memory.

The Dynamic Frames Approach

Solution used in Dafny: Dynamic Frames
- each object only keeps track of its own invariants
- each object maintains a ghost field for its own representation frame
- frames of different objects are kept separate by adding appropriate disjointness constraints
- yields compositional verification approach
- The idea behind Dynamic Frames is the introduction in the abstract vocabulary of the footprints of methods and functions.

Counter Example

Let's revisit our Counter example and rewrite it using the standard idiom for dynamic frames in Dafny.

Dynamic memory allocation

Note that framing only applies to the heap, or memory accessed through references. Local variables are not stored on the heap, so they cannot be mentioned in reads annotations.
Note also that types like sets, sequences, and multisets are value types, and are treated like integers or local variables.
Arrays and objects are reference types, and they are stored on the heap.

Verification of object-oriented code

The concepts discussed today are essential to verify code written in OOP style.

As an example, let us see how one could verify a library for binary search trees.

Summary

Class invariants are a natural way of expressing properties about objects
Dynamic frames are a key feature of Dafny that allow us to scale to larger programs