Contractor Validation Tool

All the files necessary for replaying this case studies are available in the examples section of this web site.

2. Signature

Class source: JDK 1.4 implementation (Java)
Behaviour requirements sources: i) Javadoc documentation restrictions; ii) Manually-generated model presented in a paper by Dallmeier et al. Paper and Model.

The Java Signature class is used to provide applications the functionality of a digital signature algorithm. There are three phases to the use of a Signature object for either signing data or verifying a signature:

1. 1. Initialization, with either a public key, which initializes for verification (initVerify), or a private key, which initializes for signing (initSign).
   

2. 2. Updating, which updates the bytes to be signed or verified (update).
   

3. 3. Signing or verifying a signature on all updated bytes (sign and verify respectively).
   

We ran Contractor on a C version of the JDK 1.4 implementation of class Signature, introducing requires clauses that prevented exceptions from being thrown. We obtained the following abstraction:

The resulting abstraction clearly represents how an instance of Signature can only be in 3 different states: uninitialized (S3), initialized for signing (S23) or initialized for signature verification (S27). After checking the source code, we find that the implementation stores this information in an integer variable named state, which takes values from the set {UNINITIALIZED, SIGN, VERIFY}.

Our abstraction proved to be a faithfull representation of both the manually-generated model, depicted in the following abstraction, as well as the restrictions imposed by the official Java documentation.

ICSE 2011 Manuscript Case Studies