Modeling Types

June 22, 2010 – 6 years, 9 months ago, by eifler

Short Description

If an interface specification language provides several built-in modeling types, a fundamental problem arises in how to specify them in a way that is useful for verification. Modeling types can, of course, be specified using other modeling types, but ultimately some modeling types must be specified in some other way.

Challenge: Develop a specification technique for modeling types.

Code

Specification

Long Description

One of the key innovations in JML’s design is the use of a library of modeling types that describe mathematical bags (multisets), sets, sequences, relations, and maps. These modeling types play the same role in a JML specification as the built-in traits in the Larch Shared Language or the built-in types of VDM: they allow the specifier to describe abstract values of objects using standard mathematical notions. These types are designed to have immutable objects, to better match mathematics. They allow the specification of abstract values, especially for collection classes. For example, the abstract value of a java.util.Collection can be specified using a (specification-only) model field whose type is a JMLEqualsBag. While the hope was that such types would be useful for both runtime assertion checking and static verification, they do not work well with static verification.

Supplementary Materials

The paper by Gary T. Leavens and K. Rustan M. Leino and Peter Müller from which this challenge is taken contains some additional information including references to relevant papers related to this challenge. Some more specification and verification challenges which are also included on this site can also be found there.

Submitted by

Timo Eifler verifythis@cost-ic0701.org