# Dafny programming language

Dafny^{1} 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 here^{2}

## 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 logic^{3} checker of Dafny, you can modify the assignment to `r :`

x= and see what error will show in VSCode^{4}. 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() { var r := AddOne(0); 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.