Computing at Glasgow University
Paper ID: 9376
DCS Tech Report Number: TR-2011-326

Hanoi: A Typestate DSL for Java
McGinniss,I. Gay,S.J.

Publication Type: Tech Report (internal)
Appeared in: DCS Technical Report Series
Page Numbers : 20
Publisher: Dept of Computing Science, University of Glasgow
Year: 2011

URL: This publication is available at this URL.


Many APIs contain interfaces in which methods have strict state based preconditions, while mainstream programming languages provide no facility to express these constraints in a concise, human readable, machine verifiable form. Failure to detect violations of these preconditions can result in partial or catastrophic failure of a system, therefore programmers must take great care in understanding and verifying the usage of such APIs. We present a domain specific language, Hanoi, which can be used to express state restrictions in APIs. By classifying Hanoi and existing typestate languages and highlighting their differences, we show Hanoi can be more concise and potentially easier to understand than existing approaches. We also present a simple dynamic checking system which uses Hanoi models to verify interface usage, alleviating the burden on the implementer of such interfaces to defend against incorrect usage.

Keywords: typestate, state modelling, programming language design, domain specific languages

PS/PS.GZ PDF Bibtex entry Endnote XML