JMLFoldingEditorExplanation

Folding editors allow one to manually or automatically show or hide various structured pieces of a document--for example, hiding the contents of a section while only keeping the section title, which is similar to hiding the implementation of a method while keeping its signature. The process of hiding and showing a usually larger or complex construct behind a concise visual representation is called "folding".

Basic folding editors permit one to manually fold and unfold constructs like source code documentation and implementation structures like method and loop bodies. Advanced folding editors provide additional features like saving and restoring the state of folding when a file is closed and then opened again, or automatically folding a set of related constructs. An example of the latter is the "short" or "contract" form supported by IDEs like EiffelStudio, whereby the implementations of all features (fields and methods) of a class are folded and hidden from the developer--only natural language documentation and contracts remain in view.

The JML Folding Editor, known under the development code name as "Grok", is an Eclipse plugin that has built-in support for folding JML specifications in an intelligent fashion. It is based upon the Open Source Coffee-Bytes folding plugin.

Manual manipulation of folding is supported, as is customizable defaults in folding behavior. For example, when a file is initially opened, should loop bodies be folded or unfolded? Perhaps only all private method bodies should be folded?

The MOBIUS extensions to this plugin focus on support for folding, in an intelligent fashion, JML formal specifications. For example, groups of adjacent related specifications written in line comments are folded as a unit. Furthermore, the state of folding within a file is saved when the Mylyn subsystem is in use. Finally, some basic notions of fisheye views (Furnas86) have been included in the subsystem.

Our next steps in the research work focus on further evolving and experimenting with fisheye notions of Degree of Interest in the context of software systems with formal specifications. Given the numerous syntactic and semantic relationships that exist between code constructs and specification constructs, and observing the ways in which verification-centric software development and verification takes place, there are many fertile opportunities for good computer-human interaction research.

Version: 2 Time: Tue Apr 1 16:30:10 2008 Author: dcochran (dcochran) IP: 193.1.132.32