3 ms·
> I also recall some Java extension but can't find it atm. You might be thinking of JML (Java Modeling Language): http://www.eecs.ucf.edu/~leavens/JML//index.s
by tom_mellior 10y ago
> I also recall some Java extension but can't find it atm.
You might be thinking of JML (Java Modeling Language): http://www.eecs.ucf.edu/~leavens/JML//index.shtml http://www.eecs.ucf.edu/~leavens/JML//index.shtml
Apparently JML-annotated programs can passed to Why3 using a confusingly documented set of tools: http://krakatoa.lri.fr/ http://krakatoa.lri.fr/
There is also the Cheker Framework for Java: http://types.cs.washington.edu/checker-framework/ http://types.cs.washington.edu/checker-framework/
But as far as I understand it's less general than all the other tools you mention.
- tom_mellior 10y agoAlso, and probably even more likely than the ones I mentioned above, there is KeY for Java verification: http://www.key-project.org/index.php http://www.key-project.org/index.php