Skip to content
Print

Algorithm Proof Inference in Scala

1
Apr
2008

Anyone who’s written any sort of program or framework knows first-hand the traumas of testing.  The story always goes something like this.  First, you spend six months writing two hundred thousand lines of code which elegantly expresses your intent.  Next, you spend six years writing two hundred million lines of code which tests that your program actually does what you think it does.  Of course, even then you’re not entirely sure you’ve caught everything, so you throw in a few more years writing code which tests your tests.  Needless to say, this is a vicious cycle which usually ends badly for all involved (especially the folks in marketing who promised the client that you would have the app done in six hours).  The solution to this “test overload cycle” is remarkably simple and well-known, but certain problems have constrained its penetration into the enterprise world (that is, until now).  The solution is program proving.

A More Civilized Age

Program proofs are basically a (usually large) set of mathematical expressions which rigorously prove that all accepted program outcomes are correct.  A program prover takes these expressions and performs the appropriate static analysis on your code, spitting out either a “yes” or a “no”.  It’s far more effective than boring old unit testing since you can be absolutely certain that all the bugs have been caught.  More than that, it doesn’t require you to write reams of test code.  All that is required is the series of expressions defining program intent:

\Gamma_m \to \{\Gamma_0 = \textit{input} | m \sub \Gamma_0\} \cup \Sigma^\star

\epsilon = e^{\epsilon \pm \delta}

f \colon \{ x \in [\epsilon, \infty) | x \to \Gamma_x \}

\rho_\delta = f(\Gamma_\delta \bullet \Gamma_\alpha) \Rightarrow \alpha \in \Sigma^\star

\mbox{prove}(\Omega) = \Omega \in \Gamma_\Beta \Rightarrow (\Omega \times \epsilon) \vee \rho_\omega

There, isn’t that elegant?  Much better than some nasty JUnit test suite.  In a happier world, all tests would be replaced by this simple, easy-to-read representation of intent.  Unfortunately, program provers have yet to overcome the one significant stumbling block that has barred them from general adoption: the limitations of the ASCII character set.

Sadly, the designers of ASCII never anticipated the widespread need to express a Greek delta, or to properly render an implication.  Of course, we could always fall back on Unicode, but support for that character set is somewhat lacking, even in modern programming languages.  And so program provers languish in the outer darkness, unable to see the wide-scale adoption they so richly deserve.

An Elegant Weapon

Fortunately, Scala can be the salvation for the program prover.  It’s hybrid functional / object-oriented nature lends itself beautifully to the expression of highly mathematical concepts of intense precision.  Theoreticians have long suspected this, but the research simply has not been there to back it up.  After all, most PhDs write all their proofs on a blackboard, making use of a character set extension to ASCII.  Fortunately for the world, that is no longer an issue.

The answer is to to turn the problem on its ear (as it were) and eschew mathematical expressions altogether.  Instead of the developer expressing intent in terms of epsilon, delta and gamma-transitions, a simple framework in Scala will infer intent just based on the input code.  All of the rules will be built dynamically using an internal DSL, without any need to mess about in low-level character encodings.  Scala is the perfect language for this effort.  Not only does its flexible syntax allow for powerful expressiveness, but it even supports UTF-8 string literals!  (allowing us to fall back on plan B when necessary)

Note that while Ruby is used in the following sample, the proof inference is actually language agnostic.  This is because the parsed ASTs for any language are virtually identical (which is what allows so many languages to run on the JVM).

class MyTestClass
  def multiply(a, b)
    a * b
  end
end
 
obj = MyTestClass.new
puts obj.multiply(5, 6)

Such a simple example, but so many possible bugs.  For example, we could easily misspell the multiply method name, leading to a runtime error.  Also, we could add instead of multiply in the method definition.  There are truly hundreds of ways this can go wrong.  That’s where the program prover steps in.

We define a simple Scala driver which reads the input from stdin and drives the proof inference framework.  The framework then returns output which we print to stdout.

object Driver extends Application {
  val ast = Parser.parseAST(System.in)
 
  val infer = new ProofInference(InferenceStyle.AGRESSIVE)
  val prover = new ProgramProver(infer.createInference(ast))
 
  val output = prover.prove(ast)
  println(output)
}

It’s as simple as that!  When we run this driver against our sample application, we get the following result:

image

Notice how the output is automatically formatted for easy reading?  This feature dramatically improves developer productivity by reducing the time devoted to understanding proof output.  One of the many criticisms leveled against program provers is that their output is too hard to read.  Not anymore!

Of course, anyone can write a program which outputs fancy ASCII art, the real trick is making the output actually mean something.  If there’s a bug in our program, we want the prover to find it and notify us.  To see how this works, let’s write a new Ruby sample with a minor bug:

class Person < AR::Base
end
 
me = Person.find(1)
me.ssn = '123-45-6789'
me.save

It’s an extremely subtle flaw.  The problem here is that the ssn field does not exist in the database.  This Ruby snippet will parse correctly and the Ruby interpreter will blithely execute it until the critical point in code, when the entire runtime will crash.  This is exactly the sort of bug that Ruby on Rails adopters have had to deal with constantly.

No IDE in the world will be able to check this code for you, but fortunately our prover can.  We feed the test program into stdin and watch the prover do its thing:

image

Once again, clear and to the point.  Notice how the output is entirely uncluttered by useless debug traces or line numbers.  The only thing we need to know is that something is wrong, and the prover can tell us that.

Conclusion

I can speak from experience when I say that this simple tool can work wonders on any project.  Catching bugs early in the development cycle is the Holy Grail of software engineering.  By learning there’s a problem early on, effort can be devoted to finding the bug and correcting it.  I strongly recommend that you take the time to check out this valuable aid.  By integrating this framework into your development process, you may save thousands of hours in QA and testing.

Comments

  1. That’s nice. How about integrating it to core Scala libraries?

    jau Tuesday, April 1, 2008 at 1:21 am
  2. Not to nitpick, but there is another bug in the Ruby example code: the String with the SSN is formatted wrong. The middle section should only have 2 numbers, not 3.

    Aaron Davis Tuesday, April 1, 2008 at 5:58 am
  3. @Aaron

    Ah, very true! Seems I should update the proof inference engine to check for typos. :-)

    Daniel Spiewak Tuesday, April 1, 2008 at 7:48 am
  4. One assumes this relies on RFC 2549? In which case how to do handle the non-availability of the highest QoS?

    Of course, management would call a halt to any such excess even if it were available.

    Richard Tuesday, April 1, 2008 at 8:04 am
  5. Fortunately, this proof inference engine is self-contained. While there are plans to allow distributed deployments of the engine (to improve performance on more resource-intensive proofs), that is currently not implemented. Once it is though, you can be sure that RFC 2549 will feature prominently in the dispatch protocol, ensuring maximum throughput and optimal performance.

    Daniel Spiewak Tuesday, April 1, 2008 at 10:15 am
  6. Do you sell an educational license for this? I would like to use it to verify correctness of my ML application suite that I developed for my senior thesis.

    Jacob Tabak Tuesday, April 1, 2008 at 10:32 am
  7. No need for an educational license! In an attempt to spur (much needed) innovation in this field, I’m releasing all the code as open source. Feel free to download from the link and give it a try!

    Daniel Spiewak Tuesday, April 1, 2008 at 10:34 am
  8. Tsk! Tsk! You forgot to import the poisson distribution.

    There:
    import math.statistical.distribution.poisson._

    Jeff Heon Tuesday, April 1, 2008 at 11:08 am
  9. The sad thing is for half the article I was wondering what the heck you’re talking about. Then I remembered about the calendar and it all made sense, if you can call it that… :)

    German B. Tuesday, April 1, 2008 at 7:16 pm
  10. This is _evil_

    I came here through a google alert on April 7th, and read seriously till about half-way through.

    HRJ Sunday, April 6, 2008 at 9:57 pm
  11. lol Glad it was a worthy prank! The whole ASCII art for output was probably what gave it away. :-)

    Daniel Spiewak Sunday, April 6, 2008 at 10:02 pm
  12. I seriously thought you were crazy until I saw the comments and checked the date.

    I just discovered your blog and am really enjoying it.

    Justin Camerer Saturday, May 3, 2008 at 8:46 pm
  13. I recently discovered your blog and was reading through all entries about Scala until I stumbled upon this one. It was March, 15th. So, I had a hard time realizing what was going on. I actually figured it out when I saw the second screenshot. Then I scrolled up and saw the date! :)

    I sent this entry to my colleagues yesterday. It was fun to see how it works even after two years :D

    Michel Krämer Friday, April 2, 2010 at 5:15 am

Post a Comment

Comments are automatically formatted. Markup are either stripped or will cause large blocks of text to be eaten, depending on the phase of the moon. Code snippets should be wrapped in <pre>...</pre> tags. Indentation within pre tags will be preserved, and most instances of "<" and ">" will work without a problem.

Please note that first-time commenters are moderated, so don't panic if your comment doesn't appear immediately.

*
*