# Verifying Selection Sort: an Introduction to Program Verification in Dafny

## Introduction

Dafny is a programming language. It should be familiar to anyone with experience with languages like Java or C#. In a nutshell, it is characterized by:

- A strong and static type system
- Class-based object-orientation, with trait-based inheritance
- Functional programming features and a module system

The key characteristic that makes Dafny quite different from most other programming languages is that it is designed with formal verification in mind. In Dafny, you can annotate your code to mathematically formalize its specification, and verify that your code is correct with respect to its specification. Dafny is not just designed to support object-oriented programming and functional programming, but also verified programming.

We're going to introduce verified programming in Dafny to give a concrete idea of what it feels like to write verified software. All you need to follow is some experience with a Java-like language and a vague recollection of selection sort.

## An Unverified Implementation of Selection Sort

Dafny is a full-fledged programming language and you may even want to use it if you have no interest in verification whatsoever. In fact, writing unverified Dafny program is a good way to get familiarity with the language. Following is one possible implementation of selection sort in Dafny.

```
method {:verify false} SelectionSort(a: array<int>)
{
for i := 0 to a.Length
{
var minValue := a[i];
var minPos := i;
for j := i + 1 to a.Length
{
if a[j] < minValue {
minValue := a[j];
minPos := j;
}
}
if i != minPos {
a[i], a[minPos] := minValue, a[i];
}
}
}
```

Selection sort is implemented as a method named `SelectionSort`

(which
need not belong to a class) that takes as an input parameter an array
of integers `a`

of type `array<int>`

. It sorts the array in place
using two local variables declarations, two nested for loops,
conditional statements, and assignments. Our method is marked as
`{:verify false}`

because we do not want verification to kick in yet.

Let's write a `Main`

method to run our program and check that it works,
at least on this one example.

```
method Main()
{
var a: array<int> := new int[3];
a[0] := 2; a[1] := 4; a[2] := 1;
SelectionSort(a);
print a[..];
}
```

If you copy and paste these two methods into a file, say `isort.dfy`

,
install dafny, and run `dafny run isort.dfy`

on the command line, you
will see the message:

```
Dafny program verifier did not attempt verification
[1, 2, 4]
```

## Verifying the Absence of Runtime Errors

We start our verification effort by proving the absence of runtime
errors (no division by 0, indexing outside of the bounds of an array,
etc…). In a statically and strongly typed language like Java, these
would take the form of exceptions. In Dafny, however, there are no
exceptions and one must prove that there is never any reason to throw
one, so to speak. All we need to do to undertake this verification is
to remove `{:verify false}`

. Doing so would reveal two error messages
from the verifier, both of which are reported on the line where
the content of two of the array's locations are swapped.

`assignment might update an array element not in the enclosing context's modifies clause`

`index out of range`

The first error reminds us that in a language like Dafny, a method
must explicitely be allowed to make modifications to a memory
reference such as `a`

. We therefore need to refine the signature of
our method with the clause `modifies a`

. This aspect of Dafny will not
play an important role in our example, and it is good enough to know
that to make reasoning simple and modular, methods in Dafny must be
explicit about what part of memory they have access to.

The second error reported is more interesting because it raises a key
question: do we actually have an index out of range access in our
code, or is it that the automation failed to verify that it is the
case on its own? In this case, it is the latter, and the verifier
needs some help in the form of an *invariant*. For concreteness, let's
consider a version of our code with enough annotation to pass
verification.

```
method SelectionSort(a: array<int>)
modifies a
{
for i := 0 to a.Length
{
var minValue := a[i];
var minPos := i;
for j := i + 1 to a.Length
invariant minPos < a.Length
{
if a[j] < minValue {
minValue := a[j];
minPos := j;
}
}
if i != minPos {
a[i], a[minPos] := minValue, a[i];
}
}
}
```

Note that the verified implementation is quite close to the unverified
one. Aside from the modifies clause, the only difference between the
unverified implementation and the one for which we verify the absence
of runtime errors is the invariant statement that is attached to the
innermost for loop. One of the fundamental design principles of Dafny
is that programming and verification should be integrated, and you
should be able to reason about your code directly, in this case by
directly annotating one of the for loop with a hint for the
verifier. To understand both why we need such an annotation, but also
why we *only* need this annotation for verification to pass, it is
useful to have a vague understanding of how verification works in Dafny.

Our verified selection sort comes with two key ingredients: code and
specification. We do not have an explicit specification yet, but we do
have an implicit one: in order to prove the absence of runtime errors,
we must ensure that accesses to the array are within bounds, which the
verifier must establish. To verify that the code meets the spec with
mathematical certainly, testing will not do. Instead, the Dafny
compiler transforms the specification and the code into a mathematical
formula. If we can prove that this mathematical formula is true, then
the code satisfies the specification. Otherwise it may or may
not. Proving such mathematical formula would be a lot of work, so
Dafny makes use of an *automated theorem prover* (ATP) to prove it on
your behalf.

Alas, ATPs have fundamental limitations and while they excel at proving properties of linear code, they need some help with loops. Fundamentally, they need to know of properties that are true when the loop starts its execution, remain true after execution of the loop, and imply what needs to be true after execution of the loops. This is called an invariant property because it captures what does not change despite all the complicated changes that may happen during execution of the loop.

Without the invariant annotation, the verifier reported that it could
not establish that `minPos`

is within bound. It is indeed difficult to
establish since it is modified within the loop. However, it should
always be true that `minPos`

is less than `a.Length`

since it
indicates the position of a value in the array that is smaller than
the one under consideration in the outer loop. Therefore, we can help
verification by annotation the for loop with `invariant minPos < a.Length`

.
The verifier is not only able to verify that this property
is indeed an invariant of the loop, but this turns out to be enough
information for the verification to succeed.

## Verifying the Functional Spec: Output Array is Ordered

While it is generally useful to verify the absence of runtime errors,
we would now like to verify the specific behavior of our selection
sort implementation, its *functional specification*. There are several
properties that characterize the functional behavior of a sorting
algorithm, one of which is that once the computation is done, the
values in the array should be ordered. Before we can do the actual
verification, we need to specify what we expect of selection
sort. First, we need to formalize what it means for an array to be
ordered.

In English, we might say something like: *Definition: an array is
ordered if for any non-negative integer value i ranging from 0 to the
length of the array, exclusive, the value at index i is less than the
value at index i+1*. With more formal notation, we might also say:
*Definition: an array a of length l is ordered if and only if for all i
in [0,l), a[i] <= a[i+1]*.

In Dafny, we do not write our specifications in English but instead in
a formal language. As a first approximation, the formal language is
that of formal mathematics, in a syntax that closely resembles the
syntax of Dafny's expressions. In Dafny, such a definition is called a
`predicate`

.

```
ghost predicate Ordered(a: array<int>, left: nat, right: nat)
reads a
requires left <= right <= a.Length
{
forall i: nat :: 0 < left <= i < right ==> a[i-1] <= a[i]
}
```

There's a lot to unpack in this example. First note that we define a
predicate `Ordered`

with three typed parameters. The first parameter,
`a`

, is the array. The two extra parameters, `left`

and `right`

allow
us to generalize the definition to a sub-range, which will be useful
later on.

The body of the predicate,
`forall i: nat :: 0 < left <= i < right ==> a[i-1] <= a[i]`

,
is the definition itself. This definition is a
mathematical proposition, as hinted by the keyword `forall`

. This
proposition may or may not be computable.

Our predicate definition is prefixed with the keyword `ghost`

to
indicate that it is meant to be used for specification purposes and
need not be compiled or be included in the executable. In some cases,
the keyword may be required if the predicate is truly a non-computable
mathematical formula.

The two clauses that follow the declaration of the predicate are
relevant to verification. The first clause, `reads a`

makes it
explicit that the predicate reads the array a. This will not play an
important role in our example. It is the dual of the modifies clause
we encountered previously, and for now it is good enough to know that
these clauses are important to keep verification simple and modular.

The second clause, `requires left <= right <= a.Length`

, is a
precondition that restricts the definition to values of `left`

,
`right`

, and `a.Length`

to ones satisfying that precondition. Such
preconditions are a fundamental feature of Dafny that allow for the
definition of partial functions. It may not be obvious at first sight,
but this is highly valuable to writing efficient code, since you can
define partial functions and ensure statically that they will not be
used outside of their intended domain of definition, removing any need
for checking arguments at runtime and making your code throw an
exception (recall: Dafny does not have exceptions!), or worse, returning a
dummy value.

Now that we are done formalizing what it means for an array to be
ordered, we can revisit our implementation of selection sort and
ensures, with mathematical certainty, that the code satisfies our
specification. To attach the specification to the implementation, we
annotate the method with a clause `ensures Ordered(a,0,a.Length)`

that
establishes that any execution of `SelectionSort`

should result in an
array `a`

that satisfies the predicate `Ordered(a,0,a.Length)`

. We
call such clause a postcondition.

```
method SelectionSort(a: array<int>)
modifies a
ensures Ordered(a,0,a.Length)
{
for i := 0 to a.Length
invariant Ordered(a,0,i)
{
var minValue := a[i];
var minPos := i;
for j := i + 1 to a.Length
invariant minPos < a.Length
{
if a[j] < minValue {
minValue := a[j];
minPos := j;
}
}
if i != minPos {
a[i], a[minPos] := minValue, a[i];
}
}
}
```

To help with the verification, we provided more annotation, in the form
of invariants. Selection sort works by incrementally ordering the
array, maintaining the property that the sub-array up to the position
of the outer index `i`

is ordered. We therefore capture this with an
invariant annotation that we attach to the outer loop
`invariant Ordered(a,0,i)`

.

This example is a good example of how effective automation can be. The
verification effort reduces to the specification of a single
invariant, which captures formally what one might write as a comment
to justify the correctness of our implementation. In fact, it is not
even necessary! You could comment it out and verification would still
succeed. It is still valuable to add for documentation purposes and to
help the verifier. In fact, you could add more invariant properties to
confirm your intuition about what the verifier is proving, for example
by adding the invariant
`forall k: nat :: i <= k < j ==> minValue <= a[k]`

to the inner loop.

## Verifying the Functional Spec: Values are Preserved

Our functional specification of selection sort can be improved. Aside
from ensuring that the algorithm makes the array ordered, we also need
to ensure that the values in the array after sorting are the same ones
as before. More formally, we want to ensure that the multiset of
values of the array before and after sorting are equal. We capture
this definition with another predicate, `Preserved`

.

```
twostate predicate Preserved(a: array<int>, left: nat, right: nat)
reads a
requires left <= right <= a.Length
{
multiset(a[left..right]) == multiset(old(a[left..right]))
}
```

This definition introduces a few new interesting concepts. First, the
expression `multiset(a[left..right])`

shows an example use of not one
but two of Dafny's built-in collection types. The subexpression
`a[left..right]`

transforms the sub-array into a *sequence* (or list)
of values. The expression `multiset(a[left..right])`

creates a
multiset from that sequence. You might think that while this notation
is conveniently succinct, the performance of this code will suffer, but
remember, this is part of the specification, and this will have no
impact on the runtime performance of our selection sort
implementation.

Second, note that while predicate `Ordered`

captures a property that
is intrinsic to the array, our new predicate is meant to capture a
relation between the input and the output of selection
sort. Therefore, we need to be able to refer to the array both before
execution of selection sort and after. This is done thanks to the use
of the `twostate`

prefix that declares that the predicate is a
relation between a heap-allocated object before and after execution of
some method, and the expression `old`

that refers to the array before
execution. Other mentions of `a`

refer to that array after execution
of the method.

We can combine our two predicates, `Ordered`

and `Preserved`

into one,
`Sorted`

, that will be the final functional specification of our
implementation.

```
twostate predicate Sorted(a: array<int>)
reads a
{
Ordered(a,0,a.Length) && Preserved(a,0,a.Length)
}
```

We attach this specification to our method as a postcondition and refine our verification efforts accordingly with new invariant annotations.

```
method SelectionnSort(a: array<int>)
modifies a
ensures Sorted(a)
{
for i := 0 to a.Length
invariant Ordered(a,0,i)
invariant Preserved(a,0,a.Length)
{
var minValue := a[i];
var minPos := i;
for j := i + 1 to a.Length
invariant minPos < a.Length
invariant a[minPos] == minValue
{
if a[j] < minValue {
minValue := a[j];
minPos := j;
}
}
if i != minPos {
a[i], a[minPos] := minValue, a[i];
}
}
}
```

Unlike `Ordered`

which is invariant up to the index `i`

, `Preserved`

is invariant on the entire array and throughout the execution of the
method, and it is an invariant of the outer loop. Unfortunately, this
would not be quite enough for the verification to succeed. Note that
we have not said much about the inner loop yet. It searches for the
smallest value in the suffix of the array and this value is swapped
with the value at the current index of the outer loop. It should be
the case that `minPos`

and `minValue`

be in sync, and we add the
invariant `invariant a[minPos] == minValue`

to capture this property.

With these invariant annotations, Dafny can verify on its own, in an instant, that the body of the method indeed satisfies the postcondition, which specifies that the array is ordered and contains the same values as when the method was called.

## Generic Selection Sort

To keep things simple, we have thus far assumed that the input array
contains integers. Now we would like to abstract our implementation so
that it can sort an array for any values as long as they can be
compared. In Dafny, we would do this using a *trait*. If you're not
familiar with the concept, you can think of it as an interface which
may contain code. We define a trait of `Comparable`

values.

```
trait Comparable<T(==)> {
function Lt(x: T, y: T): bool
}
```

Our trait is generic and parameterized by a type `T`

. The suffix
`(==)`

is a *type characteristic* that will ensure that our trait is
only instantiated on types for which it is possible to test whether
two values are equal. The trait contains a single declaration for a
function `Lt`

that takes two parameters of type `T`

and returns a
Boolean value.

In Dafny, we make a distinction between *methods* and *functions*. As
a first approximation, you can think of them as the imperative and the
functional version of a computation, respectively. While the body of
methods is made of a sequence of statements, the body of a function is
an expression. While a method can declare mutable local variables and
modify heap-allocated values, functions are, as a first approximation,
free of side effects and state. In general, when a choice between a
method and a function is possible, it is wise to choose using a
function as it makes verification easier, which is why we choose to
define `Lt`

as a function.

We extend the `Comparable`

trait to define a new one, `Sorted`

that
will group together our predicates for specification.

```
trait Sorted<T(==)> extends Comparable<T> {
ghost predicate Ordered(a: array<T>, left: nat, right: nat)
reads a
requires left <= right <= a.Length
{
forall i: nat :: 0 < left <= i < right ==> Lt(a[i-1],a[i]) || a[i-1] == a[i]
}
twostate predicate Preserved(a: array<T>, left: nat, right: nat)
reads a
requires left <= right <= a.Length
{
multiset(a[left..right]) == multiset(old(a[left..right]))
}
twostate predicate Sorted(a: array<T>)
reads a
{
Ordered(a,0,a.Length) && Preserved(a,0,a.Length)
}
}
```

We can now define selection sort in a trait `SelectionSort`

where the
type of values is abstract but extends the traits `Comparable`

and
`Sorted`

.

```
trait SelectionSort<T(==)> extends Comparable<T>, Sorted<T> {
method SelectionSort(a: array<T>)
modifies a
ensures Sorted(a)
{
for i := 0 to a.Length
invariant Ordered(a,0,i)
invariant Preserved(a,0,a.Length)
{
var minValue := a[i];
var minPos := i;
for j := i + 1 to a.Length
invariant minPos < a.Length
invariant a[minPos] == minValue
{
if Lt(a[j], minValue) {
minValue := a[j];
minPos := j;
}
}
if i != minPos {
a[i], a[minPos] := minValue, a[i];
}
}
}
}
```

Dafny is designed in such a way that verification is unaffected by this abstraction and the verification effort is unchanged.

Traits, unlike classes, cannot be instantiated, so if we want to use our selection sort implementation, we need to define a class that extends the trait. You might wonder why we did not define selection sort in a class directly: it is because in Dafny, a class cannot extend another class! This unusual design ensures that you can benefit from multiple inheritance while keeping verification reasonable simple. Nevertheless, you should still be able to design your code following the core precepts of object-oriented programming: inheritance, subtyping, late binding, overriding, encapsulation, and dynamic dispatch.

We therefore define a class `Sort`

that extends `SelectionSort`

and
complete its implementation.

```
class Sort<T(==)> extends SelectionSort<T> {
const CMP: (T,T) -> bool
constructor(cmp: (T,T) -> bool)
ensures CMP == cmp
{
CMP := cmp;
}
function Lt(x: T, y: T): bool {
CMP(x,y)
}
}
```

The class is made of typical members such as fields, constructors,
methods, and functions. A constant (or immutable) field `CMP`

holds
our comparison function and is set by the constructor. Function `Lt`

that was declared in the `Comparable`

trait is implemented. We can see
a glimpse of the functional programming side of Dafny: it
is possible to pass a function as an argument to a
method/function/constructor and to store it in a field.

We can now write a `Main`

method to test our generic selection sort.

```
method Main()
{
var a: array<int> := new int[3];
a[0] := 2; a[1] := 4; a[2] := 1;
var Sort := new Sort((x: int, y: int) => x < y);
Sort.SelectionSort(a);
print a[..];
}
```

## Verifying the Runtime Complexity

There is a lot more we could prove about our selection sort implementation. For example, you may try to prove that selection sort is stable. Instead, we will prove properties about the runtime complexity of our implementation. This will give us a chance to introduce more interesting concepts. Recall that when studying the runtime complexity of a sorting algorithm we usually count either the number of comparisons, or the number of swaps. In this example, we will focus on establishing a bound on the number of comparisons. More specifically, we want to show that if the input array is of size N, the number of comparisons will be less than N * N.

To that end, we extend trait `Comparable`

to define a new trait
`Measurable`

. The purpose of this trait is to keep track of the number
of times we call the comparison function.

```
trait Measurable<T(==)> extends Comparable<T> {
ghost var comparisonCount: nat
method Ltm(x: T, y: T) returns (b: bool)
modifies this`comparisonCount
ensures b ==> Lt(x,y)
ensures comparisonCount == old(comparisonCount) + 1
{
comparisonCount := comparisonCount + 1;
b := Lt(x,y);
}
}
```

A crucial detail is that we are declaring a mutable field,
`comparisonCount`

as `ghost`

. This is because while we do need a
variable to keep track of the number of times the comparison function
has been called, we do not want this variable and its counting to
affect the performance of our code! By declaring the field as `ghost`

,
we ensure that it will be removed by the compiler.

The `Measurable`

trait defines method `Ltm`

that calls our comparison
function but also increment the counter. Because the counter is ghost,
the statement that increments it will be removed by the
compiler. Because `Ltm`

modifies the state of the object it belongs
to, it needs to declare `modifies this`

. In fact, to simplify
verification, we declare more specifically that we modify one specfic
field of the object as `modifies this`comparisonCount`

.

At a high-level, a pencil-and-paper proof would look something like
this. Assume that the array is of size N. At every iteration of the
outer loop, if the index is at position i, the inner loop will do
roughly N - i comparisons. All in all, it means that the number of
comparison will be something like N + (N-1) + … + 1. In preparation
for reasoning about such a summation, we define a function `Sum`

.

```
ghost function Sum(x: int): nat
{
if x <= 0 then 0 else x + Sum(x-1)
}
```

Even though this function is not used in the specification, we declare
it `ghost`

to clarify that it is used only as part of the mathematical
reasoning and should be understood as a function in the mathematical
sense.

We can add a second postcondition to our method. It states that executing the method does not increase the number of counts by more than square of the size of the array. Of course, we can expect to add additional invariants to loops to help the verification of our complexity property.

```
trait SelectionSort<T(==)> extends Comparable<T>, Measurable<T>, Sorted<T> {
method SelectionSort(a: array<T>)
modifies a, this
requires comparisonCount == 0
ensures Sorted(a)
ensures comparisonCount <= a.Length * a.Length
{
for i := 0 to a.Length
invariant Ordered(a,0,i)
invariant Preserved(a,0,a.Length)
invariant comparisonCount == i * a.Length - Sum(i)
{
var minValue := a[i];
var minPos := i;
assert comparisonCount == i * a.Length - Sum(i) + (i + 1 - i) - 1;
for j := i + 1 to a.Length
invariant minPos < a.Length
invariant a[minPos] == minValue
invariant Preserved(a,0,a.Length)
invariant comparisonCount == i * a.Length - Sum(i) + (j - i) - 1
{
label L:
var cmp := Ltm(a[j], minValue);
assert a[..] == old@L(a[..]);
if cmp {
minValue := a[j];
minPos := j;
}
assert(i * a.Length - Sum(i) + (j - i) - 1) + 1 == i * a.Length - Sum(i) + ((j + 1) - i) - 1;
}
if i != minPos {
a[i], a[minPos] := minValue, a[i];
}
assert comparisonCount == (i+1) * a.Length - Sum(i+1);
}
}
}
```

In this case, verification required a little more information than
just the loop invariants. Also, the invariants are more complicated
than what you might have expected from the high-level explanation for
the complexity bound, but this is because in the inner loop, we need to
keep a precise count of how many comparisons are being done. This is
the kind of reasoning that is intuitive, difficult to do precisely on
paper, usually ignored, and the source of subtle errors. Thanks to
Dafny though, we can flesh out a rigorous argument with confidence
that the correct expression is `(i + 1 - i)`

and not `(i - i)`

, for
example.

Note that we have added a few `assert`

statements that can be
understood as hints of a property that ought to hold at the position
where it is stated. The point of such assertions is to break down the
proof and provide hints to the ATP by stating intermediate properties
that can be potentially easier to verify but will play a key role in
the overall proof. Take
`assert comparisonCount == (i+1) * a.Length - Sum(i+1);`

for example. This is letting the verifier know of a useful
identity between `Sum`

and `comparisonCount`

.

Another example, probably much more mysterious, is
`assert a[..] == old@L(a[..]);`

.
It states that the values of the array are the same at
the point in the program labeled `L`

and the one where the assertion
is made. By default, the `old`

expression refers to the state of the
method at the beginning of execution, but it can be modulated to refer
to a specific line in the body of the statement.

You may try to understand what these assertions mean and why they are useful, but the point of this discussion isn't to understand how to verify the complexity of selection sort, but rather to address the most important frustrations of new Dafny users: how do we know what assertions to make and where? In hindsight, all these assertions might seem true and relevant, but it doesn't say anything about how to come up with them, and to new Dafny users, it might seem like a magic incantation.

It is crucial to understand that these are not, in fact, magic
incantation that only people trained as mathematicians can
spell. Dafny is not just a full-fledged programming language, it is
also a full-fledged *proof assistant*. There is a systematic way to
figure out how to convince Dafny that a result is true if it is indeed
the case. It may not always be trivial, and it requires some training,
but you can rest assured that if there is a proof, you ought to be
able to provide enough information for the verification.

Consider again the obscure case of `assert a[..] == old@L(a[..]);`

.
It would be unrealistic to have to know so much about verification to
just guess that verification needs this specific property at this
specific place for the verification to succeed. Without this
assertion, verification fails but assists you by providing a key piece
of information: invariant `Preserved(a,0,a.Length)`

could not be
proved to be maintained by the inner loop.

Since it is an invariant, it should hold at any point within the loop,
so we can assert it in between every statement to see which one makes
the verification fail. You will find that it is statement
`var cmp := Ltm(a[j], minValue);`

that prevents the verification from verifying
the invariant. Three possibilities:

- The code is actually incorrect
- The invariant isn't actually one and our proof is wrong
- The verification needs some hint

To some extent, it makes sense that the verification might need a
hint. When we call method `Ltm`

, how do we know that it is not going
to change array `a`

? Of course it is in a sense obvious since it is
clearly not mentioning `a`

but obvious doesn't cut it in formal
verification. Now, we did specify that the method modifies the field
but nothing else, so it should be the case that `a`

is left
unchanged. This is where it makes sense to assert
`a[..] == old@L(a[..]);`

to double-check that the verification agrees. In this
case, not only does it agree, but it also turns out to be the hint the
verification needs to succeed. You may be interesting in seeing
another example in
action.

One may feel like the verification should not have required such a hint but ATPs are fundamentally bound to miss obvious facts every now and then. It is not a bug of the verifier, merely an unfortunate and perhaps unavoidable case of incompleteness of its proving capability.

We can finish our implementation by defining a class to extend these traits.

```
class Sort<T(==)> extends SelectionSort<T> {
const CMP: (T,T) -> bool
constructor(cmp: (T,T) -> bool)
ensures CMP == cmp
ensures comparisonCount == 0
{
CMP := cmp;
comparisonCount := 0;
}
function Lt(x: T, y: T): bool {
CMP(x,y)
}
}
```

## Verifying Backward Compatibility of an Optimization

We have seen three kinds of verification so far:

- Verifying the absence of runtime errors
- Verifying a functional specification
- Verifying runtime complexity

There is another very important case we need to mention briefly:
verification of optimizations. Throughout this introduction, our
implementation of selection sort uses an inner loop that identifies
`minValue`

and `minPos`

and eventually performs a swap. We could also
have chosen to perform the swap whenever we identify a new
`minValue`

. This would save two local variables and the condition
statement following the loop. This may or may not actually be an
optimization, but for the sake of this discussion, let us assume that
it is.

If we have the luxury of a functional specification, we may implement this optimization and make sure that the functional specification continues to hold. But we do not always have such a functional specification. First, there may not be a crisp and clear functional specification beyond ensuring the absence of runtime errors. Even in that case, the functional specification may not be complete (case in point, we did not formally verify that our implementation of selection sort is stable).

It is, however, very common for existing code to have been tested and
used enough that *it* serves as the specification, and the
verification goal is therefore to show that the optimized code behaves
like the unoptimized but trusted one. In such a case, ghost variables
are very handy, as they allow making the old trusted code ghost and
serve as the specification.

```
method SelectionSort(a: array<int>)
modifies a
{
for i := 0 to a.Length
{
ghost var minValue := a[i];
for j := i + 1 to a.Length
invariant a[i] == minValue
{
if a[j] < minValue {
minValue := a[j];
}
if a[j] < a[i] {
a[i], a[j] := a[j], a[i];
}
}
assert a[i] == minValue;
}
}
```

Here, `minValue`

has become a ghost variable and the invariant
maintains that throughout the execution of the inner loop, the value
`a[i]`

is the smallest we have encountered so far. Aside from proving
the absence of runtime errors, this kind of verification where one
improves code while proving backward compatibility with respect to the
ghost version of the old code allows verification effort to deliver a
high-degree of confidence for a small specification and verification
effort.

## Conclusion

Hopefully, this example gives a concrete idea of what program specification and verification feels like, and shows that it is not limited to toy academic languages. Proving the functional correctness of selection sort shows that even for such a non-trivial properties, automation is good enough to keep the verification effort low. Moreover, the complexity example shows that while more abstract and mathematical properties may require more work, verification remains doable. Because Dafny is not just a great programming language but also a great proof assistant, one can learn systematic methodologies to verify code.