如何判定LR(0)分析程序工作的正确性

如何判定LR(0)分析程序工作的正确性？在实际使用LR(0)分析器之前，我们需要确信它们可以正确运行。这通常通过陈述并证明一个“正确性定理”来完成。对于我们的目的而言，重要的是包含在这样一个证明中的洞察力。一旦理解了基本思想，也就容易明白证明的细节。LR(0)分析器的正确性依赖于两点观察。首先，CFSM仅能读入的符号串是所分析的文法的活前缀。这一点观察非常重要，因为它告诉我们如果看到非法符号，那么该符号将不会被语法分析器所接受，理由是它不可能是活前缀的一部分。第二点观察是语法分析器的action表正确地指示了适当的行动。即，action表指示移进直到看到了句柄的结尾。随后它指示必要的归约，用相应的产生式的左部替换句柄。回忆右句型的活前缀是不超出其句柄的任意前缀。句柄是可被正确地归约为非终结符的昀左短语。直观地说，LR(0)分析器或任何其他的移进-归约分析器会移进符号以形成一个活前缀，直到整个句柄都被移进为止。随后该句柄被归约为单独的非终结符。LR(0)分析器的CFSM必须能够读入所有活前缀以保证没有漏掉任何合法归约。CFSM不需要读入右句型的所有可能的前缀，因为句柄一被移进并识别，就立即被归约。类似地，如果一个符号序列不可能是任何右句型的前缀，则它无法被分析并且不应被CFSM接受。假定有活前缀ν，怎样从其中创建新的活前缀？ν的任意前缀都是活前缀，而且如果ν仅包含终结符，这些前缀是可由它创建的仅有的活前缀。如果ν至少包含一个非终结符B，则可以把ν写成αBγ。可以使用某个产生式B→β来重写B得到αβγ。αβ的任意前缀都是活前缀，由于β是句柄，因此没有活前缀可以扩展超过β。作为一般的规则，我们通过取以非终结符B结尾的活前缀并把B替换为β的任意前缀，来创建新的活前缀，其中B→β。为证明活前缀和由CFSM所读入的字符串的对应关系，从CFSM的开始状态s0开始。s0可通过读入λ到达，而λ是所有右句型的活前缀。根据其构造，s0包含一个基本项：S→•α$。s0面临α$时有后继。这是正确的，正如我们所知α$的所有前缀都是活前缀，因为α$可被归约为S。令βC是α$的以非终结符结尾的任意前缀。在读入β后，将处于CFSM的一个状态s，其中包含形如D→γ·Cδ的一项。这种形式的一个项目必定出现在S中，因为我们知道从状态s开始可以读入C。因为C是非终结符，对于左部为C的每条产生式，LR(0)闭包操作将包含形如C→•ρ的项目。根据其构造，状态s面临输入ρ时有后继状态，这意味着βρ的任意前缀可以从s0读入。重复这样的论证，容易看出从βρ创建的任意活前缀也能够由CFSM读入。因此，以状态s0开始的CFSM能够读入所有可能的活前缀。为明白CFSM仅读入活前缀，假定由CFSM所读入的所有长度为n的字符串都是活前缀。这对n=0的情况肯定是正确的。令βX是可由CFSM读入的长度为n+1的字符串。在读入β后，必定处于状态s中，从它开始可以读入X。这意味着s包含形如B→γ•Xδ的项目。该项目是基本项或者闭包项。如果它是基本项，γ必定至少一个字符长，否则该项目一定是开始项目S→•α$。已知α$的所有前缀都是活跃的，因此假定|γ|=m≥1。βX的昀后m个符号必为γ，因为s中包含B→γ•Xδ。在读入βX开头的n-m个符号ω之后，将处于包含B→·γXδ的状态s′。s′必须也包含B的前面直接为•的项目，因为B→•γXδ仅能通过预测被创建。因此，B能够从s′读入，且因此ωB能够从s0读入。由于|ωB|≤n，ωB是活前缀，且因此ωγX=βX也是活前缀。如果B→γ·Xδ是闭包项，则γ必定为空。B→•Xδ通过求某个基本项的闭包被直接或间接地加入。即，s必定包含基础项D→θ•C1π，其中C1→C2σ2,C2→C3σ3,…,Cρ→Bσρ+1。利用上一段的论证，可以断定βB是活前缀，且βX也是活前缀。以上已经证明了CFSM精确地接受所分析的文法的活前缀集。为确信LR(0)分析器能够正确工作，余下的一切就是要证明相应于CFSM状态的语法分析器action表总是执行正确的分析动作。假定正在分析某个有效输入字符串z，并且已经完成了零次或多次正确的归约得到右句型γy，其中y是剩余的输入，而γ已经被移进分析栈中。我们通过从y移进零个或多个终结符号到达下一个句柄。假定S*⇒rmαAw⇒rmαβw，其中αβ=γx，且xw=y。即，正确的语法分析器动作是读入x，随后执行A→β的归约。可以确信这是LR(0)编译器将要做的么？假定在移进γ之后处于状态s。x能够从s读入，因为γx=αβ是活前缀。进一步，语法分析器直到移进所有x之前不执行归约。这个结果是根据这样一个事实得出：在移进x时访问的每个状态必须执行移进动作，因此任意归约动作将导致移进-归约冲突，而这对LR(0)文法来说是不允许的。因此语法分析器在读入x时不执行假归约。已知αA是活前缀。读入α之后所到达的状态一定包含一项B→ν•Aδ，并因此也包含一项A→•β。该状态面临β的后继必须包含一项A→β•，此状态在移进x之后到达，而且将会执行所期望的归约动作。以上论述证明，在已经将输入字符串z归约为γy之后，语法分析器将正确地执行下面的步骤，并把αβw归约为αAw。通过对推导z所需步数的归纳，可以确定它将昀终被归约为目标符号S，由此成功地完成分析。昀后一点，如果交给LR(0)分析器一个不正确的输入字符串将会怎样？CFSM仅能够读入活前缀，因此输入若在某些点不能被归约为活前缀，语法错误将会被正确地检测出来。