《程序的形式验证-相关基础》由会员分享,可在线阅读,更多相关《程序的形式验证-相关基础(7页珍藏版)》请在金锄头文库上搜索。
程序的形式验证 -相关基础中国科学院软件研究所张文辉http:/ 公式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:/ http:/ ?