Proving Theorems About JML Classes - Formal Methods and Hybrid Real-Time Systems - page 275

(a) hm ∈ Z ↔ P ( Z × ( OID × VID ))

VID ))
These proof obligations depend on the nature of the Z toolkit operators and laws
that have been used. For instance, when applying relational overriding to hm in
the Put operation the proof obligation (a) is generated, or when applying some
laws on injections, such as
∀ f : X Y •∀x :dom f • f ∼ ( fx )= x
another proof obligation (b) is generated. Other examples of proof obligations
that are not related to type checking are what in Z/Eves is known as forward
rules . They expose some important property P of a schema S , which is usually
easy to prove, without requiring further proofs involving S and assuming P to
expand S , hence cluttering the goal with unnecessary detail. For instance, this
happens often with state schemas, where the state invariant is needed to finish
some proof about an operation over the map. Again, this is a general lesson
previously learned from earlier work [42].
It is through these and other kinds of proof obligations arising whilst ma-
nipulating goals that we found problems in the original design, as well as inter-
esting/reusable lemmas for similar problems. This is the major benefit of such
mechanisation efforts: they produce reusable general theories that can benefit
other future verification experiments and verified components. For the experi-
ment explained in this paper, we relied on around 85-95 of these lemmas and
rules, from which around 8-10 could be generally reused in any context, and
many more that could be reused whenever injections and injective sequences
are involved. Fortunately, most of this essential machinery was already avail-
able. From [42], we got most of the general material on injections and sequences.
In [11], most of the specific rules for Entry and HM were provided. Thus, we
reused quite a large number of lemmas, resulting in a much lower burden of
proof. In this particular case, that low burden is because the work in [11] was
already targeted at hash maps. Obviously, in general the reuse is not always
that high, yet as the number of experiments grows, the richer the set of general
theories becomes, hence the greater the chances of having higher reuse rates.

(b) hm ∈ N ( Z → ( OID ×

4 Conclusions

There are many opportunities for profitable interaction between JML and dif-
ferent mechanised formalisms: this paper describes just the tip of the iceberg.

4.1 Verifying the JML Type System

JML and its tools rely on the correctness of annotations, which in turn rely on the
underlying JML meta-type system to provide functionalities, such as side-effect
free bounded predicates and varied equational theories. So subjecting the type
system to the scrutiny of mechanical theorem proving is likely to be beneficial.
And JML already goes in this direction: there are quite detailed annotations
within the meta-type system.