编程理论 - 证明不变量

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 中的状态到达所有状态，而无需提前输入

感谢您的所有帮助，我发现这两个步骤非常困难，但认为我的第一部分的伪代码很好