动态逻辑

英文

dynamic logic

简介

亦称程序模态逻辑.一种非经典逻辑.指在程序设计语言基础上扩展模态逻辑的一种形式.此类逻辑系统使用无穷多对模态词，即对每一程序段α引入一对模态词[α]和〈α〉，使得对系统的任一合适公式A：

[α]A表示：执行程序段α后的一切可能状态中，A均为真.

〈α〉A表示：执行程序段α后至少有一种可能状态中，A为真.

动态逻辑可刻画相应程序设计语言的语义，并在系统内对相应语言编写的程序进行正确性证明.