69
правок
Изменения
Нет описания правки
==Корректность алгоритма==
{{Теорема
|statement = Приведенный алгоритм правильно строит все списки ситуаций.То есть алгоритм поддерживает инвариант <tex> [A \rightarrow \alpha \cdot \beta, i] \in D_{j} \Longleftrightarrow \exists \delta \in \Sigma \cup N : ((S \Rightarrow^* w_0...w_i A \delta) \wedge A \Rightarrow^* w_i...w_j)</tex>
|proof =
=====Алгоритм не добавит в список ситуацию, которая ему не принадлежит:<tex>\Longrightarrow</tex>=====
Докажем индукцией по исполнению алгоритма.<br/>
База (инициализация): <tex>\alpha = \varepsilon \Rightarrow^* \varepsilon </tex> и <tex>[S' \Rightarrow^* rightarrow \gamma cdot S , 0] \delta </tex> при <tex>\gamma = \delta = \varepsilon in D_0</tex>.<br/>Индукционный переход: пусть в <tex> I_D_{0},...,I_D_{j} </tex> нет лишних ситуаций. Пусть включаем <tex>[A \rightarrow \alpha \cdot \beta, i] </tex> в <tex>I_D_{j}</tex>. Рассмотрим три случаяСитуация может включится одним из трех способов: 1. Включаем по правилу <tex> \mathtt{scan}</tex>.<br/>
1. Включаем по правилу <tex>(1)</tex>.<br/>