Toward Automatic Generation of Provably Correct Java Card Applets
Alessandro Coglio · 2003
This paper overviews an ongoing project aimed at developing an automatic generator of Java Card applets from higher-level spec(ification)s written in a domain-specific language called "SmartSlang ". The generator is based on Specware, a system for the formal specification and refinement of software. The applet generator translates a SmartSlang spec into the logical language of Specware, re-expresses the translated spec in terms of Java Card concepts via a series of refinement steps using Specware's machinery, and generates Java Card code from the refined spec. The Java Card concepts used for refinement and code generation are captured as a shallow embedding of the Java Card language and API in the logic of Specware. Since proofs are associated to refinement steps, the applet generator produces a machine-processable proof tree along with the code, enabling the correctness of the generated code (with respect to the spec) to be checked independently from the applet generator, via a smaller and simpler applet checker to be also developed in this project.