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

Literature.

[CL] Remark. Note that the square function

x^{2} = x \cdot x

is defined in the included module Standard.

Integer Square Root (case study). Specification:

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

Chapter. Numeric Programs.

Section. Primitive Recursion.

Square root function.

⌊ \sqrt{x} ⌋ = ?

Square root with assignments.

⌊ \sqrt{x} ⌋ = ?

Section. Course of Values Recursion.

Subsection. Course of Values Recursion with Measure.

Bottom up program for the square root function.

f (x, y) = ?

Invariant

y^{2} ≦ x \to {f (x, y)}^{2} ≦ x \land x < {(f (x, y) + 1)}^{2}

⌊ \sqrt{x} ⌋ = ?

Section. Recursion on Notation.

Subsection. $p$ -ary arithmetic.

A fast program for the square root function. (1 point)

sgn (0) = 0

sgn (x) = 1 \leftarrow x \neq 0

⌊ \sqrt{x} ⌋ = ? \leftarrow x = 4 \cdot y + z \land 0 ≦ z \land z ≦ 3