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:

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:

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.

Download proof-inference.zip

Filed in Scala | Comments (12)

Should ORMs Insulate Developers from SQL?

25
Feb
2008

This is a question which is fundamental to any ORM design. And really from a philosophical standpoint, how should ORMs deal with SQL? Isn’t the whole point of the ORM to sit between the developer and the database as an all-encompassing, object oriented layer?

A long time ago in an office far, far away, a very smart cookie named Gavin King got to work on what would become the seminal reference implementation for object relational mapping frameworks the world over (or so Java developers would like to think). This project was to be bundled with JBoss, possibly the most popular enterprise application server, and would support dozens of databases out of the box. It was to offer heady benefits such as totally object-oriented database access, transparent multi-tier caching and a flexible transaction model. At its core though, Hibernate was design to resolve a single problem: application developers hate SQL.

No really, it’s true! Bread-and-butter application developers really dislike accessing data with SQL. This has led to endless conflict (and bad jokes) between application developers and database administrators. Often times the developer team would write a set of boilerplate lines in Java and then copy/paste these arbitrarily throughout their code, swapping in the relevant query as supplied by the DBA. For obvious reasons, this would become very hard to maintain and just intensified the bad blood between developer and database.

If you think about it though, it’s a bit odd that this intense dislike would mutate from just hating the insanity of JDBC to hating JDBC, SQL and RDBMS in general. SQL is a very nice, almost mathematical language which allows phenomenally powerful queries to be expressed simply and elegantly. It abstracts developers from the headache of database-specific hashing APIs and algorithms which are almost filesystems in complexity. The language was designed to make it as easy as possible to get data out of a relational database. The fact that this effort backfired so utterly is a source of endless confusion to me.

But irregardless, we were talking about ORMs. When it was first introduced, Hibernate held out the promise that developers would never again have to wade knee deep through a sea of half-set SQL. Instead, developers would pass around POJOs (Plain Old Java Object(s)), modifying their values like any other Java bean and then handing these objects off to the data mapper, which would handle the details of persistence. Furthermore, Hibernate promised that developers would never again have to worry about which databases support which non-standard SQL extensions. Since developers would never have to work with SQL, anything database-specific could be handled within the persistence manager deep in the bowels of Hibernate itself.

This all seems lovely and wonderful, but there’s a catch: it doesn’t work so well in practice. Now before you stone me, I’m not talking about Hibernate specifically now, but ORMs in general. It turns out to be completely impossible to interact with a relational database solely through an object-oriented filter. This is easily seen with a simple example:

SELECT * FROM people WHERE age > 21 GROUP BY lastName

How in the world are you going to represent that in an object model? Sure, maybe you can provide a little abstraction for the query details, but it starts to get complex if you try to handle things like grouping non-declaratively. The developers working on Hibernate quickly realized this problem and came up with an innovative solution: write their own query language! After all, SQL is too confusing, so why not invent an entirely new query language with the “feel” of SQL (to keep the DBAs happy) but without all of the database-specific wrinkles?

This query language is now called “HQL”, and as the name implies, it’s really SQL, but not quite. Here’s how the aforementioned example would look in HQL (disclaimer: I’m not a Hibernate expert, so I may have gotten the syntax wrong):

FROM Person WHERE :age > 21 GROUP BY :lastName

Remarkably similar, that. Executing this query in a Hibernate persistence manager yields an ordered list of Person entities pre-populated with data from the query. It seems to make a lot of sense, but there are a number of problems with this approach. First, it requires Hibernate to literally have its own compiler to translate HQL queries into database-specific SQL. Second, it hasn’t really solved the core problem that many developers have with SQL: it’s a declarative query language. As you can see, HQL is really just SQL in disguise, so it really doesn’t eliminate SQL from your database access, just dresses it in a funny hat.

Other ORMs have appeared over the years, taking alternative approaches to the problem of object-relational mapping, but none of them quite eliminating the query language. Even DSL-based ORMs like ActiveRecord fail to remove SQL entirely:

class Person < AR::Base; end
 
Person.find(:all, :conditions => 'age > 21', :group => 'lastName')

It’s sort of SQL-free, but you can still see bits and pieces of a query language around the edges. In fact, what ActiveRecord is actually doing here is building a proper SQL query around the SQL fragments which are passed as parameters. It’s a system which is ripe for SQL injection, but surprisingly leads to very few problems in real-world applications. This is the approach which is also taken by ActiveObjects for its database query API.

So ORMs in and of themselves seem to have failed to entirely eliminate SQL from the picture, but what about other frameworks? There are a few quite recent efforts which seem to have nearly succeeded in eliminating the direct use of SQL completely from application code. Ambition is perhaps the best (and most clever) example of this, though others like scala-rel are catching up fast. Ambition is designed from the ground up to interact naturally with ActiveRecord, so the two combined perhaps represent the first “true” ORM: one which does not require the developer at any point to deal with any SQL whatsoever.

But was it really worthwhile? As clever as things like Ambition are, is it really that much easier than just writing queries in SQL? As Nathan Hamblen so eloquently said (when referring to a totally different topic):

…is the end of the ORM rainbow. You get there, throw yourself a party and realize that important things are broken.

A quote taken out of context perhaps, but I think it applies to the “cult of SQL genocide” with as much validity. In the end, by denying yourself access to the powerful and well-understood mechanism that is SQL, you’re just crippling your own application and forcing yourself to write more code instead of less.

So what’s the “right” approach? Is there a happy medium between ActiveRecord+Ambition and full-blown SQL on Rails? I think so, and that is the approach I have been trying to implement with ActiveObjects. As I’m sure you know, ActiveObjects takes a lot of its inspiration from ActiveRecord, so the syntax for querying the database is very similar:

EntityManager em = ...
em.find(Person.class, Query.select().where("age > 21").group("lastName"));
 
// ...or
em.find(Person.class, "name > 21");   // no grouping

You still have the full power of SQL available to you. You can still write complex, nested boolean conditionals and funky subqueries, but there’s no longer any need to be burdened with the whole of SQL’s verbosity. As with vanilla ActiveRecord, this code intends to be a bit of a hand-holder, shielding innocent application developers from the fierce world of RDBMS.

Is this the right way to go? I’m honestly not sure. I’ve met a lot of developers that would give their left eye to never have to look at another SQL statement again (for developers already missing a right eye, this isn’t much of a stretch). On the other hand, there are purists like myself who revel in the freedom afforded by a powerful, declarative language. It’s hard to say which path is better, but at the end of the day, it’s really the question itself that matters. Giving application developers the choice to select whichever approach they feel is most appropriate, that is the solution.

Filed in Database | Comments (41)

Adding Type Checking to Ruby

6
Feb
2008

What’s the first thing you think of when you consider the Ruby Language? Dynamic types, right? Ruby is famous (infamous?) for its extremely flexible type system, and as a so-called “scripting language”, the core of this mechanism is a lack of type checking. This feature allows for some very concise expressions and a great deal of flexibility, but sometimes makes your code quite a bit harder to understand. More importantly, it weakens the assurances that a certain method will actually work when passed a given value.

Several different solutions have been proposed to workaround this limitation. The canonical technique involves intensifying tests and increasing test coverage. Ruby has some excellent unit test frameworks (such as RSpec) which serve to ease the pain associated with this approach, but no matter how you slice it, tests are a pain. Having to rely on tests to take the place of type checking in the code assurance process can be extremely frustrating.

Another, less common technique is to simply perform dynamic type checks within the method itself. Like so:

def create_name(fname, lname)
  raise "fname must be a String" unless fname.kind_of? String
  raise "lname must be a String" unless lname.kind_of? String
 
  fname + " " + lname
end

This code explicitly checking the dynamic kind of the parameter values to ensure that they are of type or subtype of String. The issues with this sample should be relatively obvious.

Primarily, it’s ugly! This sort of repetitious, boiler-plate conditional checking is exactly the sort of thing Ruby tries to avoid. What’s more is the added bulk of all of these repetitive checks (assuming you perform one check per-parameter per-method) because far more unwieldy than just improving the rspec test coverage.

While manually type checking may be a bad solution syntactically, it’s on the right track conceptually. What we really want is some sort of assertion that the parameters are of a certain type, but that won’t overly bloat our existing code. We need some sort of framework that will “weave in” (think AOP) its type assertions without getting in the way our our algorithms.

Well it turns out that someone’s already done this. Eivind Eklund kindly pointed me to his type checking framework in a comment on a previous post. The basic idea is to perform the type checking assertions, but to factor the work out into an API encapsulated by an intuitive DSL. So rather than performing all those nasty unless statements as above, we could simply do something like this:

typesig String, String
def create_name(fname, lname)
  fname + " " + lname
end

It’s really as simple as that. Passing the type values to the typesig method just prior to a method declaration give the cue to the Types framework to perform some extra work on each call that method. Now we have the runtime assurances that the following code will not work (with a very intuitive error message):

create_name("Daniel", 123)

Will produce the folling output:

ArgumentError: Arg 1 is of invalid type (expected String, got Fixnum)

But the fun doesn’t stop there. Ruby encourages the “duck typing” pattern, where algorithm developers concern themselves not with what the value is but rather what it does. This means that the type checking really should be done based on what methods are available, not just the raw type. It turns out that the Types framework supports this as well:

class Company
  def name
    "Blue Danube"
  end
end
 
class Person
  def name
    "Daniel Spiewak"
  end
end
 
typesig String, Type::Respond(:name)
def output(msg, value)
  puts msg + " " + value.name
end
 
c = Company.new
p = Person.new
 
output("The company name is: ", c)
output("The person is: ", p)
 
output("The programmer is: ", "a genius")    # error

Types can check not only the kind of the object but also to what methods it responds. This is crucial to enabling its adoption into modern Ruby code bases, many of which rely heavily on this “duck typing” technique.

You can think of the Types framework just like another layer in your testing architecture. Obviously it’s not performing any sort of static type checking (since Ruby has no compile phase). All it’s doing is providing that extra certainty that you’re never passing something weird from somewhere in your code, something that would break your algorithm.

So what’s the catch? Well, obviously you need to have the Types framework installed. It’s not as easy as just typing gem install types either, since the framework actually predates Ruby Gems. You’ll have to download the framework and then copy around the types.rb file yourself. But this is just deployment semantics. The more interesting issue are the limitations of the code itself.

As far as I can tell, the only restriction on the framework is that it must be used within a proper class, not in the root scope. This means that all of my examples above would have to be enclosed in a class, rather than just copy-pasted into a .rb file and run in place. But other than this one limitation, the framework is incredibly flexible. I really haven’t shown you the seriously interesting stuff in terms of the API (there are more examples at the top of the types.rb file). In many ways, Types is actually more powerful than any static type checking mechanism could be (yes, I’m even including Scala in that evaluation).

I haven’t had a chance to use Types on any serious project myself, but I can see tremendous potential, particularly for companies with large-scale Ruby/Rails deployments or even smaller projects looking for just a bit tighter code assurance. As far as I’m concerned, there shouldn’t be a non-trivial Ruby project attempted without this lovely library, Rails or no Rails.

Filed in Ruby | Comments (20)

The End of the Ruby Fad?

23
Jan
2008

Well, it’s a new year; and apparently no sooner are the resolutions forgotten and the hangovers behind us then the internet en mass decides that we need a new language. Ruby was indisputably the hip language of 2006 and 2007. However, in an opinion shift so sudden as to make one’s head spin, the blogosphere seems to have rebelled against the hype and gone in search of a new mistress.

It seems more and more these days like people just don’t want to hear about Ruby. Ruby posts to link sites like DZone or Reddit get voted down before they have a chance to see the light of day. Pointless flames litter the blogs, declaiming Ruby and alternatively crowning Groovy, Scala, Java or even XML in its place. The sad thing is that no one seems to have found the middle ground yet.

Personally, I’m with Reganwald on this one. I started coding with Ruby back in 2002 (or was it 2001? I can’t remember now). It was actually at the recommendation of some random guy on a forum who said that Ruby was a nice and clean language with a lot of potential. I was getting pretty tired of Java at that point, so I figured I’d give it a try. Since then, Ruby has become part of my essential scripting toolset, finding applications everywhere from complex utility scripts, build systems and even hacky dynamic web pages for my server monitoring tools. Based on the strength of the language, I’ve tried Rails a few times without success. I mean, honestly which is easier to remember?

link_to :page => ""

…or,

<a href=""></a>

The middle ground is really where Ruby belongs, where it flourishes. It’s hardly a general-purpose language, so it could never replace Java and company. With that said, it’s far easier to write an incremental backup script in Ruby than in Java. And while Ruby may not be suitable for an enterprise level, high-traffic web application, it’s certainly up for some tasks within that application. It’s also perfect for managing scripting and rapid prototyping against that application infrastructure. Unfortunately the community as a whole seems either blind to its benefits or blinded by its hype.

It seems like it’s constantly an “all or nothing” attitude with these new languages. Developers these days fall into two camps: those who have heard the hype and rejected what it stands for, and developers who are totally carried away by the emotion of the fad. To the former camp, developers who straddle the middle ground are traitors to the cause and just as bad as the hyper fanatics. But to the fanatics, the moderates are fence riders who refuse to fully embrace their destiny. In short, it’s the moderates who catch flack from both camps. Yet ironically, it’s the moderates who seem to be doing useful things with the technology, rather than wasting energy on five minute blog demos and eloquent rebuttals.

So on one hand, I’m glad to see the hype die. It was frustrating having to deal with yet-another bigoted “Rails Rocks, Java Suxz” rant every time I opened my RSS. On the flip side, the backlash is equally annoying. It certainly would be nice to have some balance around here, instead of breaking out the petroleum sulfite every time someone accidentally expresses an opinion. Perhaps now that the bubble has burst, we’ll finally get to see the popularity of Ruby in its proper place.

Filed in Ruby | Comments (36)

ActiveObjects 0.7 Released

22
Dec
2007

Just in time for the Christmas holidays, I give you ActiveObjects version 0.7! This release sports a whole slew of minor performance tweaks and bugfixes, providing better reliability. Also, we’ve greatly increased the number and scope of the unit tests running against the core. This gives us more confidence that the code is indeed as stable as we hope.

Actually, the big ticket item for 0.7 is the introduction of polymorphic relations. This feature is fully tested and stable, so I don’t anticipate it introducing any issues in the coming days as we narrow our focus to 1.0. However, no feature is so well tested as to be certainly bug free under all circumstances. I look forward to fixing any problems you may encounter with the library!

A few minor feature additions:

Support for persisting enum values
One-to-one relations
EntityManager#flush(…) now also flushes the relations cache

Looking toward the road ahead, things are really starting to settle down a bit. The main feature I’m looking to implement for 0.8 is extensible value caching, which should allow you to determine how and where the cached field values are stored. The main use-case behind this is support for memcached, which has been requested a few times and has actually been on the agenda since 0.3. With memcached driving the value cache, ActiveObjects should be almost perfectly scalable.

To that end, it’s also worth mentioning that I did some profiling (using the NetBeans Profiler) using a Wicket-based web application I’m developing on the side. I’m happy to report that the overhead imposed by ActiveObjects is extremely minimal. In each test, the bottleneck was in the PreparedStatement#execute method (in JDBC). Since ActiveObjects generates very streamlined and natural queries, it seems that this is really the minimal execution time possible for such database access. Extrapolating further from this data, and given that the JDBC exec time was avg 40ms, while the execution time in the ActiveObjects API was on the order of 1ms-5ms, we can safely say that ActiveObjects is less than 10% slower than using JDBC directly (compare that to the 50% overhead claimed by ActiveRecord). This “estimate” doesn’t even take into account the many performance advantages offered by ORMs over hand-coded database access (such as relations caching, optimal query construction, etc).

Anyway, enough shameless boasting. As Hibernate has often pointed out, ORM benchmarks are usually worse than useless. The only benchmark which really matters is how well the ORM performs in your application. Try it out, see what you think.

Filed in Java | Comments (6)