Executable Documentation of Template-Hook Interactions in Frameworks using JML







Deposit Papers 


Khanolkar, Neeraj and Leavens, Gary T. (2006) Executable Documentation of Template-Hook Interactions in Frameworks using JML. Technical Report 06-18, Computer Science, Iowa State University.

Full text available as:Adobe PDF


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.
Subjects:Software: PROGRAMMING TECHNIQUES (E): Object-oriented Programming
Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
ID code:00000437
Deposited by:Gary T. Leavens on 21 July 2006
Alternative Locations:

Contact site administrator at: