[PL] Dafny programming language

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³ checker of Dafny, you can modify the assignment to r : x= and see what error will show in VSCode⁴. This is a nice try for understanding what's post-condition.

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.

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.

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.

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.