4 ms·
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
by 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 agoI 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 agoEclipse does not do static analysis by default I believe. There are some patches however...
- ShabbyDoo 16y agoThe 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 agoFor 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/