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.

Chapter. Programs Operating on Lists.

Section. Operations on Lists.

Map. Given the function $f (x)$ , define the function ${Map}_{f} (x)$ such that

L {Map}_{f} (x) = L (x)

i < L (x) \to {Map}_{f} (x) [i] = f (x [i])

Verify your implementation!

{Map}_{f} (x) = ?

L {Map}_{f} (x) = L (x)

i < L (x) \to {Map}_{f} (x) [i] = f (x [i])

List modification. Define the function $x [i ≔ a]$ such that

i < L (x) \to L (x [i ≔ a]) = L (x)

i < L (x) \to (x [i ≔ a]) [i] = a

i < L (x) \land j < L (x) \land j \neq i \to (x [i ≔ a]) [j] = x [j]

Verify your implementation!

x [i ≔ a] = ?

i < L (x) \to L (x [i ≔ a]) = L (x)

i < L (x) \to (x [i ≔ a]) [i] = a

i < L (x) \land j < L (x) \land j \neq i \to (x [i ≔ a]) [j] = x [j]

Take and drop. Define the functions $Take (n, x)$ and $Drop (n, x)$ such that

n ≦ L (x) \to L Take (n, x) = n

n ≦ L (x) \to \exists y x = Take (n, x) \oplus y

and

n ≦ L (x) \to L Drop (n, x) = L (x) \dot{-} n

n ≦ L (x) \to \exists y x = y \oplus Drop (n, x)

Verify your implementations!

Take (n, x) = ?

Drop (n, x) = ?

n ≦ L (x) \to L Take (n, x) = n

n ≦ L (x) \to \exists y x = Take (n, x) \oplus y

n ≦ L (x) \to L Drop (n, x) = L (x) \dot{-} n

n ≦ L (x) \to \exists y x = y \oplus Drop (n, x)

Zip and unzip. Define the functions $Zip (x, y)$ and $Unzip (z)$ such that

L (x) = L (y) \to L Zip (x, y) = L (x)

L (x) = L (y) \land i < L (x) \to Zip (x, y) [i] = x [i], y [i]

and

L (x) = L (y) \to Unzip Zip (x, y) = x, y

Verify your implementations!

Zip (x, y) = ?

Unzip (z) = ?

L (x) = L (y) \to L Zip (x, y) = L (x)

L (x) = L (y) \land i < L (x) \to Zip (x, y) [i] = x [i], y [i]

L (x) = L (y) \to Unzip Zip (x, y) = x, y

Interval. Define the function $[m .. n)$ such that

L ([m .. n)) = n \dot{-} m

i < n \dot{-} m \to [m .. n) [i] = m + i

Verify your implementation!

[m .. n) = ?

L ([m .. n)) = n \dot{-} m

i < n \dot{-} m \to [m .. n) [i] = m + i

Exercise. Prove

k ≦ m \land m ≦ n \to [k .. m) \oplus [m .. n) = [k .. n)

k ≦ m \land m ≦ n \to [k .. m) \oplus [m .. n) = [k .. n)

List minimum. Define the function $Minl (x)$ such that

x \neq 0 \to Minl (x) &CLin; x

x \neq 0 \land a &CLin; x \to Minl (x) ≦ a

Verify your implementations!

Minl (x) = ?

x \neq 0 \to Minl (x) &CLin; x

x \neq 0 \land a &CLin; x \to Minl (x) ≦ a

List maximum. Define the function $Maxl (x)$ such that

x \neq 0 \to Maxl (x) &CLin; x

x \neq 0 \land a &CLin; x \to a ≦ Maxl (x)

Verify your implementations!

Maxl (x) = ?

x \neq 0 \to Maxl (x) &CLin; x

x \neq 0 \land a &CLin; x \to a ≦ Maxl (x)

Deleting elements from lists. Define the function $Delall (a, x)$ such that

b &CLin; Delall (a, x) \leftrightarrow b &CLin; x \land b \neq a

Verify your implementation!

Delall (a, x) = ?

b &CLin; Delall (a, x) \leftrightarrow b &CLin; x \land b \neq a

Filter. Given the predicate $A$ , define the function ${Filter}_{A} (x)$ such that

a &CLin; {Filter}_{A} (x) \leftrightarrow a &CLin; x \land A (a)

Verify your implementation!

{Filter}_{A} (x) = ?

a &CLin; {Filter}_{A} (x) \leftrightarrow a &CLin; x \land A (a)

Multiplicity. Define the function $#_{a} (x)$ such that

#_{a} (b, 0) = (a =_{*} b)

#_{a} (x \oplus y) = #_{a} (x) + #_{a} (y)

Verify your implementation!

Remark. The $x =_{*} y$ is the characteristic function of the binary equality predicate $x = y$ and it is defined in the module Maux*.

#_{a} (x) = ?

#_{a} (b, 0) = (a =_{*} b)

#_{a} (x \oplus y) = #_{a} (x) + #_{a} (y)

List union. Define the function $⋃ x$ such that

⋃ (x, 0) = x

⋃ (x \oplus y) = ⋃ x \oplus ⋃ y

Verify your implementation!

⋃ x = ?

⋃ (x, 0) = x

⋃ (x \oplus y) = ⋃ x \oplus ⋃ y