math - プログラミング理論 - 不変式の証明

Question

関数 Next[u,x] が u からの u エッジを持つノードのセットを与えるリラックスしたトライを使用して、文字列を認識するためのこの疑似コードを定義しました (基本的に (u,x,v)は T のエッジです)。

ここにあります：

U := {1};

while s ≠ λ and U ≠ Ø do


 U:= U in u Union Next [u, head(s)];
 s:= tail(s)
 od;

 if U ≠ Ø then
  if Final[u] for some u in U then
    Accept 
  else reject
  fi
 else
   reject
 fi

基本的に、ループの事後条件を定義し、ループ不変条件を指定しました (これらの要素をカバーしたと思いますが、説明するのに役立つと思われる場合は、それを使用してください)。

したがって、不変条件が不変である理由 (つまり、ループ条件が成立する場合にループ本体によってどのように保持されるか) を示す短い引数を与える必要があります。

次に、入力を進めずに新しいノードに移動できるように、この擬似コードを拡張する必要があります。

(別の配列 (Null など) を追加することでこれを行うと思います。Null[u] は、入力を進めずに u から移動できる状態のセットです)

また、入力を進めることなく U の状態から入力のすべての状態を確認する前の各反復に到達できるように変更する必要があります。

ご協力いただきありがとうございます。これらの 2 つの手順は非常に難しいと感じていますが、最初の部分の疑似コードは問題ないと思います