Grade Counter

This example reads grades from an input array. The number of each grade level is counted. If there are more than 10 "F"s, the output variable excessiveFailure is set to 1.

In the implementation, there is an error in that the excessiveFailure variable is set based on the number of "D"s rather than the number of "F"s. This example exhibits the value of TASS's loop co-invariant functionality. Using traditional model checking techniques, a depth first search of the state space occurs. This search is exponential in the number of students (N_BOUND). With TASS's loop co-invariants, the bug is quickly discovered.

Correct Version

#pragma TASS input {N_BOUND > 0}
int N_BOUND;
#pragma TASS input {N > 0 && N < N_BOUND} 
int N;
#pragma TASS input 
double scores[N];
#pragma TASS output 
int excessiveFailure;
int failureFlag = 0;
int numGrade[5];

void main() {
	int i = 0;
	
	for(; i < 5; i++)
		numGrade[i] = 0;
	i=0;
l:
	while(i < N) {
		if(scores[i] >= 90.0)
			numGrade[0]++;
		else if(scores[i] >= 80.0)
			numGrade[1]++;
		else if(scores[i] >= 70.0)
			numGrade[2]++;
		else if(scores[i] >= 60.0)
			numGrade[3]++;
		else
			numGrade[4]++;
		if(numGrade[4] > 10)
			failureFlag = 1;
		i++;
	}
	excessiveFailure = failureFlag;
}

Incorrect Version

#pragma TASS input {N_BOUND > 0} 
int N_BOUND;
#pragma TASS input {N > 0 && N < N_BOUND} 
int N;
#pragma TASS input 
double scores[N];
#pragma TASS output 
int excessiveFailure;
int failureFlag = 0;
int numGrade[5];

void main() {
	int i = 0;
	
	for(; i < 5; i++)
		numGrade[i] = 0;
	i=0;
l:
#pragma TASS jointinvariant @main {numGrade[0] == spec.numGrade[0] && numGrade[1] 
== spec.numGrade[1] && numGrade[2] == spec.numGrade[2] && numGrade[3] == 
spec.numGrade[3]  && numGrade[4] == spec.numGrade[4] && failureFlag == spec.failureFlag 
&& i >= 0 && i == spec.i}
	while(i < N) {
		if(scores[i] >= 90.0)
			numGrade[0]++;
		else if(scores[i] >= 80.0)
			numGrade[1]++;
		else if(scores[i] >= 70.0)
			numGrade[2]++;
		else if(scores[i] >= 60.0)
			numGrade[3]++;
		else
			numGrade[4]++;
		if(numGrade[3] > 10)
			failureFlag = 1;
		i++;
	}
	excessiveFailure = failureFlag;
}

TASS Interaction

 $ ./tass compare -loop examples/gradeCount/gradeCountSpec.c
 examples/gradeCount/gradeCountImpl.c
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|  version 1.0_r1777 (2010-07-12)        http://vsl.cis.udel.edu/tass  |
+----------------------------------------------------------------------+
       specification : gradeCountSpec (numProcs = 1)
      specSourceFile : examples/gradeCount/gradeCountSpec.c
      implementation : gradeCountImpl (numProcs = 1)
      implSourceFile : examples/gradeCount/gradeCountImpl.c
                mode : COMPARE
              prover : CVC3
            deadlock : ABSOLUTE
           reduction : URGENT
            simplify : true
      simplifyProver : false
         bufferBound : 10
             verbose : false
         loop method : true
          repository : ./TASSREP
            frontend : MINIMP
          errorBound : 1

Comparing gradeCountSpec and gradeCountImpl...


 ************ ERROR DETECTED ************
Execution error (kind: FUNCTIONAL_COMPATIBILITY, certainty: MAYBE)
Corresponpdence of joint invariants could not be established.
 with:
  Process 0 at location 4: gradeCountSpec.c 19.1--19.13: "while(i < N)"
  Process 1 at location 4: gradeCountImpl.c 21.1--21.13: "while(i < N)"

Writing trace to gradeCountSpec_gradeCountImpl.trace...Invalid query pc => co-invariants 
in corresponding loops.
{gradeCountSpec_numGrade_l_0[4]=90, gradeCountImpl_numGrade_l_0[1]=0, 
gradeCountSpec_numGrade_l_0[1]=0, gradeCountSpec_numGrade_l_0[3]=0, gradeCountSpec_i_l_0=0, 
gradeCountImpl_numGrade_l_0[2]=0, gradeCountSpec_numGrade_l_0=(ARRAY (arr_var: INT): IF 
(arr_var = 0) THEN 0 ELSE IF (arr_var = 1) THEN 0 ELSE IF (arr_var = 2) THEN 0 ELSE IF 
(arr_var = 3) THEN 0 ELSE 90 ENDIF ENDIF ENDIF ENDIF), gradeCountSpec_failureFlag_l_0=0, 
gradeCountSpec_numGrade_l_0[2]=0, gradeCountImpl_numGrade_l_0=(ARRAY (arr_var: INT): IF 
(arr_var = 0) THEN 0 ELSE IF (arr_var = 1) THEN 0 ELSE IF (arr_var = 2) THEN 0 ELSE IF 
(arr_var = 3) THEN 0 ELSE 90 ENDIF ENDIF ENDIF ENDIF), gradeCountImpl_numGrade_l_0[4]=90, 
X1=1, X0=2, gradeCountImpl_numGrade_l_0[0]=0, gradeCountImpl_numGrade_l_0[3]=0, X2=(ARRAY 
(arr_var: INT): 90), gradeCountImpl_failureFlag_l_0=0, gradeCountSpec_numGrade_l_0[0]=0, 
gradeCountImpl_i_l_0=0, X2[0]=90}
done.

Writing model gradeCountSpec.model...done.
Writing model gradeCountImpl.model...done.
STATS:
   statesSeen    : 53
   statesMatched :  1
   statesSaved   : 53
   transitions   : 53
   numValues        : 154
   numQueries       : 23
   numMessages      : 0
   numValidCalls    : 0
   numSimplifyCalls : 0
   time          : 1.113s.

RESULT: gradeCountSpec and gradeCountImpl MAY NOT be functionally equivalent. Counterexample found.