Tool development

The LOOP project is centered around the LOOP tool. The latter is a compiler, which translates classes in object-oriented languages into logical theories, for use in proof tools. Its use can be illustrated as follows.

[A picture of how the LOOP tool works]

Originally, only the translation for CCSL existed. This original version is currently under revision in Dresden. The Java translation is now reasonably stable. The JML translation is still under construction.

The LOOP tool is implemented in Ocaml. It has an Emacs interface. It is not publicly available, mainly because it is not stable enough and because there is no explicit documentation.

More information is available from J. van den Berg, B. Jacobs, The LOOP compiler for Java and JML In: T. Margaria and W. Yi (eds.), Tools and Algorithms for the Construction and Analysis of Software (TACAS), (Springer LNCS 2031, 2001) 299--312. © Springer-Verlag