CW 343

K. Mertens, N. Smeets, M. van Dooren, J. Dockx, E. Steegmans
A New Semantics for JML Signals Clauses

Abstract

JML, which stands for "Java Modeling Language", is a behavioral interface specification language designed to specify Java classes and interfaces. JML uses syntactic sugar to make specifications easier to read and write. In this paper, we reveal that the current JML desugaring of signals clauses has a somewhat counterintuitive meaning. A new semantics is proposed that is more intuitive. Special attention is given to the desugaring of signals clauses that are spread over different behavior blocks connected by the keywords also or and. The described desugaring ensures behavioral subtyping. The consequences of the new semantics are worked out.