Executable Documentation of Template-Hook Interactions in Frameworks using JML

Date
2006-06-01
Authors
Khanolkar, Neeraj
Leavens, Gary
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
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.

Description

Copyright © 2006, Neeraj Khanolkar and Gary T. Leavens All Rights Reserved.

Keywords
Formal specification, object-oriented framework, runtime assertion checking, template, hook, temporal process documentation, preconditions, postconditions, flow-based assertions, JML
Citation
DOI
Source
Collections