Convert C language code to problem specification by computing the invariant of a program
You can not reconstruct the specification from just the code.

For one thing, you don't know whether the code is correct or not. For another, there are multiple possible specifications that are all compatible with the code.

For instance, consider the following function:

unsigned int f(unsigned int x) {
    return x+1;
}


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