谓词变换器语义学

语言学vte谓词变换器语义学是，通过给这种语言中的每个语句分配一个相应的谓词变换器来定义命令式编程范式的语义：语句的状态空间上两个谓词之间的总函数。在这个意义上，谓词变换器语义学是一种指称语义学。实际上，在受保护的命令中，Dijkstra只使用了一种谓词转换器：众所周知的最弱前提条件。此外，谓词变换器语义是对Floyd-Hoare逻辑的重新表述。而Hoare逻辑是作为一个演绎系统提出的，谓词变换器语义是建立Hoare逻辑有效演绎的完整策略。换句话说，它们提供了一种有效的算法，将验证Hoare三段论的问题减少为证明一阶公式的问题。从技术上讲，谓词转换语义学执行一种将语句转化为谓词的符号执行：在最弱先决条件的情况下，执行向后运行，在xxx后决条件的情况下，执行向前运行。

对于一个语句S和一个后置条件R，最弱的前提条件是一个谓词Q，使得对于任何前提条件P。.换句话说，它是保证R在S之后成立所需的最宽松或限制性最小的要求。

暂时不考虑终止，我们可以用一个谓词I来定义最弱自由前提条件的规则，表示为wlp，这个谓词称为循环不变性，通常由程序员提供。这简单地说明：(1)不变量在循环开始时必须成立；(2)此外，对于任何初始状态y，不变量和保护措施一起足够强大，以建立循环体能够重新建立不变量所需的最弱前提条件；(3)最后，如果和当循环在给定的状态y终止时，循环的事实。