Executable Documentation of Template-Hook Interactions in Frameworks using JML
                                  by
                 Neeraj Khanolkar and Gary T. Leavens

			       Abstract

Object-oriented frameworks are an important technique for capturing
design expertise. However, the learning curve for a framework is
usually quite steep and can be the biggest obstacle in its
adoption. We propose an executable and yet readable method for
framework documentation using the Java Modelling Language (JML), based
on the specification of the interaction between a framework's template
methods and its customizable hooks. This method is geared toward
allowing the developers to quickly instantiate a prototype application
from the framework, which can be later tweaked using some other
detailed and usually non-executable documentation.  We use flow-based
assertions to specify the hook method preconditions and template
method postconditions. The flow-based precondition for a particular
hook serves as a modular documentation of when and how that hook is
called in the framework's overall call-sequence. Similarly, the
flow-based postcondition of a template method tells the possible
sequences of hook invocations that its execution may cause.
Flow-based assertions are written using a few types, which we
precisely specify. We also briefly describe a case study that uses our
technique to document a Model-View-Controller framework.

Keywords: Formal specification, object-oriented framework, runtime
assertion checking, template, hook, temporal process documentation,
preconditions, postconditions, flow-based assertions, JML.

2006 CR Categories:
D.1.5 [Programming Techniques]
        Object-oriented programming;
D.2.1 [Software Engineering]
        Requirements/Specifications --- languages, JML;
D.2.4 [Software Engineering]
        Software/Program Verification --- assertion checkers,
        programming by contract;
F.3.1 [Theory of Computing]
        Logics and Meanings of Programs --- assertions, pre- and
        post-conditions, specification techniques.