0
$\begingroup$

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?
Improve this question
$\endgroup$
0

1 Answer 1

Reset to default
3
$\begingroup$

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 > x? Or that retval > 0? We can't tell. There just isn't enough information to know. (Ignore integer overflow for the moment.)

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.