[math-fun] Fun with program verification

19 Mar 2012

      More light-heartedly, for those who find this sort of thing fun, a while
back I made a little puzzle (inspired by Bill Gosper) to illustrate the
inherently deep difficulty of program verification:

========
A predicate on positive integers:

    boolean isToad(int n)
    {
        return ( n==2 || n==frog(4,floor((n-1)/2),1,0)-1) );
    }

is defined with the aid of the following helper method:

    int frog(int q, int r, int s, int t) {
        if (r<t) {
            return 0;
        } else if (r==t) {
            return 1;
        } else if (q==0) {
            return 0;
        } else {
            return ( frog(q,r,s+1,s+t) + frog(q-1,r-t,1,0) );
        }
    }

Questions:
  1.  Which integers are toads?
  2.  Can you describe what the frog method does?
  3.  Can you explain why this code works?
========

Without spoiling it:

  1.  Just run the program on successive n and it will quickly be obvious
what "toads" are.  Take this as the "requirements" or "specification" to be
validated against.

  2.  Documenting what the frog code is computing is, in theory, only a
little harder.  But I've found programmers and their ilk often struggle
mightily with this--until they abandon certain preconceptions about how it
"ought" to be working.

  3.  Many funsters could answer this, but most software professionals
boggle.  I look forward to meeting the AI that can do it!

"Enjoy"!

Marc LeBrun

Mike Stay

tags

participants (2)