Intro to Constraint-based Verification

CS › Program Synthesis

参考 MIT CS 6.S981 Lec 11

有一种通用的验证方法，就是将程序自动转换为以下形式的逻辑语句

$$\varphi = \forall x.Q(x) $$

那么程序正确的一个充分条件就是 $\varphi$ 为真.

我们以如下的语言为例, 介绍一些重要的概念.

1
2
3
4
5
6
expr := N | x | expr + expr | expr > expr
cmd  := x := expr
      | cmd ; cmd
      | if( expr ) cmd else cmd
      | while( expr ) cmd
      | skip

A program in this language manipulates a state $\sigma$ that maps each variable to an integer value. We denote expression $expr$ evaluates to $n$ under state $\sigma$ by

$$<expr, \sigma>\to n $$

and denote commands (often called statements) transform a state $\sigma$ into another state $\sigma^\prime$ by

$$<cmd, \sigma>\to \sigma^\prime $$

1. Program Logics

我们介绍一些关于 formalism of Program Logics 的背景知识 (aka Axiomatic Semantics, aka Hoare-Floyd style verification.)

$\textbf{Definition}$: Hoare Triple

$\{A\}cmd\{B\}$ is a Hoare Triple meaning that for all states satisfying predicate $A$, if we execute command $cmd$ starting from this state and it terminates then the resulting state will satisfy predicate $B$.

这里的 predicate 指的是断言.

$\textbf{Definition}$ Stronger version of Hoare Triple

在上面的基础上, 如果运行完 $cmd$ 之后, 程序的确可以终止, 那么上述的 Hoare Triple 可以加强为

$$[A]cmd[B] $$

This implies that $cmd$ will terminate on all inputs that satisfy the predicate A.

TBD.