Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)

Literature.

[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.

[CL] CL-TeX.

[CL] Remark. Note that the square function

x^{2} = x \cdot x

is defined in the included module Standard.

Section. Case Study: Integer Square Root.

Specification.

{⌊ \sqrt{x} ⌋}^{2} ≦ x \land x < {(⌊ \sqrt{x} ⌋ + 1)}^{2}

Top-down program by primitive recursion.

⌊ \sqrt{0} ⌋ = 0

⌊ \sqrt{x + 1} ⌋ = ⌊ \sqrt{x} ⌋ \leftarrow x + 1 < {(⌊ \sqrt{x} ⌋ + 1)}^{2}

⌊ \sqrt{x + 1} ⌋ = ⌊ \sqrt{x} ⌋ + 1 \leftarrow x + 1 ≧ {(⌊ \sqrt{x} ⌋ + 1)}^{2}

Exercise. Prove

{⌊ \sqrt{x} ⌋}^{2} ≦ x \land x < {(⌊ \sqrt{x} ⌋ + 1)}^{2}

{⌊ \sqrt{x} ⌋}^{2} ≦ x \land x < {(⌊ \sqrt{x} ⌋ + 1)}^{2}

Top-down program with assignment.

⌊ \sqrt{0} ⌋ = 0

⌊ \sqrt{x + 1} ⌋ = y \leftarrow ⌊ \sqrt{x} ⌋ = y \land x + 1 < {(y + 1)}^{2}

⌊ \sqrt{x + 1} ⌋ = y + 1 \leftarrow ⌊ \sqrt{x} ⌋ = y \land x + 1 ≧ {(y + 1)}^{2}

Exercise. Prove

{⌊ \sqrt{x} ⌋}^{2} ≦ x \land x < {(⌊ \sqrt{x} ⌋ + 1)}^{2}

{⌊ \sqrt{x} ⌋}^{2} ≦ x \land x < {(⌊ \sqrt{x} ⌋ + 1)}^{2}

Bottom-up program by backward recursion.

f (x, y) = y \leftarrow x < {(y + 1)}^{2}

f (x, y) = f (x, y + 1) \leftarrow x ≧ {(y + 1)}^{2}

⌊ \sqrt{x} ⌋ = f (x, 0)

Exercise. Prove

{⌊ \sqrt{x} ⌋}^{2} ≦ x \land x < {(⌊ \sqrt{x} ⌋ + 1)}^{2}

{⌊ \sqrt{x} ⌋}^{2} ≦ x \land x < {(⌊ \sqrt{x} ⌋ + 1)}^{2}

Bottom-up program with accumulator.

f (x, y, s) = y \leftarrow s + 2 \cdot y + 1 = s_{1} \land x < s_{1}

f (x, y, s) = f (x, y + 1, s_{1}) \leftarrow s + 2 \cdot y + 1 = s_{1} \land x ≧ s_{1}

⌊ \sqrt{x} ⌋ = f (x, 0, 0)

Exercise. Prove

{⌊ \sqrt{x} ⌋}^{2} ≦ x \land x < {(⌊ \sqrt{x} ⌋ + 1)}^{2}

{⌊ \sqrt{x} ⌋}^{2} ≦ x \land x < {(⌊ \sqrt{x} ⌋ + 1)}^{2}

Fast program by recursion on notation.

(x \neq_{*} y) = 1 \leftarrow x \neq y

(x \neq_{*} y) = 0 \leftarrow x = y

⌊ \sqrt{x} ⌋ = (z \neq_{*} 0) \leftarrow x = 4 \cdot y + z \land 0 ≦ z \land z ≦ 3 \land y = 0

⌊ \sqrt{x} ⌋ = r \leftarrow x = 4 \cdot y + z \land 0 ≦ z \land z ≦ 3 \land y \neq 0 \land 2 \cdot ⌊ \sqrt{y} ⌋ = r \land x < {(r + 1)}^{2}

⌊ \sqrt{x} ⌋ = r + 1 \leftarrow x = 4 \cdot y + z \land 0 ≦ z \land z ≦ 3 \land y \neq 0 \land 2 \cdot ⌊ \sqrt{y} ⌋ = r \land x ≧ {(r + 1)}^{2}

Exercise. Prove

{⌊ \sqrt{x} ⌋}^{2} ≦ x \land x < {(⌊ \sqrt{x} ⌋ + 1)}^{2}

[CL] Hint. Prove the property by complete induction. In the induction step, start by using the following theorem

\exists y \exists z (x = 4 \cdot y + z \land z < 4)

from the module Maux*.

{⌊ \sqrt{x} ⌋}^{2} ≦ x \land x < {(⌊ \sqrt{x} ⌋ + 1)}^{2}