Specification of the Javacard API in JML
Erik Poll, Joachim van den Berg, Bart Jacobs · 2000
This paper reports on an effort to increase the reliability of JavaCard-based smart cards by means of formal specification and verification of JavaCard source code. As a first step, lightweight formal interface specifications, written in the specification language JML, have been developed for all the classes in the JavaCard API (version 2.1). They make many of the implicit assumptions underlying the current implementation explicit, and thus facilitate the use of this API and increase the reliability of the code that is based on it. Furthermore, the formal specifications are amenable to tool support, for verification purposes. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.