Assertion can be verified, similar postcondition cannot?

Sep 21, 2011 at 1:43 PM

Hi all,
I've got another question if I may.
I am trying to verify an implementation of C's strcmp function. This is what I came up with:

#include <vcc.h>
int strcmp(const char* s1, _(ghost size_t s1Size) const char* s2 _(ghost size_t s2Size))
_(requires \thread_local_array(s1, s1Size))
_(requires \thread_local_array(s2, s2Size))
_(requires \exists unsigned int i;  i < s1Size && s1[i] == '\0')
_(requires \exists unsigned int i;  i < s2Size && s2[i] == '\0')
_(ensures \result >= -1 && \result <= 1)
{
	int ret;
	unsigned int i;
	for (i = 0; s1[i] == s2[i]; ++i)
	_(invariant i >= 0 && i < s1Size)
	_(invariant i >= 0 && i < s2Size)
	_(invariant \forall unsigned int j; j < i ==> s1[j] != '\0')
	_(invariant \forall unsigned int j; j < i ==> s2[j] != '\0')
	_(invariant \forall unsigned int j; j < i ==> s1[j] == s2[j])
	{
		if (s1[i] == '\0')
		{
			ret = 0;
			_(assert (\exists unsigned int k; (k < min(s1Size, s2Size) &&
				(\forall unsigned int j; j < k ==> s1[j] == s2[j]) &&
				(s1[k] == '\0' && s2[k] == '\0'))) ==> ret == 0)
			return ret;
		}
	}
	
	ret = s1[i] < s2[i] ? -1 : 1;

	_(assert (\exists unsigned int k; (k < min(s1Size, s2Size) &&
		(\forall unsigned int j; j < k ==> s1[j] == s2[j]) &&
		(s1[k] < s2[k]))) ==> ret == -1)
	_(assert (\exists unsigned int k; (k < min(s1Size, s2Size) &&
		(\forall unsigned int j; j < k ==> s1[j] == s2[j]) &&
		(s1[k] > s2[k]))) ==> ret == 1)
	return ret;
}

_(ghost _(pure) size_t min(size_t a, size_t b)
_(ensures \result == (a <= b ? a : b))
)

The code as it is can be verified completely. However, when taking the assertions from right before the return statements and
adding them as function postconditions (by just changing "assert" to "ensures" and "ret" to "\result"), they cannot be verified
anymore.
Again, I would be glad for any help.
Marian

Developer
Sep 26, 2011 at 10:52 AM

Hi Marian,

The problem is that you have put different assertions before the different return statements. So for example, the assertion inside the loop has as conclusion "ret == 0" which is trivial in that branch (because you just did "ret = 0"), but not so trivial for the return at the end of the funtion. Conversely, the assertions from just before the end of the functions might not hold if the function returns from inside the loop.

Indeed, the function does not satisfy the postonditions corresponding to your assertions, because the hypotheses of your postconditions are missing the hypotheses "s1[j] != '\0'" (i.e., they should read "j < j ==> s1[j] == s2[j] && s1[h] != '\0'). In particular, if s1[0] = s2[0] = '\0', but s1[1] > s2[1], then you would have to return 0 (by the postcondition from inside the loop), but you would also have to return 1 (by the postcondition from outside the loop).

Hope this helps,

ernie

Sep 27, 2011 at 6:11 PM

You're right, I didn't think about that. Thanks to your explanation I managed to verify the postconditions :)

Marian