This article describes a case study concerning a component of a Java Purse applet developed by the smart card manufacture Gemplus. This component is a representation of decimal numbers in Java. The decimal component is annotated with specifications consisting of invariants and pre- and postconditions, describing the functional behavior. These specifications are written in the specification language JML. After translation of the annotated source code to the theorem prover PVS, the correctness of these annotations is proved interactively.
展开▼
