Задача 1. Написать блок-схему, которая является обще полностью корректной относительно спецификации \((\varphi,~\psi)\) при заданной \(\gamma\), и доказать это. Блок-схема имеет три входные переменные \(x_1, x_2, x_3\) и одну выходную переменную \(z_1\). Домен переменных \(x_1\) и \(z_1\) обозначим как \(M\), домен переменных \(x_2\) и \(x_3\) обозначим как \(A\). Элементы множества \(M\) можно сравнивать на равенство, то же справедливо для множества \(A\). Других операций для этих множеств не определено.
Обратите внимание на то, что в спецификациях используются функциональные и предикатные символы и наборы аксиом. Это означает, что эти символы нельзя использовать для определения вычисления и, поэтому, нельзя использовать в качестве функций, приписанных операторам блок-схемы.
Функциональные и предикатные символы:
\(select: M \times A \rightarrow V\)
\(store: M \times A \times V \rightarrow M\)
\(valid: M \times A \rightarrow \{T, F\}\)
Элементы множества \(V\) можно сравнивать на равенство, других операций для этого множества не определено.
Аксиомы над указанными символами:
\(Ax1: \forall m \in M, a \in A, v \in V \cdot valid(m, a) \Rightarrow select(store(m, a, v), a) = v\)
\(Ax2: \forall m \in M, a, b \in A, v \in V \cdot valid(m, a) \land valid(m, b) \land a \neq b \\ \Rightarrow select(store(m, a, v), b) = select(m, b)\)
\(Ax3: \forall m \in M, a, b \in A, v \in V \cdot valid(m, a) \land valid(m, b) \\ \Rightarrow valid(store(m, a, v), b)\)
\(\varphi(x_1, x_2, x_3) \equiv valid(x_1, x_2) \land valid(x_1, x_3)\)
\(\psi(x_1, x_2, x_3, z_1) \equiv valid(z_1, x_2) \land valid(z_1, x_3) \\
\land select(z_1, x_2) = select(x_1, x_3) \land select(z_1, x_3) = select(x_1, x_2) \\ \land \forall x \in A \cdot x \neq x_2 \land x \neq x_3 \land valid(z_1, x) \land valid(x_1, x) \Rightarrow select(z_1, x) = select(x_1, x)\)
Сигнатуры для операторов CALL и их спецификации:
- \((DEREF, M \times A, V)\)
- \(\varphi_{DEREF}(m, a) \equiv valid(m, a)\)
- \(\psi_{DEREF}(m, a, v) \equiv v = select(m, a)\)
- \((SETREF, M \times A \times V, M)\)
- \(\varphi_{SETREF}(m, a, v) \equiv valid(m, a)\)
- \(\psi_{SETREF}(m, a, v, m’) \equiv m’ = store(m, a, v)\)