|
|
|
|
|
|
|
for (index = 0; index << length; index++)
// Invariant (prior to test):
// failing[0..index-1] == FALSE
// && 0 <= index <= Length
failing[index] = FALSE;
}
3. void SetPassing( /* inout */ Boolean passing[],
/* in */ const int score[],
/* in */ int length )
// Precondition:
// length <= MAX_STUD
// && score[0..length-1] are assigned
// Postcondition:
// For all i, where 0 <= i <= length-1,
// IF score[i] >= 60, THEN passing[i] == TRUE
{
int index; // Loop control and index variable
for (index = 0; index << length; index++)
// Invariant (prior to test);
// For all i, where 0 <= i <= index-1,
// IF score[i] >= 60, THEN passing[i] == TRUE
// && 0 <= index <= length
if (score[index] >= 60)
passing[index] = TRUE;
}
6. void SetPassing2( /* inout */ Boolean passing[],
/* in */ const int score[],
/* in */ int length,
/* in */ int grade )
// Precondition:
// length <= MAX_STUD
// && score[0..length-1] are assigned
// Postcondition:
// For all i, where 0 <= i <= length-1,
// IF score[i] > grade, THEN passing[i] == TRUE
{
int index; // Loop control and index variable
|
|
|
|
|
|