命令式程序的建模

这里给出基于状态的程序的定义。

CFG和transition system都可以被用来描述程序。本质上，程序底层是一个变迁系统，即一组状态及其转移关系。

基于CFG的形式化

程序被形式化为CFG，其节点集L是程序中的位置。位置之间有转移函数 $\delta$，程序的转移用statement标注。设S是状态集，由所有的对程序中出现的变量的valuation组成。每个statement T都有其语义，即关系 $R_T\subset S\times S$，对应着 transition formula。

如此定义的程序对应着一个变迁系统，其状态集是$L\times S$，转移关系R如下定义：$(l,s)R(l^{\prime },s^{\prime })$当且仅当$\exists T,(l,T,l^{\prime })\in \delta \wedge (s,s^{\prime })\in R_T$。初始状态集对应于CFG的初始位置。