Convert C language code to problem specification by computing the invariant of a program

Suppose that you need to give a problem specification of some problem P and you have an implementation of P, in C.

I have 2 questions:

1. Can you obtain the formal specification of the problem if you compute the invariant of the external for cycle?
2. What is the relation between the specification and the C code invariant?

unsigned int f(unsigned int x) {

Was the intended specification that retval == x+1? Or that retval > x? Or that retval > 0? We can't tell. There just isn't enough information to know. (Ignore integer overflow for the moment.)