Google open sources "Contracts for Java"

This is very similar to JML!<p>I co-wrote a paper on the subject a couple years ago during my undergraduate, which I humbly share with you :)<p>A Case Study in JML-Assisted Software Development <a href="http://portal.acm.org/citation.cfm?id=1556581&#38;preflayout=flat" rel="nofollow">http://portal.acm.org/citation.cfm?id=1556581&#38;preflayout...</a><p>Download: <a href="http://cic.puj.edu.co/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:cbg_09.pdf" rel="nofollow">http://cic.puj.edu.co/wiki/lib/exe/fetch.php?media=grupos:av...</a>

Very cool stuff. I wonder if there is any way to integrate something like KeYmeara (<a href="http://symbolaris.com/info/KeYmaera.html" rel="nofollow">http://symbolaris.com/info/KeYmaera.html</a>) for a way to prove correctness of Java systems (or components of Java systems).

Not having any experience with contracts like this, I wonder how this relates to testing. Is this thought to be an addition or an alternative to usual xUnit style and integration tests. Or are these concepts not even related and I am getting it all wrong?

I have read a bit about Crystal SAF, a static analysis framework for Eclipse from CMU:<p><a href="http://code.google.com/p/crystalsaf/" rel="nofollow">http://code.google.com/p/crystalsaf/</a><p>What appealed to me was that it seemed to have a nice API against which one can write his own analyses. It exposes Java code at a granularity of control flow -- homogenization of for loops, while loops, etc. FindBugs works really well, and I use it on a reasonably large production codebase. However, extending it doesn't seem like much fun as one must express patterns in terms of Java bytecode! I tried using Crystal's built-in analyses on the same codebase upon which I use FindBugs, but it failed with an NPE.<p>Also, Soot from McGill (<a href="http://www.sable.mcgill.ca/soot/" rel="nofollow">http://www.sable.mcgill.ca/soot/</a>) seems worthy of consideration although the code is a bit creaky (it's dates back to at least 98, I think). It includes four different representations of Java code in various states between source code and byte code. Also, there are a lot of papers, theses, etc. which document various parts of the package.

In general, why has static analysis not been more popular? When I first ran FindBugs on a 50 KLOC codebase I inherited, it identified several real, non-trivial bugs which likely hurt many users. Perhaps the average Java developer's skill level is too low to make sense of these tools' results? But, one would think that most teams have at least one "adult" who would love more visibility into a codebase.

Microsoft has a similar project for .NET <a href="http://research.microsoft.com/en-us/projects/contracts/" rel="nofollow">http://research.microsoft.com/en-us/projects/contracts/</a> . Based on a quick look I think Microsoft's project is a bit more mature (already has VS-intergration for example).

Looks interesting, but why isn't there a .jar to download or a maven reference to use this project? Moreover, there is no documentation explaining how to activate/disactivate contracts... Sorry, but it seems like half-ass delivery to me !!!

A good thing to have - better than the "assert" keyword in Java.

In the sorted parameters example contract, would it not be as good to pass an new object whose constructor ensures the sorting?

Great to see, although it's really too bad that they didn't introduce this as part of the language when they developed it.

The next step for this would be to statically verify the annotations are being obeyed.

Hmm, other java contract projects more mature for a few years even and fully in production..<p>Why Google even pushed this out in such an alpha state?