程序求精新策略及自动验证方法研究

传统的程序求精策略无法求精至可执行程序,且存在验证的可信度低和自动化程度不高的问题。针对上述问题,提出一种较完整的程序求精策略并给出自动验证方法。使用递归定义函数技术刻画问题规约,基于Morgan精化规则程序求精至IMP程序,并使用验证条件生成器(verification condition generator,VCG)自动生成验证条件,通过Isabelle定理证明器验证IMP程序的正确性,最后利用开发平台自动生成C++可执行程序。以最长标志基因序列问题为实例进行程序求精和自动验证,检验了所提策略的有效性。该策略提高了算法程序开发的正确性,减轻了传统验证烦琐的工作量。

法律英语中and和or的语义分析

法律英语具有严谨,庄重的特点,在措词上强调准确,精练,得当,符合法律庄严的特点。英语句级语义结构的特征是关系词结集(connective-oriented nexus),英语语义的合成主要通过关系词这个外显形标记来实现。And和or是英语中最重要的关系词之一,在语义合成过程显得尤其重要,因为它们不仅具有连接句子的功能,还可以用来连接词,短语,以及从句。然而在语言应用过程中,and和or的使用有时会使得法律工作者们难以把握和理解句子的意思,语义含混的情况时有发生,本文着力于探讨法律条文中出现and和or时,该两个词语对于整句话的语义影响,运用案例分析,从而探讨如何来努力避免因为这两个词带来的司法争议。