[saithound]

To add to logicchains' answer:

Normally, you wouldn't take the function body as a formal statement, and would have a separate formal specification instead. In the example of increment, the formal specification is no simpler and no more useful than the implementation itself, but this is usually not the case.

Imagine e.g. that the following specification describes the desired behavior of a function f:

    f(x) <= √x  and  (f(x) + 1) > √x

The OS developer would write something the code below to implement this specification.

  int f(int x) {
    int r1 = 0;
    int r2 = 1;
    while (x >= r2) {
      r1++;
      r2 = r2 + r1 + r1 + 1;
    }
    return r1;
  }

Does this C implementation conform to the specification? It's not all that easy to tell. But if the program is actually correct, then Floyd-Hoare logic [1] allows you to go through the program line-by-line and produce a proof that for any integer i and variable x', the following holds:

  lemma f_implements_spec: "
    { valueOf(x') = i \<and> i > 0 }
    x' = f(x')
    { valueOf(x') <= \<sqrt>(i) \<and> valueOf(x') - 1 > \<sqrt>(i) }"

meaning that if the statement x'=f(x') is ever executed in an environment where x' has an integer value i > 0, then after this line is executed, the result stored in x' will satisfy the specification above.

[1] https://en.wikipedia.org/wiki/Hoare_logic