2-formal.tex

Модели сценариев, согласно предложенному методу, можно описывать на языке программирования Си, но для описания действий посылки и получения сигналов предлагается расширить язык Си вспомогательными операциями для удобства спецификации.
Поэтому промежуточные модели окружения должны быть предварительно транслированы на язык программирования Си. 
Тогда нужно показать, что трансляция промежуточной модели окружения не влияет на возможность обнаружения ошибок в модуле.

Модель окружения на языке программирования Си анализируется в рамках верификационной задачи инструментом верификации моделей программ при проверке некоторого свойства корректности.
Под программой далее будем понимать именно совокупность исходного кода модели окружения и модуля программы.
По исходному Си-программы строится модель, которая проверяется на соответствие свойству недостижимости ошибочных состояний\footnote{В данной работе рассматриваются только такие свойства корректности, которые могут быть сведены к задаче недостижимости ошибочного оператора.} методом верификации моделей.
Покажем, что множества ошибочных состояний исходной программы и программы, полученной после трансляции исходной программы на язык Си, изоморфны.
Для этого необходимо рассмотреть свойства таких моделей рассматриваемых программ, которые используются инструментами верификации моделей при проверке свойств недостижимости ошибочного оператора.

\subsubsection{Символическая система переходов}

Для описания моделей программ воспользуемся символическими системами переходов (англ. symbolic transition system)~\cite{Clarke:1981}.
Система определяется тройкой $STS \mathbf{:=} <V, \alpha, \delta>$. Где $V$ --- конечное множество типизированных переменных системы, каждая из которых задана на дискретном конечном множестве значений.
Функция означивания $s \in \Sigma_V$ переменных из множества $V$ называется состоянием системы. Множество $\Sigma_V$ --- это множество состояний системы, полученное перебором всех возможных значений переменных из множества $V$.
Формула пропозициональной логики $\alpha(V)$ над переменными из множества $V$ называется \textit{характеристической функцией множества начальных состояний}.
Состояния, при которых данный предикат принимает истинное значение, называются \textit{начальными состояниями}.
Формула пропозициональной логики $\delta(V, V^{'})$ --- это \textit{характеристическая функция отношения переходов} между состояниями.
Функция определена над переменными из $V \cup V^{'}$, то есть переменными в данном и в следующем состояниях системы.
Если для двух состояний $s_1 \in \Sigma_V$ и $s_2 \in \Sigma_V$ выполняется $(s_1, s_2) \models \delta$, то между ними возможен переход.

\textit{Путь} --- это конечная последовательность $\xi_k = s^0, s^1, ..., s^k$ состояний \break $s^{i} \in \Sigma_{V}$, в которой для каждого состояния справедливо $(s^{i}, s^{i+1}) \models \delta$ и для начального состояния $s^1 \models \alpha$. 
\textit{Предикат пути} длины $k$ шагов имеет вид:

\[
\eta_k \mathbf{:=} \alpha(V^{1}) \land \bigwedge_{i \in [1,k]}\delta[V = V^{i}, V^{'} = V^{i+1}](V, V^{'})
\]

$V^{i}$ обозначает множество переменных системы на шаге выполнения $i$.
Будем говорить, что состояние $s^k \in \Sigma_{V}$ достижимо за $k$ шагов, если существует такой путь выполнения $\xi_k = {s^1, s^2, ... s^k}$, что $\xi_k \models \eta_k$.
Обозначим множество всех достижимых за $k$ шагов состояний как $R_k$, а множество всех достижимых состояний как $R$.

Рассмотрим некоторое подмножество переменных системы $U \subseteq V$.
Проекцией состояния $s \in \Sigma_{V}$ на множество переменных $U$ называется такая функция означивания переменных $U$, обозначаемая как $s \Downarrow U$, которая переменным из $U$ ставит в соответствие те же значения, что и $s$.
Проекцией $K \Downarrow U$ некоторого подмножества всех состояний системы $K \subseteq \Sigma_V$ на множество переменных $U$ назовем множество всех проекций состояний из $K$ на множество переменных $U$.


\subsubsection{Символическая система переходов и структуры Крипке}
Каждый способ моделирования систем <<фиксирует>> свой набор свойств системы.
Метод описания систем при помощи структур Крипке широко распространен и применяется в том числе и для проверки свойства недостижимости ошибочных состояний.
Метод моделирования систем при помощи систем символических переходов не уступает в выразительности структурам Крипке.

Построим следующую структуру Крипке про произвольной $STS$:
\[K \mathbf{:=} <S, S_0, R, L>\]

\begin{itemize}
    \item $S = \Sigma_V$ --- конечное множество абстрактных состояний, полученное путем рассмотрения всех значений переменных $V$.
    \item $S_0 = \{s \in S| s \models \alpha\}$ --- множество начальных состояний, удовлетворяющих характеристической функции $\alpha$.
    \item $R = \{(s, t)| (s, t) \models \delta\}$ --- отношение переходов, которое определяется определяется характеристической функцией $\delta$.
    \item $L(s)$ --- такая функция разметки, которая ставит в соответствие состоянию набор истинных предикатов из $AP = \{a_1, ..., a_k\}$, определенных на множестве переменных $V$. То есть $a_i \in L(s)$, если $s \models a_i$.
\end{itemize}

В построенной структуре Крипке $K$ и в $STS$ множества всех состояний системы, начальных состояний и переходов попарно совпадают.
То есть для любой символической системы переходов может быть построена эквивалентная структура Крипке.

\subsubsection{Язык программирования $LZ$}

Расширения языка Си для отправки и получения сигналов влияют на порядок выполнения операций в программе и передачу данных между потоками.
Предположим, что и при трансляции новых операций на язык Си будут использоваться некоторые только операции с целыми числами, захват и освобождение блокировок, проверка простых логических выражений.
При посылке и получении сигналов, а также при трансляции данных операций на язык Си, не предполагается использовать вызовы произвольных функций, циклы с переменным числом итераций, рекурсию, изменять значения по указателям, выделять или освобождать память, создавать или останавливать потоки, выполнять переходы по goto и т.п.
Поэтому при рассмотрении программ и их моделей целесообразно рассмотреть упрощенный Си-подобный язык, который сохранит именно те особенности семантики программ на языке Си, на которые влияет добавление операций посылки и получения сигналов.
Таким языком станет некоторый структурный статически типизированный язык программирования $LZ$.

Программа на языке $LZ$ имеет следующий синтаксис:
\begin{flalign*}
& Globals:~g_1:~\tau_1;~g_2:~\tau_2;~...~g_n:~\tau_n;\\
& Procedures: \\
& ~~~Procedure~1:\\
& ~~~~~~Locals:~v_1:~\tau_1;~v_2:~\tau_2;~...~v_{k_1}:~\tau_{k_1}; \\
& ~~~~~~P_1; \\
\\
& ~~~Procedure~2:\\
& ~~~~~~Locals:~v_2:~\tau_1;~v_2:~\tau_2;~...~v_{k_2}:~\tau_{k_2}; \\
& ~~~~~~P_2; \\
& ~~~... \\
& ~~~Procedure~N:\\
& ~~~~~~Locals:~v_2:~\tau_1;~v_2:~\tau_2;~...~v_{k_N}:~\tau_{k_N}; \\
& ~~~~~~P_N; \\
\end{flalign*}

Здесь использовались следующие обозначения:
\begin{itemize}
    \item $g_i$ --- глобальные переменные программы с типами $\tau_i$. Множества значений типов $\{int, lock, bool\}$ являются конечными и дискретными. Тип $int$ соответствует подмножеству целых чисел, $bool$ соответствует истинностным значениям, множество значений типа $lock$ содержит два элемента: 0 (блокировка не захвачена) и 1 (блокировка захвачена). \item $Procedure~i$ --- заголовок описания процедуры с номером $i$, которое состоит из деклараций локальных переменных $v_i$ и кода $P_i$ процедуры.
\end{itemize}

Выполнение программы представляет собой параллельное выполнение операций из процедур программы в отдельных потоках. 
Каждый $i$-ый поток выполняет соответствующую ему процедуру $P_i$.
Потоков в программе всегда не менее 1 и все они начинают выполнение одновременно.
Порядок выполнения операций одной процедуры определяется операторами следования ($;$), ветвления ($if$) и цикла ($while$).

Грамматика кода процедуры $P_i$ имеет вид:
\begin{flalign*}
P \mathbf{:=} &~P;P~|~if~(A)~\{P\}~else~\{P\}~|~while~(A)~\{P\}~|~op~|~skip \\
op \mathbf{:=} &~x = t~|~lock(x)~|~unlock(x)~|~assume(A) \\
t \mathbf{:=} &~(t)~|~t - t~|~x~|~t + t \\
A \mathbf{:=} &~\neg A~|~A \land A~|~A \lor A~|~A \to A~|~(A)~|~x~|~nondet()
\end{flalign*}

Рассмотрим каждый символ подробнее:
\begin{itemize}
    \item $op$ --- операция в программе. Операциями являются $lock$, $unlock$, $assume$, $skip$ и присваивание.
    \item t --- выражение, составленное при помощи арифметических операторов \{+, -\} над переменными программы с типом $int$. Выражения используются только в операциях присваивания.
    \item x --- имя некоторой переменной. В любой процедуре может выполняться доступ к глобальным переменных и локальным переменным данной процедуры. Локальные переменные могут иметь только типы $int$ и $bool$.
    \item $lock(x)$ и $unlock(x)$ --- функции захвата и освобождения блокировки $x$. Блокировками являются глобальные переменные с типом $lock$.
    \item nondet() --- неопределенное значение из множества значений типа $bool$;
    \item $A$ --- логическая формула пропозициональной логики, расширенная теорией целых чисел. Формула может быть составлена при помощи логических связок $\{!, \&\&, ||, ==\}$ над переменными программы;
    \item $assume(A)$ --- проверка выполнения формулы $A$. Если формула не истинна, то процедура не может продолжить выполнение и перейти к следующей операции.
    \item $skip$ --- операция бездействия.
\end{itemize}

\subsubsection{Модель программ на языке программирования $LZ$}
Построим модель программы $P$ на языке $LZ$ при помощи символической системы переходов $STS \mathbf{:=} (V_P, \alpha_P, \delta_P)$.

В каждой процедуре пронумеруем каждую операцию и проверку условий циклов и операторов ветвления.
В результате каждая операция и условие операторов цикла или ветвления будут иметь свой уникальный порядковый номер, называемый \textit{меткой}.
Дополнительной меткой обозначим конец каждой процедуры.

Введем следующие обозначения:
\begin{itemize}
    \item $V_P = V \cup PC$--- множество переменных состояния.
    \item $\Sigma_{V_P}$ --- множество всех состояний модели программы.
    \item $V = G \cup L_0 \cup ... \cup L_N$ --- множество переменных.
    \item $G$ --- множество глобальных переменных программы.
    \item $L_i$ --- множество локальных переменных процедуры с номером $i$. 
    $V_i = G \cup L_i$ --- множество переменных процедуры $i$.
    \item Переменные $pc_i$ (англ. program counter) являются вспомогательными и предназначены для сохранения метки текущей выполняемой операции или проверяемого условия оператора. Множество таких переменных обозначим как $PC = \{pc_1, ... , pc_N\}$. 
    Элементы множества $C \subset \Sigma_{PC}$ всех допустимых функций означивания переменных $PC$ будем называть конфигурациями, а $\Sigma_{PC}$ множеством конфигураций.
    \item $\alpha_{P}(V_P)$ --- характеристическая функция начальных состояний.
    \item $\delta_{P}(V_{P}, V^{'}_{P})$ --- характеристическая функция отношения переходов.
\end{itemize}
 
Выполнение программы будем моделировать как асинхронную параллельную композицию потоков.
Характеристическая функция отношения переходов имеет вид:

\begin{flalign*}
& \delta_P(V_P, V^{'}_P) \mathbf{:=} \bigvee_{i \in [1,N]}(\delta_{i}(V_i, pc_i, V^{'}_i, pc_i^{'}) \land \sigma_i)\text{, где}  
\\
& \sigma_i \mathbf{:=} \bigwedge_{\substack{j \in [1,N],\\j \neq i}}same(\{pc_j\}\cup L_j)
\end{flalign*}

Здесь предикат $same(A)$ означает, что переменные из некоторого подмножества переменных состояния $A \subset V_P$ сохраняют свои значения:

\[same(A) \mathbf{=} \bigwedge_{x \in A}x^{'} = x\]

\textit{Характеристическая функция процедуры} $\delta_{i}(V_i, pc_i, V_i^{'}, pc_i^{'})$ моделирует выполнение отдельного потока с номером $i$.
Пусть поток выполняет процедуру $P_i$, в которой $k_i$ меток, тогда: 

\begin{align*}
\delta_{i}(V_i, pc_i, V^{'}_i, pc_i^{'}) \mathbf{:=} \bigvee_{l \in [1,k_i]}\delta_{op_l}(V_i, pc_i, V^{'}_i, pc_i^{'})
\end{align*}

Где $\delta_{op_l}$ --- \textit{характеристическая функция операции или оператора с меткой $l$}.
Пусть операция имеет метку $l_1$, а метка следующей выполняемой операции или условия оператора будет $l_2$.
Тогда характеристическая функция операции в позиции $l_1$ имеет вид:

\begin{align*}
\delta_{op_{l_1}}(V_i, pc_i, V'_i, pc'_i) \mathbf{:=} pc_i = l_1 \land pc'_i = l_2 \land \rho_{op}(V_i, V'_i)
\end{align*}

Здесь $\rho_{op}(V_i, V'_i)$ --- \textit{характеристическая функция операции}, которая не зависит от метки.
Характеристические функции операций языка представлены в таблице~\ref{table:predicate}.
 
Рассмотрим проверку условия $A(V_i)$ оператора ветвления или цикла с меткой $l_1$.
Если условие истинно, то выполнеются операция с меткой $l_{true}$, а иначе операция с меткой $l_{false}$.
Тогда характеристическая функция условия оператора с меткой $l_1$ имеет вид:

\begin{align*}
\delta_{op_{l_1}}(V_i, pc_i, V'_i, pc'_i) \mathbf{:=} & pc_i = l_1 \land same(V_i) \land \\
& (A(V_i) \land pc' = l_{true} \lor \neg A(V_i) \land pc' = l_{false})
\end{align*}

\begin{table}
\centering
\begin{tabular}{ | l | l |}
\hline
Операция & Характеристическая функция \\
\hline
$lock(x)$ & $\rho_{op}(V_i, V'_i) \mathbf{:=} x = 0 \land x' = 1 \land same(V_i \setminus \{x\}))$ \\
\hline
$unlock(x)$ & $\rho_{op}(V_i, V'_i) \mathbf{:=} x' = 0 \land same(V_i \setminus \{x\})$ \\
\hline
$x = t(V_i)$ & $\rho_{op}(V_i, V'_i) \mathbf{:=} x' = t(V_i) \land same(V_i \setminus \{x\})$ \\
\hline
$assume(A(V_i))$ & $\rho_{op}(V_i, V'_i) \mathbf{:=} A(V_i) \land same(V_i)$ \\
\hline
$skip$ & $\rho_{op}(V_i, V'_i) \mathbf{:=} same(V_i)$ \\
\hline
\end{tabular}
\caption{Характеристические функции операций языка $LZ$.}
\label{table:predicate}
\end{table}

Пусть в процедуре $i$ есть некоторый блок кода, состоящий из нескольких операций.
Первая операция блока всегда имеет \textit{метку входа в блок}, а \textit{метку выхода из блока} имеет следующий оператор после последнего оператора блока.
Здесь и далее блок кода всегда имеет только одну \textit{метку входа в блок} и одну \textit{метку выхода из блока}.
Пусть блок имеет метку входа $l_1$ и метку выхода из блока $l_2$.
\textit{Предикат пути через блок} имеет вид:

\begin{flalign*} 
\pi \mathbf{:=} pc^{1}_{i} = l_1 \land pc^{k+1}_{i} = l_2 \land \bigwedge_{i \in [1,k]}\delta_{P}[V_P = V^{i}_{P}, V^{'}_P = V^{i+1}_{P}](V_{P}, V^{'}_{P})
\end{flalign*}

Предикат $\Delta_k = \bigwedge_{i \in [1,k]}\delta_{P}[V_P = V^{i}_{P}, V^{'}_P = V^{i+1}_{P}](V_{P}, V^{'}_{P})$ будем называть \textit{предикатом шагов} и для краткости записывать как $\Delta_k = \bigwedge_{i \in [1,k]}\delta_{P}(V^{i}_{P}, V^{i+1}_{P})$.
Другую часть предиката пути назовем \textit{предикатом граничных условий} и обозначим $\gamma = pc^{1}_{i} = l_1 \land pc^{k+1}_{i} = l_2$.

Предикат моделирует путь длины $k$ шагов из состояния $s^1$, которое является функцией означивания переменных состояния $V^1_P$ на первом шаге, в состояние $s^{k+1}$, которое является функцией означивания переменных состояния $V^{k+1}_P$ после выполнения шага $k$.
Состояние $s^1$ будем называть \textit{входным}, а состояние $s^{k+1}$ \textit{выходным}.
Если существует такая конечная последовательность состояний $s^0, s^1, ..., s^k$, что предикат принимает истинное значение, то будем говорить, что состояние $s^{k+1}$ достижимо из состояния $s^{1}$ и обозначим этот факт как $(s^1, s^{k+1}) \models \pi$.

Рассмотрим блоки с предикатами пути $\pi_1$ и $\pi_2$ из разных программ с множествами состояний $\Sigma_{V_{P_1}}$ и $\Sigma_{V_{P_2}}$ соответственно.
Пусть программы имеют общее непустое множество переменных $U$, значения которых определяют ошибочные состояния.
Тогда блоки считаются эквивалентными относительно $U$, если для любых входного и достижимого выходного состояний $x_1$ и $y_1$ найдется путь через второй блок из состояния $x_2$ в $y_2$, у которых соответствующие проекции на множество переменных $U$ попарно совпадают с $x_1$ и $y_1$.
И выполняется условие, что второй блок не добавляет новых достижимых состояний с другими проекциями на множество $U$, которых в первом блоке быть не могло.

Условие эквивалентности блоков относительно множества переменных $U$ имеет вид:
\begin{enumerate}
    \item Для любого такого входного и выходного состояний $\{x_1$, $y_1\} \subset \Sigma_{V_{P_1}}$, что $(x_1, y_1) \models \pi_1$, найдутся такие входное и выходное состояния $\{x_2, y_2\} \subset \Sigma_{V_{P_2}}$ и $(x_2, y_2) \models \pi_2$, что $x_1 \Downarrow U = x_2 \Downarrow  U$ и $y_1 \Downarrow U = y_2 \Downarrow  U$.
    \item Для любого такого входного и выходного состояния $\{x_2, y_2\} \subset \Sigma_{V_{P_2}}$, что $(x_2, y_2) \models \pi_2$, найдутся входное и выходное состояния $\{x_1$, $y_1\} \subset \Sigma_{V_{P_1}}$ и $(x_1, y_1) \models \pi_1$, что $x_1 \Downarrow U = x_2 \Downarrow  U$ и $y_1 \Downarrow U = y_2 \Downarrow  U$.
\end{enumerate}

Рассмотрим случай последовательного выполнения двух некоторых операций с характеристическими функциями $\rho_1(x, x^{'})$ и $\rho_2(x, x^{'})$.
Операции имеют метки $1$ и $2$ соответственно, а после следует операция с меткой 3.
Путь через такой блок всегда имеет длину 2 шага и предикат пути имеет вид:
\begin{flalign*}
\pi\mathbf{:=} 
& pc^1 = 1 \land pc^3 = 3 ~\land \\
& (pc^1 = 1 \land \rho_1(V^1_i, V^2_i) \land pc^2 = 2 ~\lor \\ 
& ~pc^1 = 2 \land \rho_2(V^1_i, V^2_i) \land pc^2 = 3) ~\land \\
& (pc^2 = 1 \land \rho_1(V^2_i, V^3_i) \land pc^3 = 2) ~\lor \\ 
& ~pc^2 = 2 \land \rho_2(V^2_i, V^3_i) \land pc^3 = 3) \Leftrightarrow \\ 
& pc^1 = 1 \land pc^3 = 3 \land \rho_1(V^1_i, V^2_i) \land \rho_2(V^2_i, V^3_i) \end{flalign*}

Данный результат иллюстрирует возможность сокращенной записи предиката последовательного выполнения пути через блок.
Такой путь можно рассматривать как выполнение некоторой искусственной операции с характеристической функцией $\rho_{op}(V_i, V'_i) = \rho_1(V_i, V_t) \land \rho_2(V_t, V'_i)$, где $V_t$ --- вспомогательный набор переменных.
Такую функцию назовём \textit{предикатом блока}.
Предикат блока из $k$ последовательных операций имеет вид $V_i=V^{1}_i \land V^{'}_i = V^{k+1}_i \land \bigwedge{j \in [1,k]}\rho_i(V^j_i, V^{j+1}_i)$.

Рассмотрим оператор ветвления с условием $\phi(V_i)$ и ветвями, в которых выполняются блоки кода с предикатами $\rho_{then}$ и $\rho_{else}$ и метками $1$ и $2$. 
Метка выхода из блока пусть равна $4$.
Тогда предикат пути через блок с оператором ветвления имеет вид:
\begin{flalign*}
\pi \mathbf{:=} & pc^1 = 1 \land pc^3 = 4 ~\land \\
& (pc^1 = 1 \land ( \phi(V^1_i) \land pc^2 = 2 \lor \neg \phi(V^1_i) \land pc^2 = 3) \land V^2_i = V^1_i ~\lor \\ 
& ~pc^1 = 2 \land \rho_{then}(V^1_i, V^2_i) \land pc^2 = 4 \lor \\ &
~pc^1 = 3 \land \rho_{else}(V^1_i, V^2_i) \land pc^2 = 4) \land \\ &
(pc^2 = 1 \land (\phi(V^2_i) \land pc^3 = 2 \lor \neg \phi(V^2_i) \land pc^3 = 3) \land V^3_i = V^2_i \lor \\ &
~pc^2 = 2 \land \rho_{then}(V^2_i, V^3_i) \land pc^3 = 4 \lor \\ &
~pc^2 = 3 \land \rho_{else}(V^2_i, V^3_i) \land pc^3 = 4) \Leftrightarrow \\ &
pc^1 = 1 \land pc^3 = 4 \land V^2_i=V^1_i \land \\ &
(pc^2 = 2 \land \phi(V^1_i) \land \rho_{then}(V^1_i, V^3_i) \lor pc^2 = 3 \land \neg \phi(V^1_i) \land \rho_{else}(V^1_i, V^3_i))
\end{flalign*}

Предикат пути через блок с ветвлением можно рассматривать как выполнение за один шаг искусственной операции с характеристической функцией $\rho_{op}(V_i, V'_i) = \phi(V_i) \land \rho_{then}(V_i, V'_i) \lor \neg \phi(V_i) \land \rho_{else}(V_i, V'_i)$.
Такую функцию также будем называть предикатом блока.

Предикат последовательного пути через любой блок с операторами ветвления и следования можно представить в виде выполнения за один шаг искусственной операции с предикатом пути, построенным на основе правил, проиллюстрированных для отдельных двух операций и оператора ветвления.

Назовем операции \textit{независимыми}, если для их характеристических функций $\rho_1(V_i, V'_i)$ и $\rho_2(V_i, V'_i)$  справедливо условие: 

\begin{flalign*}
\rho_1(V^1_i, V^2_i) \land \rho_2(V^2_j, V^3_j) \Leftrightarrow \rho_2(V^1_j, V^2_j) \land \rho_1(V^2_i, V^3_i).
\end{flalign*}

Примером независимых операций являются операции над локальными переменными из разных потоков или операции, в результате которых изменяемая глобальная переменная имеет одно и то же значение.

\begin{lemma}
\label{interleaving}
Истинность предиката пути, на котором могут выполняться подряд две независимые операции не зависит от порядка выполнения данных операций между собой.
\end{lemma}
\begin{proof}
Утверждение тривиально выполняется для последовательного случая, если рассмотреть предикат блока из двух независимых операций:

\begin{flalign*}
\rho(V_i, V'_i) = & \rho_1(V_i, V_t) \land \rho_2(V_t, V'_i) \Leftrightarrow \rho_2(V_i, V_t) \land \rho_1(V_t, V'_i)
\end{flalign*}

Теперь рассмотрим два потока, в которых выполняются независимые операции c характеристическими функциями $\rho_1(V_1, V'_1)$ и $\rho_2(V_2, V'_2)$ соответственно.
Пусть обе операции имеют метку 1 в соответствующих процедурах, после которой следует метка 2.
Тогда предикат пути через блок имеет вид:

\begin{flalign*}
\pi \mathbf{:=} & pc^{1}_1 = 1 \land pc^{1}_2 = 1 \land pc^{3}_1 = 2 \land pc^{3}_2 = 2 \land \\ 
& (pc^{1}_1 = 1 \land \rho_1(V^{1}_1, V^{2}_1) \land pc^{2}_1 = 2 \land pc^{2}_2 = pc^{1}_2 \land same(V^1 \setminus V^1_1) \lor \\ 
& ~pc^{1}_2 = 1 \land \rho_2(V^{1}_2, V^{2}_2) \land pc^{2}_2 = 2 \land pc^{2}_1 = pc^{1}_1 \land same(V^1 \setminus V^1_2)) \land \\ 
& (pc^{2}_1 = 1 \land \rho_1(V^{2}_1, V^{3}_1) \land pc^{3}_1 = 2 \land pc^{3}_2 = pc^{2}_2 \land same(V^2 \setminus V^2_1) \lor \\ 
& ~pc^{2}_2 = 1 \land \rho_2(V^2_2, V^3_2) \land pc^{3}_2 = 2 \land pc^{3}_1 = pc^{2}_1 \land same(V^2 \setminus V^2_2)) \Leftrightarrow \\ 
& pc^{1}_1 = 1 \land pc^{1}_2 = 1 \land pc^{3}_1 = 2 \land pc^{3}_2 = 2 \land \\ 
& (\rho_1(V^1_1, V^2_1) \land \rho_2(V^2_2, V^3_2) \land pc^{2}_1 = 2 \land pc^{2}_2 = 1 \land \\
& ~same(V^1 \setminus V^1_1) \land same(V^2 \setminus V^2_2) ~\lor \\ 
& ~\rho_2(V^{1}_2, V^{2}_2) \land \rho_1(V^{2}_1, V^{3}_1) \land pc^{2}_1 = 1 \land pc^{2}_2 = 2 \land \\ 
& ~same(V^1 \setminus V^1_2) \land same(V^2 \setminus V^2_1))
\end{flalign*}

В силу определения независимых операций, если предикат $\rho_1(V^1_1, V^2_1) \land \rho_2(V^2_2, V^3_2)$ принимает истинное или ложное значение, то такое же значение принимает и предикат $\rho_2(V^{1}_2, V^{2}_2) \land \rho_1(V^{2}_1, V^{3}_1)$.
\end{proof}

Следствием данной леммы является возможность записывать предикат пути в сокращенном виде, не рассматривая все варианты чередований выполнения независимых операций.
Если независимых операций больше двух, то попарно можно <<переставлять>> и большее число операций.
На основе данной леммы может быть доказано следующее свойство.

\begin{lemma}
\label{indep}
На эквивалентность блоков не влияют независимые операции выполняемые параллельно в других процедурах.
\end{lemma}
\begin{proof}
Рассмотрим программу с N процедурами.
Пусть характеристическая функция первой процедуры $\delta_1(V_i, pc_1, V'_i, pc'_i)$.
Данная процедура выполняет блок с метками входа $l_1$ и выхода $l_2$.
Параллельно выполняются другие процедуры с предикатами $\delta_{j}(V_j, pc_j, V'_j, pc'_j)$.
Все процедуры со второй по N-ую содержат операции независимые операциям первой процедуры.
Тогда предикат пути через первую процедуру имеет вид

\begin{flalign*}
\pi \mathbf{:=}
& pc^{1}_{1} = l_1 \land pc^{k+1}_{1} = l_2 \land \\
&\bigwedge_{i \in [1,k]}(\bigvee_{j \in [2,N]}(\delta_j(V^i_j, pc^i_j, V^{i+1}_j, pc^{i+1}_j) \land \sigma_j) \lor  (\delta_1(V^i_1, pc^i_1, V^{i+1}_1, pc^{i+1}_1) \land \sigma_1)
\end{flalign*}

Как было показано в лемме \ref{interleaving}, порядок выполнения независимых операций не влияет на истинность предиката пути.
Тогда достаточно рассмотреть случай, когда с $1$-ого по $p$-ый шаг выполняются операции первой процедуры, а с $p+1$-го по $k$-ый шаг остальная программа.

\begin{flalign*}
\pi \mathbf{:=}
& pc^{1}_{1} = l_1 \land pc^{p+1}_{1} = l_2 \land \\
& \bigwedge_{i \in [1,p]}(\delta_1(V^i_1, pc^i_1, V^{i+1}_1, pc^{i+1}_1) \land \bigwedge_{j \in [2,N]}same(\{pc^i_j\} \cup V^i_j)) \land \\
& \bigwedge_{i \in [p+1,k]}\bigvee_{j \in [2,N]}(\delta_j(V^i_j, pc^i_j, V^{i+1}_j, pc^{i+1}_j) \land \bigwedge_{\substack{j \in [1,N],\\j \neq i}}same(\{pc^i_j\} \cup V^i_j)) \Leftrightarrow \\
& \gamma \land \Delta_p \land \zeta
\end{flalign*}

В предикате выше $\pi_{seq1} = \gamma \land \Delta_p$ соответствует предикату пути последовательного выполнения операций первой процедуры, где $gamma$ --- предикат граничных условий, а $\Delta_p$ --- предикат шагов с 1-ого по $p$-ый.
А $\zeta$ описывает все возможные пути дальнейшего выполнения.
Если требуется доказать эквивалентность блока первой процедуры некоторому другому блоку, то его предикат пути можно выписать точно так же с предикатом последовательного выполнения $\pi_{seq2}$.
Тогда для доказательства эквивалентности достаточно доказать требуемое определением условие относительно предикатов путей $\pi_{seq1}$ и $\pi_{seq2}$.
\end{proof}

Далее покажем, что модель операций захвата и освобождения блокировок адекватна и решает задачу синхронизации потоков.

\begin{lemma}
\label{locks}
Предикат пути через блоки кода с захваченной блокировкой принимает истинное значение только в том случае, если на этом пути операции между метками входа и выхода каждого блока под блокировкой может одновременно выполнять только один поток.
\end{lemma}
\begin{proof}
Рассмотрим N потоков, каждый из которых захватывает блокировку, освобождает блокировку и находится затем в бездействии.
Для простоты будем считать, что в программе нет других переменных.
Характеристическая функция каждого потока имеет вид:

\begin{flalign*}
\begin{array}{lll}
\delta_{i}(A, pc_i, A', pc'_i) \mathbf{:=}
& pc_i = 1 \land A = 0 \land A' = 1 \land pc'_i = 2 ~\lor \\
& pc_i = 2 \land A' = 0 \land pc'_i = 3 ~\lor \\
& pc_i = 3 \land A' = A \land pc'_i = 3 
\end{array}
\end{flalign*}

Предикат пути через все блоки процедур имеет вид:
\begin{flalign*}
\pi(P) \mathbf{:=} & A^{0} = 0 \land \bigwedge_{i \in [1,N]}pc^{1}_i = 1 \land \\ & \bigwedge_{i \in [1,P]} \bigvee_{j \in [1,N]}(\delta_{j}(A^{i}, pc^{i}_i, A^{i+1}, pc^{i+1}_i) \land \bigwedge_{\substack{k \in [1,N],\\k \neq j}}pc^{i+1}_k = pc^{i}_k)  
\end{flalign*}
Покажем, что для любой длины пути P и числа потоков N для любого истинного значения предиката пути выполняется требуемое леммой условие:
\begin{flalign*}
\lambda(P) = \bigwedge_{i \in [1,P]}\bigwedge_{j \in [1,N]}(pc^{i}_j = 2 \to \bigwedge_{\substack{k \in [1,N],\\k \neq j}}\neg(pc^{i}_k = 2))
\end{flalign*}

Выполним доказательство по индукции.
Пусть длина пути P = 1, тогда:
\begin{flalign*}
\pi(1) \mathbf{:=} & A^{1} = 0 \land \bigwedge_{i \in [1,N]}pc^{1}_i = 1 \land \\ &
\begin{array}{lll}
\bigvee_{j \in [1,N]}(
(& pc^1_j = 1 \land A^1 = 0 \land A^{2} = 1 \land pc^{2}_j = 2 ~\lor \\
& pc^1_j = 2 \land A^{2} = 0 \land pc^{2}_j = 3 ~\lor \\
& pc^1_j = 3 \land A^2 = A^1 \land pc^{2}_j = pc^1_j) 
\land \bigwedge_{\substack{k \in [1,N],\\k \neq j}}pc^{2}_k = pc^{1}_k) \Leftrightarrow \end{array}  \\ &
A^{1} = 0 \land A^{2} = 1 \land \bigwedge_{i \in [1,N]}pc^{1}_i = 1 \land 
\bigvee_{j \in [1,N]}
(pc^{2}_j = 2 \land
\bigwedge_{\substack{k \in [1,N],\\k \neq j}}pc^{2}_k = pc^{1}_k)
\Leftrightarrow \\ &
A^1 = 0 \land A^2 = 1 \land \bigwedge_{i \in [1,N]}pc^{1}_i = 1 \land 
\bigvee_{j \in [1,N]}
(pc^{2}_i = 2 \land
\bigwedge_{\substack{k \in [1,N],\\k \neq j}}pc^{2}_k = 1))
\end{flalign*}
В то же время:
\begin{flalign*}
\lambda(1) \mathbf{:=} \bigwedge_{j \in [1,N]}(pc^{1}_j = 2 \to \bigwedge_{\substack{k \in [1,N],\\k \neq j}}\neg(pc^{1}_k = 2))
\end{flalign*}
Из предикатов видно, что $\pi(1) \to \lambda(1)$, так как за один шаг только один поток перейдет к метке 2.

Пусть тогда для длины пути $P=t$ справедливо $\pi(t) \to \lambda(t)$. Тогда покажем, что для $P=t+1$ будет справедливо $\pi(t+1) \to \lambda(t+1)$:
\begin{flalign*}
\lambda(t+1) \mathbf{:=} \lambda(t) \land \bigwedge_{j \in [1,N]}(pc^{t+1}_j = 2 \to \bigwedge_{\substack{k \in [1,N],\\k \neq j}}\neg(pc^{t+1}_k = 2))
\end{flalign*}
\begin{flalign*}
\pi(t+1) \mathbf{:=} \pi(t) \land \bigvee_{j \in [1,N]}(\delta_{j}(A^{t+1}, pc^{t+1}_j, A^{t+2}, pc^{t+2}_j) \land \bigwedge_{\substack{k \in [1,N],\\k \neq j}}pc^{t+2}_k = pc^{t+1}_k)
\end{flalign*}

Пусть предикат пути принимает истинное значение, тогда:
\begin{enumerate}
    \item Если все потоки находятся в метках 3 на $k+1$ шаге, то справедливость $\pi(t+1) \to \lambda(t+1)$ не вызывает сомнений, так как блокировка не может быть захвачена.
    \item Если все потоки находятся в метках 1, то только один поток перейдет в метку 2 и формула $\pi(t+1) \to \lambda(t+1)$ также будет верна.
    \item Пусть тогда есть поток с номером $z$, такой что $pc^{t+1}_z = 2$.
    Причем такой поток может быть только один, а иначе не будет верно $\pi(t) \to \lambda(t)$.
    Значит другие потоки находятся в теках 1 или 3.
    Заметим, что тогда $A^{t+1} = 1$, а иначе либо шаг потока $z$ в метку 2 произошел без захвата блокировки, что противоречит характеристической функции операции, либо на некотором шаге до k+1-ого был еще один поток в метке 2 одновременно с потоком $z$.
    Но тогда будет неверно $\pi(t) \to \lambda(t)$.
    В этом случае возможны два развития событий на $k+1$ шаге:
    \begin{enumerate}
        \item Любой поток, включая поток $z$, перейдет в метку 3 на шаге $k+1$, тогда требуемая формула $\pi(t+1) \to \lambda(t+1)$ будет верна.
        \item Какой либо поток перешел в состояние 2, но это противоречит $A^{t+1} = 1$ и характеристической функции операции захвата блокировки.
    \end{enumerate}
\end{enumerate}


\end{proof}

\subsubsection{Расширение языка программирования $LZ$}
Язык программирования $ELZ$ --- это расширение языка $LZ$ операциями посылки и получения сигналов.
Отправка сигнала выполняется операцией $send(d, x_1, ..., x_n)$, а получение операцией $receive(d, y_1, ... y_n)$. 
Здесь $d$ --- это заданное константой имя сигнала.
Получение и отправка сигналов происходят только при выполнении соответствующих операций с одним и тем же именем сигнала, переданного в качестве первого параметра.
Аргументами операции $send$ являются локальные переменные $x_1, ..., x_n$ потока отправителя, значения которых будут переданы получателю сигнала.
Аргументами операции $receive$ выступают локальные переменные $y_1, ... y_n$ потока получателя, в которые будут сохранены значения, переданные отправителем.
Число аргументов может быть разным, но все операции посылки и получения некоторого сигнала $d$ должны иметь равное число и типы аргументов.


Передача и прием сигналов выполняется согласно модели синхронизации рандеву и имеет следующую семантику:
\begin{itemize}
    \item Сигнал передается только между двумя потоками, в которых отправитель выполняет операцию $send(d, ...)$, а получатель $receive(d, ...)$. 
    Если нет ни одного отправителя в момент, когда поток выполняет операцию приема сигнала, то операция не может быть выполнена до тех пор, пока отправитель не появится. 
    Аналогично отправитель не может выполнить операцию отправки, пока не появится получатель.
    \item Если несколько процедур могут послать или получить сигнал с одним именем, то пара отправитель-получатель выбирается случайно.
    Одновременно не может происходить несколько процессов передачи сигналов с одним именем.
    \item После выполнения операции получения или отправки сигнала поток выполняет следующую операцию программы.
\end{itemize}

Рассмотрим операции $send(d, x_i)$ и $receive(d, x_j)$ в потоках $i$ и $j$ соответственно.
Число аргументов не влияет на дальнейшие рассуждения, поэтому для простоты пусть аргумент при передаче сигнала будет всегда один.

В заданной системой символических переходов модели прием сигнала разбит на две операции: инициализация приема $flag$ и непосредственно получение значений $recv$.
Операции не могут встречаться в программе независимо друг от друга и выполняются строго подряд в одной процедуре.
Характеристические функции операций имеют вид:

\begin{flalign*}
\rho_{flag} \mathbf{:=} & s = 0 \land s' = 1 \land same(V_j \setminus {s}) \\
\rho_{recv} \mathbf{:=} & s = 2 \land s' = 0 \land x'_j = t \land same(V_j \setminus \{s, x_j\}) \\
\end{flalign*}

Здесь $s$ и $t$ являются вспомогательными переменными, добавленными к множеству глобальных переменных программы, а $x_j$ --- это локальная переменная получателя.
Переменная $s$ предназначена для управления порядком выполнения операций передачи сигнала.
Ее начальное значение равно 0.
Переменная $t$ предназначена для хранения значений аргументов при пересылке рассматриваемого сигнала.
Переменная $t$ единственная, так как аргумент операций приема и посылки только один.
Каждый сигнал соответствует своей паре уникальных вспомогательных переменных.

Посылка сигнала $send$ происходит за один шаг выполнения, но значения локальной переменной отправляющего потока $x_i$ сохраняются во временной переменной $t$.
Характеристическая функция выполняемой в потоке $i$ операции $send(d, x_i)$ имеет вид:

\begin{flalign*}
\rho_{send} \mathbf{:=} & s = 1 \land s' = 2 \land t' = x_i \land same(V_i \setminus \{s, t\}) 
\end{flalign*}

\begin{lemma}
На пути выполнения блока из операций $flag$ и $recv$ приема сигнала $d$ всегда происходит посылка данного сигнала из другого потока.
\label{send}
\end{lemma}
\begin{proof}
Выполнение посылки или приема зависит только от значений вспомогательных переменных $s$ и $t$.
В таблице~\ref{table:send} представлены предусловия и постусловия операций относительно переменной $s$.
Остальные операции в программе значения вспомогательных переменных не меняют, поэтому не влияют на возможность выполнения рассматриваемых операций.
Если хотя бы один поток выполнил $flag$, то $recv$ не будет выполнена до $send$, поэтому метка выхода из блока никогда не будет достигнута.
Аналогично и $send$ не может быть выполнен до тех пор, пока какой-либо поток не выполнит $flag$.

\begin{table}
\centering
\begin{tabular}{ | l | c | c | }
\hline
Операция & Предусловие & Постусловие \\
\hline
$flag$ & $s = 0$ & $s = 1$ \\
\hline
$send$ & $s = 1$ & $s = 2$ \\
\hline
$recv$ & $s = 2$ & $s = 0$ \\
\hline
\end{tabular}
\caption{Предусловия и постусловия операций посылки и приема сигнала.}
\label{table:send}
\end{table}
\end{proof}

% Ну и заголовок
\subsubsection{Трансляция программ на языке $ELZ$ в программы на языке $LZ$}

Рассмотрим две программы на языке $ELZ$ и на языке $LZ$ соответственно.
Первая называется \textit{исходной программой}, а вторая \textit{результатом трансляции}.
Исходная программа содержит $N$ процедур, как и результат трансляции.
Множества конфигураций программ обозначим $C_1$ и $C_2$ соответственно.
Для множества переменных состояния исходной программы далее используется обозначение $V_{P_1}$, а для множества переменных состояния результата трансляции --- $V_{P_2}$.
В программах достижимы множества состояний $R_1 \subset \Sigma_{V_{P_1}}$ и $R_2 \subset \Sigma_{V_{P_2}}$ соответственно.
Множества переменных программ назовем $V_1$ и $V_2$ соответственно, где $V_1 \subset V_2$.
Множество локальных переменных каждой процедуры в исходной программе совпадает с соответствующим множеством результата трансляции.

Результат трансляции получен из исходной программы при помощи замены операций посылки и приема сигналов на некоторые блоки, называемые \textit{блоками трансляции}.
Остальные операции исходной программы остались без изменения в результате трансляции.
Пусть каждая операция посылки или приема сигнала с меткой $l_i$ транслируется в блок с меткой первой операции $m_i$ и меткой выхода из блока $n_i$.
Если трансляция выполнена согласно предложенной выше схеме, то для каждой процедуры можно построить такое отображение $F_i$, которое каждой метке процедуры $i$ в результате трансляции кроме меток операций из блоков трансляции ставит в соответствие метку той же операции в исходной программе.
Для метки первой операции любого блока трансляции в соответствие ставится метка операции посылки или получения сигнала оригинальной программы.
Остальным меткам операций из блоков трансляции ставится в соответствие пустой элемент $\varnothing$.
Для отображения элементов множества конфигураций $C_2$ в множество $C_1 \cup {\varnothing}$ можно определить отображение $F$ на основе отображений $F_i$.
$F$ отображает элемент $x \in C_2$ в $\varnothing$, если существует хотя бы одна такая переменная $pc_i$, что $F_i(x \Downarrow \{pc_i\}) = \varnothing$.
То есть в $\varnothing$ переводятся все конфигурации результата трансляции, если хотя бы одна процедура в такой конфигурации находится внутри выполнения какого-либо блока трансляции кроме первой операции.
Остальные значения переменных $pc_i$ отображаются согласно $F_i$.

Множеством ошибочных состояний исходной программы называется множество $E_1 = \Sigma_{V_{P_1}} \Downarrow V_1$.
Множеством ошибочных состояний результата трансляции называется множество $E_2 = S_e \Downarrow V_1$, где $S_e = \{s \in \Sigma_{V_{P_2}}| s \Downarrow {PC_2} \in C_2, F(s \Downarrow {PC_2}) \neq \varnothing\}$.
Достижимыми ошибочными состояниями называются соответственно множества проекций $ER_1 = (E_1 \cap R_1) \Downarrow V_1$ и $ER_2 = (S_e \cap R_2) \Downarrow V_1$.

Множества достижимых ошибочных состояний исходной программы и результата трансляции изоморфны, если:
\begin{itemize}
    \item Для любого достижимого состояния $s_1 \in R_1$ и $s_1 \Downarrow V_1 \in ER_1$ существует достижимое ошибочное состояние результата трансляции $s_2 \in R_2$, что $(s_2 \Downarrow V_1) \in ER_2$ и $s_2 \Downarrow V_1 = s_1 \Downarrow V_1$, $F(s_2 \Downarrow PC_2) = s_1 \Downarrow PC_1$.
    \item Для любого достижимого состояния результата трансляции $s_2 \in R_2$, $(s_2 \Downarrow V_1) \in ER_2$ существует такое достижимое состояние исходной программы $s_1 \in R_1$, $s_1 \Downarrow V_1 \in ER_1$, что $F(s_2 \Downarrow PC_2) = s_1 \Downarrow PC_1$.
\end{itemize}

Неформально условие изоморфности означает, что вне блоков с операциями пересылки сигналов в исходной программе и в результате трансляции достижимы только такие состояния, в которых переменные из $V_1$ принимают одни и те же значения.
Достижимость гарантирует, что совпадают множества путей в исходной программе и результате трансляции в рассматриваемых частях программы (вне операций блоков с операциями пересылки сигналов) с одними и теми же значениями переменных из $V_1$ на соответствующих шагах.
А равенство проекций гарантирует, что наборы значений переменных, от которых зависит наличие ошибок в программе, совпадают.
Вспомогательные переменные, добавленные при трансляции операций с сигналами, не важны с точки зрения поиска ошибок, так как поиск ошибок выполняется в программе, полученной при помощи объединения модуля программы и модели окружения, но в модуле программы, который исследуется на наличие ошибок, операций передачи или получения сигналов нет по построению.

Условие изоморфности может быть нарушено только при трансляции операций пересылки сигналов.
Согласно определению эквивалентности блоков, если блок трансляции эквивалентен блоку, который содержит единственную соответствующую операцию посылки или получения сигнала, относительно $V_1$, то множества достижимых ошибочных состояний программ будут изоморфны. 
Данное утверждение следует из определения эквивалентности блоков.

\begin{theorem}
\label{theorem:iso}
Множества достижимых ошибочных состояний исходной программы на языке $ELZ$ и результата ее трансляции в язык $LZ$ изоморфны.
\end{theorem}

\begin{proof}
Рассмотрим исходную программу $P$ на языке $ELZ$ с $N$ процедурами и результат ее трансляции $P'$ на языке $LZ$. 

Для каждого уникального имени сигнала добавим в $P'$  вспомогательные глобальные переменные:
\begin{itemize}
    \item $bool~s = 0$ --- глобальная переменная для управления последовательностью операций приема и передачи.
    \item $Lock~c = 0$ --- переменная блокировка для синхронизации операций по отправке или получению сигналов.
    \item $t$ --- глобальная переменная, в которую будут временно помещаться значения при передаче данных от отправителя к получателю.
\end{itemize}

Переменные $s$ и $t$ соответствуют одноименным переменным, введенным при описании модели пересылки сигналов в $ELZ$.
Здесь переменная $t$ для простоты только одна, так как предполагается, что аргумент при посылке и получении сигналов только один.

Код процедур программы $P'$ кроме операций посылки и получения сигналов остается без изменения.
Для замены операций посылки и приема сигналов предлагаются блоки трансляции, приведенные в таблице~\ref{table:translation}.

\begin{table}
\centering
\begin{tabular}{ | l | l | c | }
\hline
Операция в языке & Операция в модели & Блок трансляции \\
\hline
\multirow{2}{*}[-3em]{$receive(d, x_j)$} & $flag$ & 
\begin{lstlisting}[language=C]
lock(c);
assume(s == 0)
s = 1
unlock(c);
\end{lstlisting} \\
\cline{2-3}
& $recv$ & \begin{lstlisting}[language=C]
lock(c);
assume(s == 2);
x_j = t;
s = 0
unlock(c);
\end{lstlisting} \\
\hline
$send(d, x_i)$ & $send$ & 
\begin{lstlisting}
lock(c);
assume(s == 1);
t = x_i;
s = 2;
unlock(c);
\end{lstlisting} \\
\hline
\end{tabular}
\caption{Блоки трансляции для операций посылки и приема сигналов.}
\label{table:translation}
\end{table}

Для доказательства теоремы требуется показать эквивалентность блоков, состоящих из единственной операции в $ELZ$, попарно блокам трансляции относительно переменных исходной программы $V_1$.
В операциях блоков трансляции изменяются только значения вспомогательных переменных и значение локальной переменной потока получателя сигнала.
Переменные в аргументах операций посылки и получения сигналов являются локальными, поэтому во время выполнения блока трансляции изменить их другие потоки не могут. 
Поэтому при рассмотрении отдельного блока трансляции все другие операции программы, кроме операций приема и отправки того же сигнала, будут независимыми, так как не влияют на значения переменных, изменяемых или читаемых во время выполнения блока.
Тогда, согласно результату леммы~\ref{indep}, при рассмотрении эквивалентности блоков трансляции пути с выполнением независимых операций можно не рассматривать.

Все блоки трансляции выполняются под блокировкой $c$.
Согласно лемме~\ref{locks} предикаты путей через блоки с захваченной блокировкой истинны только при выполнении условия, что разные потоки не могут выполнять код под блокировкой одновременно.
Поэтому каждый блок трансляции не может выполняться с любым другим блоком трансляции, выполняющего прием или посылку того же сигнала.

Вследствие сказанного выше для подтверждения эквивалентности достаточно доказать требуемое свойство эквивалентности блоков только для последовательного случая.

Запишем предикаты последовательных путей через блоки трансляции при помощи предикатов блоков:

\begin{flalign*}
\pi^{t}_{flag} \mathbf{:=} & \gamma \land c^1 = 0 \land s^1 = 0 \land s^2 = 1 \land c^2 = 0 \land same(V_j \setminus \{s\})\\
\pi^{t}_{recv} \mathbf{:=} & \gamma \land c^1 = 0 \land s^1 = 2 \land x^{2}_j = t^{1} \land s^2 = 0 \land c^{2} = 0 \land same(V_j \setminus \{s, x_j\}) \\
\pi^{t}_{send} \mathbf{:=} & \gamma \land c^1 = 0 \land s^1 = 1 \land t^{2} = x^{1}_i \land s^2 = 2 \land \land c^1 = 0 \land same(V_j \setminus \{s, t\})
\end{flalign*}

Где $\gamma$ --- предикат граничного условия.
В модели программ $ELZ$ предикаты пути последовательного выполнения блоков с соответствующими операциями имеют вид:

\begin{flalign*}
\pi_{flag} \mathbf{:=} & \gamma \land s^1 = 0 \land s^2 = 1 \land same(v_j \setminus \{s\})\\
\pi_{recv} \mathbf{:=} & \gamma \land s^1 = 2 \land x^{2}_j = t^{1} \land s^2 = 0 \land same(V_j \setminus \{s, x_j\}) \\
\pi_{send} \mathbf{:=} & \gamma \land s^1 = 1 \land t^{2} = x^{1}_i \land s^2 = 2 \land same(V_j \setminus \{s, t\})
\end{flalign*}

Предикаты путей отличаются только условием захвата блокировки.
Поэтому блоки эквивалентны относительно множества переменных исходной программы $V_1$.
Множества достижимых ошибочных состояний исходной программы и результата трансляции изоморфны.
\end{proof}

Для трансляции промежуточных моделей окружения, заданных при помощи расширения языка Си операциями получения и отправки сигналов, в модели окружения на языке Си будем руководствоваться той же схемой трансляции, которая была предложена при доказательстве теоремы~\ref{theorem:iso}.
При трансляции использовались только операции языка, влияющие на порядок выполнения потоков, ожидание потоков, захват и освобождение блокировок, передачу данных между потоками, простые логические выражения и целочисленная арифметика, поэтому сделанные при переходе от языка Си к языку $LZ$ предположения выполнены.
Поэтому результат теоремы справедлив для исходной программы на языке Си, заданной с использованием предложенных расширений для передачи сигналов, для описания промежуточных моделей окружения и для результата ее трансляции, полученного согласно предложенной в теореме схеме замены операций посылки и получения сигналов.
Результат теоремы справедлив в контексте проверки требований к программам на языке Си, которые сведены к доказательству выполнения свойства недостижимости ошибочного оператора, при помощи инструмента верификации моделей программ при следующих предположениях:
\begin{itemize}
    \item Инструмент верификации моделей программ строит модель с теми же свойствами, которыми обладают модели программ, описанные при помощи символических систем переходов для программ на языках $LZ$ и $ELZ$.
    Например, к таким моделям относятся модели, заданные при помощи структур Крипке.
    \item Программа на языке Си не использует другие средства управления потоками или процессами, которые отличаются от управления потоками согласно стандарту POSIX. 
    В то же время в программе могут использоваться различные наборы механизмов синхронизации.
    Инструмент верификации должен поддерживать верификацию параллельных многопоточных программ, используя представление потоков программы на основе асинхронной композиции моделей отдельных потоков.
    \item Инструмент верификации не требует разработки моделей вспомогательных функций \textit{\_\_VERIFIER\_assume} и \textit{\_\_VERIFIER\_nondet\_int}, используемых при трансляции и предложенных сообществом SV"~COMP, и корректно моделирует их семантику.
\end{itemize}