The Mobius Demonstrator Case Study

Nov. 15, 2010 – 6 years, 5 months ago, by woj

Short Description

The Mobius Demonstrator Quiz Game has been annotated with JML to specify the so-called mildet navigation graph property. Then it has been verified with ESC/Java2.


The complete case study can be downloaded from:


The code is specified with JML annotations in the Java files of the project.

Long Description

A thorough description of the case study can be found in the technical report:

Wojciech Mostowski and Erik Poll, Midlet Navigation Graphs in JML

available at:

This is about to be published in the 13th Brazilian Symposium on Formal Methods, SBMF2010 LNCS proceedings too.

Supplementary Materials

Submitted by

Wojciech Mostowski