程序的形式验证相关基础-

第1页 / 共7页

第2页 / 共7页

第3页 / 共7页

第4页 / 共7页

第5页 / 共7页

第6页 / 共7页

第7页 / 共7页

程序的形式验证 -相关基础中国科学院软件研究所张文辉http:/lcs.ios.ac.cn/zwh/pv相关基础逻辑函数有向图逻辑：公式I=(D,I0) ：解释(XD)：赋值/状态I(x1/1xn/n)()I()(x1/I(1) ()xn/I(n)()函数X：集合f：X X不动点：f(x)=xX=(X,)：完全偏序f：单调、连续最小不动点：f = 有向图V：点的集合E：边的集合(V,E) ：有向图有向图：(V1,E1), (V2,E2) 关系： R V1V2模拟关系： R-1 E1 E2 R-1互模拟关系：R-1 E1 E2 R-1且R E2 E1 R相关基础阅读： http:/lcs.ios.ac.cn/zwh/pv/l1n09.pdf习题： http:/lcs.ios.ac.cn/zwh/pv/l1n11exe.pdf7问题 ?