[turbinerneiter]

How does this formal specification look like?

From my naive standpoint: input, output, side-effect, time

  [no_sideffect, 1ms]
  fn increment(int i) -> int:
      return i + 1

What this is missing is a formal statement that says "increases the value of the input by one" -> except you accept the function body as formal statement.

Thanks for all the answers here, I guess I'm going to look for some more reading material.

[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

[logicchains]

Here's a specification of an increment function in Isabelle/HOL, the theorem prover used for SeL4, plus some other random lemmas about it:

    theory Scratch
      imports Main
    begin

    fun increment :: "int ⇒ int" where 
    "increment x = x + 1"

    lemma increment_increments:
      shows "increment x = x + 1"
      by simp

    lemma double_increment_adds_two:
      shows "increment (increment x) = x + 2"
      by simp

    lemma increment_sub_1_is_x:
      shows "increment x - 1 = x"
      by simp

[shawnz]

If you take the original code as the formal statement, how could it ever be wrong?