# Dafny programming language

Dafny1 is a programming language with pre/post-condition, so we can statically verify our mutable algorithm follows required properties, you can find how to install it at here2

## 1. First example

```method Double(x: int) returns (r: int)
ensures r == x * 2
{
r := x + x;
}
```

This example says the return variable `r` must be `x * 2`, this post-condition will be checked by hoare logic3 checker of Dafny, you can modify the assignment to `r :` x= and see what error will show in VSCode4. This is a nice try for understanding what's post-condition.

## 2. Write it out

An important thing is, if a condition didn't get write down, it will not be used even though we might be able to infer it. Therefore, the below program will not pass the verification

```method AddOne(x: int) returns (r: int)
{
r := x + 1;
}

method Test() {
assert r > 0;
}
```

It should complain that assertion didn't hold, we should add post-condition `ensures r > x` for `AddOne` to hint Dafny which property we want here.

## 3. Termination is required

Consider a program like this:

```method Double(x: int) returns (r: int)
ensures r == x * 2
{
var s := Double(x - 1);
r := s + 2;
}
```

Dafny will complain decreases expression must be bounded below by 0, that's a rule to avoid program such that will never stop! It's the core problem of this definition. Although every `Double` says it returns the double of input, if we believe that, then `Double(x - 1)` should be `2x - 2`. Then `s + 2` should be `2x` exactly, however, this program will never return. Therefore, the condition is broken even though no one violate it.

## 4. Mixing proof style

The final thing is the proof style in Dafny is quite free, we can pick term based or assertion in a same `lemma`:

```lemma AppendDecomposition<T>(a : List<T>, b : List<T>, c : List<T>, d : List<T>)
requires Length(a) == Length(c)
requires Append(a, b) == Append(c, d)
ensures a == c && b == d
{
match a
case Nil => {
match c
case Nil => assert b == d;
case Cons(_, c) => assert Length(a) != Length(c);
}
case Cons(_, a) => {
match c
case Nil => assert Length(a) != Length(c);
case Cons(_, c) => AppendDecomposition(a,b,c,d);
}
}
```

In this example, if some cases lead absurd, I put an assertion shows it violates the pre-condition, but I didn't say how to use it, Dafny has powerful checker that understand that means such case is impossible! On the other hand, for possible cases, I can use assertion to show the post-condition is hold, or reuse the `lemma` inductively! Since we already know Dafny also check termination, and hence, we can see the recursion would be fine.

## 5. Conclusion

Dafny is a very nice static verification tool, I hope this brings more introduction for the language, and helps you well in your real work.

Date: 2023-05-17 Wed 11:27
Author: Lîm Tsú-thuàn