Experimental Units

Programs Characterization

In Table 1 we present the characterization of the programs that we use in the first study (evaluation of our RGT-based approach). The programs are characterized in terms of size (LOC - lines of code and LJML - lines of JML specification):

Table 1. Programs Characterization for the first study

In Table 2 we present the characterization of programs that we use in the second study (the comparison of two RGT-based approaches: JMLOK and JET).

Table 2. Programs Characterization for the second study

Experimental units of our RGT approach (JMLOK) evaluation:

Sample programs

Open-source JML programs

• Bomber
• Healthcard
• Jaccounting
• Jspider
• Mondex
• TransactedMemory

Experimental units of the comparison between JMLOK and JET:

Sample programs

Open-source JML programs

• Jaccounting
• Mondex
• TransactedMemory