7 ms·

Google open sources "Contracts for Java"

138 points by eneveu 16y ago

jgershen 16y ago
Very cool stuff. I wonder if there is any way to integrate something like KeYmeara (http://symbolaris.com/info/KeYmaera.html http://symbolaris.com/info/KeYmaera.html) for a way to prove correctness of Java systems (or components of Java systems).
- eneveu 16y ago
  I did not know about KeYmeara. Looks great! While I'm not sure if we may count those as "programmation by contract", some Java tools provide (some) static analysis: - Findbugs - IntelliJ IDEA does some nullness analysis : http://www.jetbrains.com/idea/documentation/howto.html http://www.jetbrains.com/idea/documentation/howto.html - JSR 305 (Annotations for Software Defect Detection in Java) attempted to standardize on a set of annotations. We use it in our project, mainly the @Nonnull at the moment... I believe Findbugs considers these annotations. - CodePro Analytix, also recently open sourced by Google, might also do some static analysis: http://code.google.com/javadevtools/codepro/doc/index.html http://code.google.com/javadevtools/codepro/doc/index.html - Eclipse might too (any expert Eclipse user knows?) I think there is still a lot to do in this space. "Contracts for Java" is a step in the right direction :)
  - tikkes 16y ago
    Eclipse does not do static analysis by default I believe. There are some patches however...
    - ShabbyDoo 16y ago
      The out-of-the-box Eclipse distro does include some static analysis stuff, but it's turned off by default. Preferences->Java->Compiler->Errors/Warnings. Under "Potential Programming Problems", you can alert on such things as guaranteed NPEs, etc.
  - ShabbyDoo 16y ago
    For completeness, PMD should be added to the list although I haven't found it as useful as FindBugs: http://pmd.sourceforge.net/ http://pmd.sourceforge.net/
JVerstry 16y ago
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 !!!
- eneveu 16y ago
  It's still quite new, so for now I think you'll have to build it from source. I know it's annoying when a jar is not available in the Maven repository. But it shouldn't be a dealbreaker either. We have a Maven repository proxy for the company, so I deploy my jars there: mvn deploy:deploy-file ... It's better than having each developer manually install the jar in their local repository: mvn install:install-file ... More information: http://maven.apache.org/plugins/maven-deploy-plugin/usage.html http://maven.apache.org/plugins/maven-deploy-plugin/usage.ht... http://maven.apache.org/plugins/maven-install-plugin/examples/specific-local-repo.html http://maven.apache.org/plugins/maven-install-plugin/example...
  - JVerstry 16y ago
    Well, it does not compile !!! There is no documentation about dependencies... This project is far from operational and mature !!! I'd really rather that people did not deliver half-ass projects and loose people's time...
  - rz0 16y ago
    Yeah, sorry but you have to build it from source, for now. There is no point in making a release now as there are a few bugs that need correcting before that. But thanks for the feedback, I've added a README file now with proper dependency information and set up instructions. The build scripts are certainly quite shacky, I must admit; it was originally integrated into Google's internal build system but now that all of that has been stripped out (including the documentation), it looks kinda non-functioning. I could certainly use some help in making that build and run smoothly in the outer Java world, since I'm not a Java programmer originally and my experience setting up Ant, Maven and the like is very very limited. P.S.: It may be Google-branded but we're still just a small team. The other guys are taking care of the within-Google integration part so I should be working on the open source integration except I'm not very knowledgeable in the Java ecosystem, nor have I ever released any open source project with that level of visibility, so please be patient.
ajmurmann 16y ago
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?
- endlessvoid94 16y ago
  It's based on the idea of formal proofs for programs. There is a really good paper about this by dijkstra, but I can't seem to find it now. Basically you defined preconditions and postconditions for each function and it looks like this "contracts" flag will raise an exception if those conditions aren't met. This is probably a better way to test software, but you still need to know how to write the preconditions and postconditions concisely.
- elviejo 16y ago
  This contracts refer to the concept of "Design by Contract." http://en.wikipedia.org/wiki/Design_by_contract http://en.wikipedia.org/wiki/Design_by_contract The poster child of design by contract is the Eiffel Programming language. http://www.eiffel.com/developers/design_by_contract.html http://www.eiffel.com/developers/design_by_contract.html IMO Contracts help you te really reduce the number of unit test you need to write. And the tests that you DO write are more intersting in the BDD kind of way. I highly recommend to study design by contract. Is one of those things that will make you a better developer in any language you use. A good book with examples in Java and Eiffel is this: Design by Contract, by Example http://www.amazon.com/Design-Contract-Example-Richard-Mitchell/dp/0201634600 http://www.amazon.com/Design-Contract-Example-Richard-Mitche...
- skybrian 16y ago
  I haven't used contracts, but I think if you have more assertions in your code then you need fewer assertions in your tests. But you still need to exercise the code with about the same number of tests, or your testing won't find the bugs.
MarkSweep 16y ago
The next step for this would be to statically verify the annotations are being obeyed.
- spicyj 16y ago
  That sounds (close to) impossible. How would you tell if a given piece of code sorts a list properly? There are a million and one sorting algorithms and the static analyzer would have to be really smart to be able to check that reliably.
  - atamyrat 16y ago
    Yes, it is impossible. See: Halting problem.
    - likpok 16y ago
      The thing about program verification is that everyone knows that of course it is in general impossible. However, I am not writing a simulator. Most of the code I write does not actually take advantage of the power of a Turing machine. The fact that the general problem is impossible does not mean that the entire area of study is useless.
      - riffraff 16y ago
        see: dependent typing http://en.wikipedia.org/wiki/Dependent_type http://en.wikipedia.org/wiki/Dependent_type and restricted languages such as Spark http://en.wikipedia.org/wiki/SPARK_(programming_language) http://en.wikipedia.org/wiki/SPARK_(programming_language)
  - deleted 16y ago
    [deleted]
- likpok 16y ago
  I'm pretty sure that Pex [1] does the static analysis on these things. It's C#, but should be close enough for you to get the idea. [1]: You can play with it here: http://www.pexforfun.com/ http://www.pexforfun.com/
shareme 16y ago
Hmm, other java contract projects more mature for a few years even and fully in production.. Why Google even pushed this out in such an alpha state?
- regularfry 16y ago
  Links?
- eneveu 16y ago
  You are not the only one arguing about the project's lack of maturity and the existence of better, more mature alternatives (which ones?). I can understand this sentiment, and I'd love to be able to add a Maven dependency on this project and start using it on production code tomorrow (well, monday actually). But I am also glad Google followed the "ship early, ship often" mantra . Better alternatives may or may not exist, but I'm pretty sure I had never heard of them before, and never really cared for "contract programming" until now. I knew about JSR 305 and used the @Nonnull annotation when it made sense, but that's about it (I guess doing this already puts me ahead of 80% of Java programmers in this regard...). Some might say that it's sad people waited for a Google-branded project to be interested in this subject. I choose to view it as an opportunity for the field as a whole. The interesting discussions it sparked (here and on other websites) are worth it by themselves. Some developers might even compare options and start using one of the "better alternatives" you hint about. The project may be young, but it seems to generate a lot of interest, and I'm sure many people will contribute and improve it.
  - rz0 16y ago
    Alternatives include: JML, C4J, Contract4J, JASS, and Modern Jass. The most popular and well-known solution is probably JML. I'd like to mention though that Cofoja itself is not so "new", in a sense; it is a rewrite of Modern Jass, which itself was a rewrite of JASS. Though the code may be mostly new, we've borrowed many concepts, ideas, and implementation techniques from our predecessors, and hopefully learnt a bit from their experience. One could then ask "why pick Modern Jass as a basis while there are other more <whatever> framework available?" but that's another question. Links: C4J. http://c4j.sourceforge.net/ http://c4j.sourceforge.net/ Contrac4J. http://www.contract4j.org/ http://www.contract4j.org/ Java with Assertions (JASS). http://csd.informatik.uni-oldenburg.de/~jass/ http://csd.informatik.uni-oldenburg.de/~jass/ Java Modeling Language (JML). http://www.jmlspecs.org/ http://www.jmlspecs.org/ Modern Jass. http://modernjass.sourceforge.net/ http://modernjass.sourceforge.net/ And if you're interested in the fine details of the internal differences between Cofoja and other frameworks, you may want to read my technical report: http://cofoja.googlecode.com/files/cofoja-20110112.pdf http://cofoja.googlecode.com/files/cofoja-20110112.pdf
jdp23 16y ago
Great to see, although it's really too bad that they didn't introduce this as part of the language when they developed it.
- dhimes 16y ago
  Live and learn, eh?
zlapper 16y ago
This is very similar to JML! I co-wrote a paper on the subject a couple years ago during my undergraduate, which I humbly share with you :) A Case Study in JML-Assisted Software Development http://portal.acm.org/citation.cfm?id=1556581&preflayout=flat http://portal.acm.org/citation.cfm?id=1556581&preflayout... Download: http://cic.puj.edu.co/wiki/lib/exe/fetch.php?media=grupos:avispa:papers:cbg_09.pdf http://cic.puj.edu.co/wiki/lib/exe/fetch.php?media=grupos:av...
- zlapper 16y ago
  (thinking out loud: wouldn't be cool if someone at Google contacts me? I'd love to work for them :)
Yrlec 16y ago
Microsoft has a similar project for .NET http://research.microsoft.com/en-us/projects/contracts/ http://research.microsoft.com/en-us/projects/contracts/ . Based on a quick look I think Microsoft's project is a bit more mature (already has VS-intergration for example).
- jefffoster 16y ago
  There was also an older project known as Spec# at http://research.microsoft.com/en-us/projects/specsharp/ http://research.microsoft.com/en-us/projects/specsharp/
- silverlake 16y ago
  MS is more advanced. It also has a static checker for contracts.
ivenkys 16y ago
A good thing to have - better than the "assert" keyword in Java.
tarkin2 16y ago
In the sorted parameters example contract, would it not be as good to pass an new object whose constructor ensures the sorting?
ShabbyDoo 16y ago
I have read a bit about Crystal SAF, a static analysis framework for Eclipse from CMU: http://code.google.com/p/crystalsaf/ http://code.google.com/p/crystalsaf/ 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. Also, Soot from McGill (http://www.sable.mcgill.ca/soot/ http://www.sable.mcgill.ca/soot/) 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.
ShabbyDoo 16y ago
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.

138 points by eneveu 16y ago

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

eneveu 16y ago
I did not know about KeYmeara. Looks great! While I'm not sure if we may count those as "programmation by contract", some Java tools provide (some) static analysis: - Findbugs - IntelliJ IDEA does some nullness analysis : http://www.jetbrains.com/idea/documentation/howto.html http://www.jetbrains.com/idea/documentation/howto.html - JSR 305 (Annotations for Software Defect Detection in Java) attempted to standardize on a set of annotations. We use it in our project, mainly the @Nonnull at the moment... I believe Findbugs considers these annotations. - CodePro Analytix, also recently open sourced by Google, might also do some static analysis: http://code.google.com/javadevtools/codepro/doc/index.html http://code.google.com/javadevtools/codepro/doc/index.html - Eclipse might too (any expert Eclipse user knows?) I think there is still a lot to do in this space. "Contracts for Java" is a step in the right direction :)
- tikkes 16y ago
  Eclipse does not do static analysis by default I believe. There are some patches however...
  - ShabbyDoo 16y ago
    The out-of-the-box Eclipse distro does include some static analysis stuff, but it's turned off by default. Preferences->Java->Compiler->Errors/Warnings. Under "Potential Programming Problems", you can alert on such things as guaranteed NPEs, etc.
- ShabbyDoo 16y ago
  For completeness, PMD should be added to the list although I haven't found it as useful as FindBugs: http://pmd.sourceforge.net/ http://pmd.sourceforge.net/

JVerstry 16y ago

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 !!!

eneveu 16y ago
It's still quite new, so for now I think you'll have to build it from source. I know it's annoying when a jar is not available in the Maven repository. But it shouldn't be a dealbreaker either. We have a Maven repository proxy for the company, so I deploy my jars there: mvn deploy:deploy-file ... It's better than having each developer manually install the jar in their local repository: mvn install:install-file ... More information: http://maven.apache.org/plugins/maven-deploy-plugin/usage.html http://maven.apache.org/plugins/maven-deploy-plugin/usage.ht... http://maven.apache.org/plugins/maven-install-plugin/examples/specific-local-repo.html http://maven.apache.org/plugins/maven-install-plugin/example...
- JVerstry 16y ago
  Well, it does not compile !!! There is no documentation about dependencies... This project is far from operational and mature !!! I'd really rather that people did not deliver half-ass projects and loose people's time...
- rz0 16y ago
  Yeah, sorry but you have to build it from source, for now. There is no point in making a release now as there are a few bugs that need correcting before that. But thanks for the feedback, I've added a README file now with proper dependency information and set up instructions. The build scripts are certainly quite shacky, I must admit; it was originally integrated into Google's internal build system but now that all of that has been stripped out (including the documentation), it looks kinda non-functioning. I could certainly use some help in making that build and run smoothly in the outer Java world, since I'm not a Java programmer originally and my experience setting up Ant, Maven and the like is very very limited. P.S.: It may be Google-branded but we're still just a small team. The other guys are taking care of the within-Google integration part so I should be working on the open source integration except I'm not very knowledgeable in the Java ecosystem, nor have I ever released any open source project with that level of visibility, so please be patient.

ajmurmann 16y ago

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?

endlessvoid94 16y ago
It's based on the idea of formal proofs for programs. There is a really good paper about this by dijkstra, but I can't seem to find it now. Basically you defined preconditions and postconditions for each function and it looks like this "contracts" flag will raise an exception if those conditions aren't met. This is probably a better way to test software, but you still need to know how to write the preconditions and postconditions concisely.
elviejo 16y ago
This contracts refer to the concept of "Design by Contract." http://en.wikipedia.org/wiki/Design_by_contract http://en.wikipedia.org/wiki/Design_by_contract The poster child of design by contract is the Eiffel Programming language. http://www.eiffel.com/developers/design_by_contract.html http://www.eiffel.com/developers/design_by_contract.html IMO Contracts help you te really reduce the number of unit test you need to write. And the tests that you DO write are more intersting in the BDD kind of way. I highly recommend to study design by contract. Is one of those things that will make you a better developer in any language you use. A good book with examples in Java and Eiffel is this: Design by Contract, by Example http://www.amazon.com/Design-Contract-Example-Richard-Mitchell/dp/0201634600 http://www.amazon.com/Design-Contract-Example-Richard-Mitche...
skybrian 16y ago
I haven't used contracts, but I think if you have more assertions in your code then you need fewer assertions in your tests. But you still need to exercise the code with about the same number of tests, or your testing won't find the bugs.

MarkSweep 16y ago

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

spicyj 16y ago
That sounds (close to) impossible. How would you tell if a given piece of code sorts a list properly? There are a million and one sorting algorithms and the static analyzer would have to be really smart to be able to check that reliably.
- atamyrat 16y ago
  Yes, it is impossible. See: Halting problem.
  - likpok 16y ago
    The thing about program verification is that everyone knows that of course it is in general impossible. However, I am not writing a simulator. Most of the code I write does not actually take advantage of the power of a Turing machine. The fact that the general problem is impossible does not mean that the entire area of study is useless.
    - riffraff 16y ago
      see: dependent typing http://en.wikipedia.org/wiki/Dependent_type http://en.wikipedia.org/wiki/Dependent_type and restricted languages such as Spark http://en.wikipedia.org/wiki/SPARK_(programming_language) http://en.wikipedia.org/wiki/SPARK_(programming_language)
- deleted 16y ago
  [deleted]
likpok 16y ago
I'm pretty sure that Pex [1] does the static analysis on these things. It's C#, but should be close enough for you to get the idea. [1]: You can play with it here: http://www.pexforfun.com/ http://www.pexforfun.com/

shareme 16y ago

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

regularfry 16y ago
Links?
eneveu 16y ago
You are not the only one arguing about the project's lack of maturity and the existence of better, more mature alternatives (which ones?). I can understand this sentiment, and I'd love to be able to add a Maven dependency on this project and start using it on production code tomorrow (well, monday actually). But I am also glad Google followed the "ship early, ship often" mantra . Better alternatives may or may not exist, but I'm pretty sure I had never heard of them before, and never really cared for "contract programming" until now. I knew about JSR 305 and used the @Nonnull annotation when it made sense, but that's about it (I guess doing this already puts me ahead of 80% of Java programmers in this regard...). Some might say that it's sad people waited for a Google-branded project to be interested in this subject. I choose to view it as an opportunity for the field as a whole. The interesting discussions it sparked (here and on other websites) are worth it by themselves. Some developers might even compare options and start using one of the "better alternatives" you hint about. The project may be young, but it seems to generate a lot of interest, and I'm sure many people will contribute and improve it.
- rz0 16y ago
  Alternatives include: JML, C4J, Contract4J, JASS, and Modern Jass. The most popular and well-known solution is probably JML. I'd like to mention though that Cofoja itself is not so "new", in a sense; it is a rewrite of Modern Jass, which itself was a rewrite of JASS. Though the code may be mostly new, we've borrowed many concepts, ideas, and implementation techniques from our predecessors, and hopefully learnt a bit from their experience. One could then ask "why pick Modern Jass as a basis while there are other more <whatever> framework available?" but that's another question. Links: C4J. http://c4j.sourceforge.net/ http://c4j.sourceforge.net/ Contrac4J. http://www.contract4j.org/ http://www.contract4j.org/ Java with Assertions (JASS). http://csd.informatik.uni-oldenburg.de/~jass/ http://csd.informatik.uni-oldenburg.de/~jass/ Java Modeling Language (JML). http://www.jmlspecs.org/ http://www.jmlspecs.org/ Modern Jass. http://modernjass.sourceforge.net/ http://modernjass.sourceforge.net/ And if you're interested in the fine details of the internal differences between Cofoja and other frameworks, you may want to read my technical report: http://cofoja.googlecode.com/files/cofoja-20110112.pdf http://cofoja.googlecode.com/files/cofoja-20110112.pdf

jdp23 16y ago

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

dhimes 16y ago
Live and learn, eh?

zlapper 16y ago

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

zlapper 16y ago
(thinking out loud: wouldn't be cool if someone at Google contacts me? I'd love to work for them :)

Yrlec 16y ago

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

jefffoster 16y ago
There was also an older project known as Spec# at http://research.microsoft.com/en-us/projects/specsharp/ http://research.microsoft.com/en-us/projects/specsharp/
silverlake 16y ago
MS is more advanced. It also has a static checker for contracts.

ivenkys 16y ago

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

tarkin2 16y ago

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

ShabbyDoo 16y ago

I have read a bit about Crystal SAF, a static analysis framework for Eclipse from CMU: http://code.google.com/p/crystalsaf/ http://code.google.com/p/crystalsaf/ 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. Also, Soot from McGill (http://www.sable.mcgill.ca/soot/ http://www.sable.mcgill.ca/soot/) 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.

ShabbyDoo 16y ago

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.