Formal Methods Europe

Homepage of FME

3rd JML Spec-a-thon summary

By Bernhard Aichernig • Nov 16th, 2010 • Category: Sponsored by FME

The 3rd JML Spec-a-thon finished up on Friday the 5th of November. Following up on my email of the 2nd that summarized our first couple of days, we thought we’d give the community a taste of what else went on at the event and what our concrete outcomes are.

As a recap, early in the week we reviewed the “state of JML” from a language, tool, and library perspective. We spent an afternoon on this topic, documenting for ourselves and the world where we think the community could/should head, given the current state of affairs, for the benefit of all.

The BON diagram located at (https://sourceforge.net/apps/trac/jmlspecs/attachment/wiki/WikiStart/JMLEcosystem.gif) summarizes this discussion pictorially at a high level. We plan on turning this document into a hyperlinked image in the JML Trac wiki so that owners of respective components (nodes, edges and edge endpoints) can write short summaries. We also think it is important to setup this information in the wiki so that it stays “live” so that anyone, at any time, can figure out how “lively” and stable any component is, much like we have done on the Mobius Trac (i.e., implicitly include the last ‘n’ tickets updated/wiki pages touched/releases shipped, etc.).

This discussion left us with several open questions about the status of recent developments and support for tools with which we are not directly involved. We requested that the developers and maintainers of some of the major tools in the JML world (e.g., JIR, JavaContracts, JMLEclipse, OpenJML, JAJML, AJML, KeY, jml4c, OpenJIR, Beetlz, SafeJML, etc.) let us know about their current state-of-affairs, so we have seen several emails on the list about this. We also spoke with several tool developers during the week either via email or over Skype.

This work turned us toward a discussion of Microsoft’s tools, as I have used some of these challenge problems for teaching this semester here at ITU. In my course, “Analysis, Design, and Software Architecture,” students learn about the obvious topics (from our community’s point of view) using BON, UML, C#, Code Contracts, Pex, and Visual Studio 2010 Ultimate Edition. Thus, we wrote contracts for some of the C# solutions to the challenge problems and then attempted to push Microsoft’s Code Contracts compiler and static checker and Pex to their limits.

This exercise gave us a hands-on feel for the strengths and weaknesses of these tools and let us better understand what Microsoft has found to be “digestible” by Windows programmers. This made us feel proud of what the JML community has accomplished in our “spare time,” but also inspired us to push toward completion and integration of recent projects.

Several of the younger participants then turned their attention to learning JML better an writing specs for several of the new classes in JDK 1.5+ that had high client usage based upon the analysis performed at earlier Spec-a-thons. Several specifications will be committed to the Specs project in the SVN repository as a result (Søren, Josu, and Daniel, *hint hint*).

A number of talks were given also about JML-related work, including David Cok presenting his new front-end for automated (primarily SMT) solvers, Josu Martinez about automatically synthesizing JML specifications for Orc programs, Dermot Cochran about new techniques for test case generation for e-voting systems based upon automated solvers and model checking, Daniel Bruns about new developments in the KeY world, Dan Zimmerman on the new JMLunitNG tool, and Joe Kiniry and Josu Martinez on new proposed extensions to JML for orchestrating specifications. We also spoke with Patrice Chalin and Robby about their current exciting work on JMLEclipse and related technologies.

Finally, with regards to concrete software deliverables, we are proud to announce that new versions of three tools will be shipped soon as a result of work at the Spec-a-thon.

First, Dan gave us a cool demonstration of the JMLunitNG tool. He generated thousands of usable unit tests in a second and showed how he could quickly run millions of tests, something far beyond the capabilities of the original JMLunit. Dan promises the announcement of a new version of the test generator with several new features, including supporting test generation that takes signals clauses into account in a smart fashion, Real Soon Now.

Secondly, David, Dan, and myself worked together to merge the latest release of the OpenJDK (1.7-b116) into OpenJML. This merge and patch took us a couple hours of work, with another couple of hours of tweaks to get all unit and system tests to pass again. This gave Dan and me a improved understanding of the OpenJDK’s project organization and its compiler. Consequently, a new prototype release of OpenJML for Java 1.7 is imminent.

Finally, Dan has been working with MacPorts and BSD Ports developers on a new release of OpenJDK 1.7 for OS X. This is critical work for the community, as Apple has announced that they will no longer develop, ship, and support JDK for OS X. We believe that Apple is forcing Oracle and/or the Open Source community to do this work for them. Given the market share that OS X now possesses, this is an understandable move, but it still makes us nervous and want to do something positive about the situation.

So, that just about wraps up this edition of the Spec-a-thon. We have, as a result of this third event, consumed the remainder of our funding for running Spec-a-thons. David, Dan, and I are discussing pursuing new funding via the Danish government in the next week. As a part of this grant proposal, we intend on organizing the first JML Conference, and would love any senior members of the community that wish to help out to sign up.

Thanks to all that participated and supported this, and past events. Photos of the 3rd Spec-a-thon will undoubtedly be going up on the webpage soon.

Joe Kiniry and Dan Zimmerman

Comments are closed.