Adding Input and Output
Assertions (shown
in red)
a == a0
static int search(int a[], int v)
{
for( int i = 0; i < a.length; i++ )
{
if( a[i] == v )
{r = i;
return i;
}
} r = -i;
return -1;
}
[a == a0 ] ^ [(($ i) a[i] == v) ¨ a[r] == v] ^ [(("i) a[i]
!= v) ¨ r == -1]
r
represents the returned value
r
represents the returned value