June 22, 2010 – 6 years, 9 months ago, by eifler
If an interface speciﬁcation language provides several built-in modeling types, a fundamental problem arises in how to specify them in a way that is useful for veriﬁcation. Modeling types can, of course, be speciﬁed using other modeling types, but ultimately some modeling types must be speciﬁed in some other way.
Challenge: Develop a speciﬁcation technique for modeling types.
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 speciﬁcation as the built-in traits in the Larch Shared Language or the built-in types of VDM: they allow the speciﬁer 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 speciﬁcation of abstract values, especially for collection classes. For example, the abstract value of a java.util.Collection can be speciﬁed using a (speciﬁcation-only) model ﬁeld whose type is a JMLEqualsBag. While the hope was that such types would be useful for both runtime assertion checking and static veriﬁcation, they do not work well with static veriﬁcation.
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.
Timo Eifler email@example.com