...NORA/HAMMR

NORA is no real acronym; HAMMR is the highly-adaptive multi-method retrieval tool. This work has been sponsored by the DFG under grant Sn11/2-3.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...task:

Actually, the proof tasks are universally closed wrt. the formal input and output parameters of the component and the query and also contain equations relating the parameters. Likewise, the pre- and postconditions are of course logical functions of the respective parameters. However, to improve the legibility, we use this traditionally abbreviated formulations.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...user.

It is technically easy to create a domain-specific extension of a specification language: this only requires that a set of predefined function and predicate names is defined, whose meaning is given by some additional axioms.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...restrictive.

In fact, the latter problem can be tackled by use of additional axioms which allow e.g. interchanges of parameters, and for the former we propose the use of abstract model checking.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.