Three Dollar Quill

Things are going... very well with Dafny. I've got a general form that I'm doing, and I don't know whether it's idiomatic, but it seems to work for my purposes.

Basically, I define the recurrence relation I'm trying to solve stuff for as a function, define another function for the closed form if applicable, define a lemma that just handles the recursive case because the base case has been trivial every time so far, and write a method that is required to satisfy the recurrence relation, but is implemented by invoking the closed form, and passing the result to the lemma.

That was all pretty abstract. Let's try to make things a bit more concrete.

..smiley:

Heyo!

... Suppose we want to verify a closed form equation for the number of regions we can divide the plane into, given n straight lines. To start with, we need the recurrence relation, and the method that implements equivalent semantics:

function regions_from_lines(n: int): int
  requires 0 <= n
{
  if n == 0 then 1
  else regions_from_lines(n - 1) + n
}

method RegionsFromLines(n: int) returns (regions: int)
  requires 0 <= n
  ensures regions == regions_from_lines(n)
{
}

I don't know, maybe? Probably?

Anyway, I'm conceptualizing this as the general template that I'm going to try to fit stuff into. Obviously, it doesn't currently verify, because I didn't write the code. Let's go through all of the steps, including the intermediate bits.

function regions_from_lines(n: nat): nat
{
  if n == 0 then 1
  else regions_from_lines(n - 1) + n
}

method RegionsFromLines(n: nat) returns (regions: nat)
  ensures regions == regions_from_lines(n)
{
  regions := 1 + n * (n + 1) / 2;
}

Technically, I could do a return statement here, but I'm going to stick the lemma afterwards, so this is easier to write later. Now, this, of course, does not verify, because Dafny isn't going to proactively try to validate the Mystery Formulas I give it. The next step, then, is to create an inductive lemma that validates the relationship between the recurrence relation and the Mystery Formula. Because this lemma will involve the Mystery Formula in its requires line, I'll define it as a function so I don't have to get it exactly in sync with itself:

function regions_from_lines(n: nat): nat
{
  if n == 0 then 1
  else regions_from_lines(n - 1) + n
}

function closed_form(n: int): int
{
  1 + n * (n + 1) / 2
}

lemma RegionInduction(lines: nat, regions: int)
  requires regions == closed_form(lines)
  ensures regions == regions_from_lines(lines)
{
}

method RegionsFromLines(n: nat) returns (regions: nat)
  ensures regions == regions_from_lines(n)
{
  regions := closed_form(n);
  RegionInduction(n, regions);
}

This moves the verification failures from the method into the lemma. At this point, I should probably emphasize that I haven't gotten any help or guidance from another person on this currently, so I could be putting together something that is excessively verbose, or inefficient, or just somehow hard to read. Regardless, the next step is to fill in the lemma with enough information for Dafny to carry out an inductive argument.

function regions_from_lines(n: nat): nat
{
  if n == 0 then 1
  else regions_from_lines(n - 1) + n
}

function closed_form(n: int): int
{
  1 + n * (n + 1) / 2
}

lemma RegionInduction(lines: nat, regions: int)
  requires regions == closed_form(lines)
  ensures regions == regions_from_lines(lines)
{
  if 1 <= lines {
    RegionInduction(lines - 1, regions - lines);
  }
}

method RegionsFromLines(n: nat) returns (regions: nat)
  ensures regions == regions_from_lines(n)
{
  regions := closed_form(n);
  RegionInduction(n, regions);
}

And, assuming I copied everything over correctly, we're done.

It turns out that, once you've figured out which water to lead Dafny to, it will drink.

Okay, let's see what happens if I sabotage the closed form. Comment out the denominator, and... Hm. I'll have to see later if there's some way to make Dafny go into more detail, but it does catch the issue.

Anyway, with all that said and done, I've got some cleanup to do to the code(?) I've written, and then it's time to tackle the next section of the textbook. Very carefully and deliberately.

For now, better wind down and rest.

Good night.