Adding Intermediate Assertions (4)
global:
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; a[r] == v
} ( ( k < i + 1) a[k] == v)
} r = -1;
return -1; ((
k) a[k] != v) ^ r == -1
}
[(( i) a[i] == v) ¨ a[r] == v] ^ [(( i) a[i] != v) ¨ r == -1]
