Adding Intermediate Assertions (1)
global: a == a
0
static int search(int a[], int v)
{
for( int i = 0; i < a.length; i++ )
{
if( a[i] == v )
{
r = i;
return i;
}
}
r = -1;
return -1;
}
[((
i) a[i] == v)
¨
a[r] == v] ^ [((
i) a[i] != v)
¨
r == -1]