模拟试题一
《软件形式化方法》期末考试试题
（120分钟）
题号
一
二
三
四
五
六
七
总分
题分
得分
一、填空题。（20分）
1,软件开发是一项包括需求获取、,,系统实现、测试的系统工程，主要经历了三个发展阶段：,,。
2,现代软件工程对于软件的定义中包括：当它被执行时能够提供所要求的功能和性能的 ；使得程序能够满意地处理信息的 ；描述程序的功能需求以及程序的 。软件工程的目标是成功地生产具有,及开销合宜的产品。
3,在形式化方法框架内可以以系统的方式,和 系统；软件开发中的形式化方法主要运用 和 描述“需求的清晰陈述”。
4,VDM是一种功能性规格说明技术，通过 和已建立的 来描述每个运算或函数的功能；与Z语言类似，VDM中的集合表示方法有 和 ；对一个软件系统来说，其VDM描述包括 和 两个部分。
二、对于图中所示有限状态机的状态转移图，给出其关系矩阵和状态转移表。（10分）
三、简述Petri网中的顺序关系、并发关系、冲突关系和混惑关系。（10分）
四、计算下列进程的事件集和迹。（10分）
(P1) μX,{a,b} ·a→X
(P2) (a→STOP{a,b})||(b→STOP{a,b})
五、逻辑演算证明。（15分）
（1）(P∧Q) ∧R├ P∧(Q∧R)
（2）├ (P→(Q→R))? ((P∧Q) →R)
（3）P(a,b) ∧((X)( ((y)P(Y,X) ∨P(X,Y) →P(X,X)) ├P(a,a)
六、对于图中所示的Kripke结构，写出其对应的三元组形式，并分别在状态s0，s1，s2，s3下考察下述CTL公式是否成立。（20）
（1）E○p
（2）Ap(
（3）E?(Ep)(
七、对于某互联网应用系统，每个用户使用系统前必须用口令进行登录。应用Z语言规格一个系统LogSys，该系统可以保存已注册的用户及其口令信息，并且可以跟踪当前已登录系统的在线用户。（15）
（1）定义ΔLogSys、ΞLogSys和InitLogSys；
（2）定义操作模式，用来注册一个新的用户和口令；
（3）定义操作模式，用来注销一个用户及其口令。
参考答案与答题要点一、填空题
1,需求分析 系统设计 程序设计阶段 程序系统阶段
2,指令或计算机程序 数据结构 操作和使用文档 正确性 可用性
3,刻画 开发 验证 集合论 逻辑符号体系
4,一阶谓词逻辑 抽象数据类型 枚举表示法 特征表示法 状态 操作
二、状态转移图和状态转移表
三、M为Petri网PN的一个标识，若存在t1和t2使得M[ t1>M’，且﹁M[ t2>，M’[ t2>，亦即，在M标识下，t1使能，而t2不使能，且t1的引发会使t2使能，即t2的使能以t1的引发为条件，则称t1和t2在M下有顺序关系。
M为Petri网PN的一个标识，若存在t1和t2使得M[ t1>和M[t2>，并满足M[ t1>M1=> M1 [ t2>，且M[ t2>M2=> M2[t1>,则称t1和t2在M下并发。就是说M标识下，t1和t2都使能，且它们当中任一个迁移的引发都不会使另一个迁移不使能。
M为Petri网PN的一个标识，若存在t1和t2使得M[ t1>和M[t2>，并满足M[ t1>M1=>﹁M1 [ t2>，且M[ t2>M2=> ﹁M2[t1>,则称t1和t2在M下冲突。就是说M标识下，t1和t2都使能，但它们当中任一个迁移的引发都会使另一个迁移不使能。
一个Petri网中可能同时存在着并发和冲突，而且并发迁移的引发会引起冲突的消失或出现。像这样并发和冲突混合在一起产生的困惑，无法根据状态的变化判断其间是否出现过冲突，所以将这种情况称为混惑。
四、(P1) 事件集：{a,b}
迹：{< >,< a>,<a,a>,<a,a,a>,…}
(P2) 事件集：{a,b}
迹：{< >,<a>,<b>}
五、（1）(P∧Q) ∧R├ P∧(Q∧R)
P∧Q 前提引入规则
P 1及基本蕴含公式
Q 1及基本蕴含公式
R 前提引入规则
Q∧R 3,4及基本蕴含公式
P∧(Q∧R) 2,5及基本蕴含公式
（2）├ (P→(Q→R))? ((P∧Q) →R)
P→(Q→R) 前提引入规则
(P∨(Q→R) 1及基本等价公式
(P∨((Q∨R) 2及基本等价公式
(P∨(Q∨R 3及基本等价公式
((P∧Q)∨R 4及基本等价公式
(P∧Q) →R 5及基本等价公式
（3）P(a,b) ∧((X)( ((y)P(Y,X) ∨P(X,Y) →P(X,X)) ├P(a,a)
合取因子：P(a,b) (P(y,x)∨P(x,x),(P(x,y)∨P(x,x) (P(a,a)
(P(x,y)∨P(x,x) 前提引入规则
(P(a,b)∨P(a,a) 1及全称量词消去规则
(P(a,a) 前提引入规则
(P(a,b) 3及基本等价公式
P(a,b) 前提引入规则
NIL 4,5归结
六、W={a0,s1,s2,s3} R={<s0,s1>,<s0,s2>,<s1,s0>,<s1,s3>,<s2,s1>,<s3,s3>} L(s0)={p},L(s1)={p,q},L(s2)={p,r}，L(s3)={q}
E○p,s0 s1 s2成立 s3不成立
Ap:( s0 s1 s2 s3 均不成立
E?(Ep),s0 s1( s2成立 s3不成立七、模式定义:
（1）
---------ΔLogSys----------------
registry,registry’,P User
login,login’,P User
---------------------------------------------
login?registry
login’?registry’
----------------------------------------------
---------ΞLogSys----------------
ΔLogSys
---------------------------------------------
registry= registry’
login= login’
---------------------------------------------
---------InitLogSys----------------
registry’,P User
login’,P User
---------------------------------------------
registry’={ }
login’={ }
---------------------------------------------
（2）
---------RegistrySys---------------------
ΔLogSys
name?,seq Char
password?,seq Char
---------------------------------------------
registry’= registry∪{name? ( password?}
login’=login
---------------------------------------------
（3）
---------LogoutSys-----------------------
ΔLogSys
name?,seq Char
---------------------------------------------
login’= {name}login
---------------------------------------------
模拟试题二
《软件形式化方法》期末考试试题
（120分钟）
题号
一
二
三
四
五
六
七
总分
题分
得分
一、填空题。（20分）
1,软件危机是指在计算机软件的开发和维护过程中所遇到的一系列严重的问题，其产生的原因主要包括：,,,；其本质特征是软件的 和 。
2,形式化方法研究如何把（具有清晰数学基础的）严格性（描述形式、技术和过程等）融入软件开发的各个阶段；包括形式化规格,和 三种活动，在软件开发的形式化规格中包含的三种规格为,和 。
3,Petri网适合于描述并发、异步、分布式软件系统规格，是由,和 三个部分组成；特殊的Petri网类型中,和 不能描述冲突,允许冲突和并发同时存在,可以用来描述非对称类型的混惑关系。
4,模式是Z语言规格中一个重要的元素，模式包含和模式连接的前提条件是,即不同模式中 是相同的。
二、构造有限状态机，使其接受的语言为由0和1构成的字符串的集合，分别满足下列条件。（10分）
（1）每个字符串以00结束。
（2）每个字符串中有3个连续的0出现。
三、对图中所示Petri网进行化简。（10分）
四、构造下述系统过程的CSP进程。（10分）
银行的每个客户先开设（open）一个账户，然后该客户就可以多次执行存（deposit）或取（withdraw）操作，最终还可能终止（terminate）该账户。假定不考虑客户每次存或取得款项数目，也不考虑透支的情况。
五、逻辑演算证明。（15分）
（1）(P∨Q) ∧(P∨R)├ P∨ (Q∧R)
（2）P∧(Q?R)├ (P∧Q)?(P∧R)
（3）├ ((x)(P(X) →((Y)P(Y))
六、对于图中所示的Kripke结构，写出其对应的三元组形式，并分别在状态s0，s1，s2，s3下考察下述CTL公式是否成立。（20）
（1）A○p
（2）Ep(
（3）A(p?q)
七、在教材7.3节中描述的电话号码系统中增加下列操作，给出完整的操作模式。（15）
（1）收回电话（RemoveEntry）：收回已经分配给某人的电话；
（2）查询电话用户（FindNames）：查询指定号码的电话用户；
（3）更改电话号码（ChangeEntry）：更改某个用户的电话号码。
参考答案与答题要点一、填空题
1,软件开发成本高 速度缓慢甚至延迟 软件运行的质量差 可靠性难以得到保证 复杂性 多样性
2,形式化验证 程序精化 行为规格 设计规格 程序规格
3,位置 迁移 流关系 状态机 标记图 自由选择网 非对称的自由选择网
4,模式兼容 同一变量的类型二,（1）
（2）
三,（1）
（2）
四、 BANK=open->(x:{deposit,withdraw}(OPER(x))(terminate;
OPER(deposit)=(deposit(STOP);
OPER(withdraw)=(withdraw(STOP)。
五、（1）(P∨Q) ∧(P∨R)├ P∨ (Q∧R)
P∨Q 前提引入规则
P∨R 前提引入规则
P∨ (Q∧R) 1,2及基本蕴含公式
（2）P∧(Q?R)├ (P∧Q)?(P∧R)
Q?R 前提引入规则
(Q∧R)∨(?Q∧? R) 1及基本等价公式
(?Q∨R) ∧(Q∨? R) 2及基本等价公式
P,?Q∨R,Q∨? R 3及前提引入规则
P∧Q 假设前提引入
Q 5及基本蕴含公式
R 4,6及基本蕴含公式
P∧R 4,7及基本蕴含公式
(P∧Q) →(P∧R) 5,8归结
P∧R 假设前提引入
R 10及基本蕴含公式
Q 4,11及基本蕴含公式
P∧Q 4,12及基本蕴含公式
(P∧R) →(P∧Q) 5,8归结
(P∧Q)?(P∧R) 9,14归结
（3）├ ((x)(P(X) →((Y)P(Y))
((x)(P(X) →((Y)P(Y)) 前提引入规则
((x)P(X)∨((Y)P(Y) 1及基本蕴含规则
((x)?P(X)∨((Y)P(Y) 2及量词转换规则
((x) (?P(X)∨P(X)) 3及全称量词消除规则
P(a)∨P(a) 4及全称量词消除规则
T 5及基本等价公式
六、W={a0,s1,s2,s3} R={<s0,s1>,<s0,s2>,<s1,s0>,<s1,s3>,<s2,s1>,<s3,s3>} L(s0)={p},L(s1)={p,q},L(s2)={p,r}，L(s3)={q}
A○p：s0,s2成立 s1,s3不成立
Ep(：s0,s1,s2成立 s3不成立
A(p?q)：s0,s1,s2,s4成立七、模式定义:
（1）
---------RemoveEntry----------------
PhoneDB
name?,Person
---------------------------------------------
name? ∈dom hasphone
hasphone’= {name?}hasphone
---------------------------------------------------------
（2）
---------FindNames----------------
=PhoneDB
number?,Phone
---------------------------------------------
number? ∈ran hasphone
name!= hasphone-1 (|{number}|)
----------------------------------------------------------------------------
（3）
---------ChangeEntry----------------
PhoneDB
name?,Person
newnumber?,Phone
---------------------------------------------
name? ∈dom hasphone
hasphone’=( {name?}hasphone)∪{name? (newnumber?}
----------------------------------------------------------------------------
模拟试题三
《软件形式化方法》期末考试试题
（120分钟）
题号
一
二
三
四
五
六
七
总分
题分
得分
一、填空题。（20分）
1,软件危机是指在计算机软件的 过程中所遇到的一系列严重的问题，应对软件危机的方式分为两种方法,和 。对于软件开发组织和管理的规范化方法中，主要研究,和 三个要素。
2,形式化方法研究如何把（具有清晰数学基础的） （描述形式、技术和过程等）融入软件开发的各个阶段；包括,形式化验证和程序精化三种活动。形式化验证主要技术包含 和 ；程序精化是将 与 相结合，研究从抽象的 推演出具体的面向计算机的 。
3,模式是Z语言规格中一个重要的元素，模式是由,和
组成。
4,Larch方法是软件系统规格的一种 ；Larch方法的程序规格包括 和与目标语言相关的 两个部分。
二、利用有限状态机描述“AB协议”。（15分）
AB协议包含发送端和接收端两个实体。发送端协议实体从发送方用户获取一个报文，将序号寄存器值赋给报文，然后向接收端协议实体发出报文，发送方发出报文之后启动超时时钟，等待认可报文。如果在给定的时间内未收到认可报文，则重发报文；如果收到认可报文，其序号与发出报文序号相同，则发送端实体从发送方用户获取下个报文。接收端协议实体在收到报文之后，如果报文无错误，则想发送端实体发送认可报文，然后将报文递交给接收方用户；如果接收的报文有错误或者序号不正确，则丢失报文。假定所用通道不会中断；报文重复n次后最终能够被接收；认可报文只要发出就能正确收到；报文不会损坏；序号寄存器初始化为0 。
三、构造下图所示Petri网的覆盖树。（10分）
四、利用CSP对“生产者-消费者”系统进行规格。（10分）
五、逻辑演算证明。（15分）
（1）((Q∨R) ∧(P(Q)├(P
（2）(P((Q(S)) ∧ ((R∨P) ∧Q├ R→S
（3）((x)P(x)(((x)(P(x)(Q(x)(R(x)),((x)P(x),((x)Q(x)├ R(a)(R(c)
六、如图中所示的Kripke结构，利用标号算法对公式进行模型检验。（15）
（1）E((p ∧r)?p)
（2）A(p?q) = (E(((p?q))
七、对于哲学家就餐问题，利用CTL描述下述性质。（15）
（1）相邻的两个哲学家不能同时都在用餐；
（2）一个哲学家只要处于等待用餐状态，就可以最终进入用餐状态；
（3）存在一个状态使得该状态下每个哲学家都拿起一把叉子。
参考答案与答题要点一、填空题
1,开发和维护 软件工程 软件形式化 方法 工具 过程
2,严格性 形式化规格 模型检验 定理证明 自动推理 形式化方法形式规格 程序代码
3,模式的名字 声明/说明部分 断言/谓词部分
4,双层规格方法 Larch共享语言 Larch接口语言
二、发送端：{持有报文Shold，等待认可Swait，收到应答Sack}
接收端：{等待报文Rwait，报文正确Rtrue，报文错误Rerror}
计时器：{启动Tstart，停止Sstop，超时Sover}
三,覆盖树：
四、 P<x>=produce?x(write!x ;
C<x>=read?x(consume!x ;
B=P<x>(P<y>|(C<x>(B),
五、（1）((Q∨R) ∧(P(Q)├(P
((Q∨R) ∧(P(Q) 前提引入规则
(Q∧(R 1及基本等价公式
(P∨Q 1及基本等价公式
(Q 2及基本蕴含公式
(P 3,4及基本蕴含公式
（2）(P((Q(S)) ∧ ((R∨P) ∧Q├ R→S
(R∨P 前提引入规则
R(P 1及基本等价公式
R 结论引入规则
P 2,3及基本蕴含公式
P((Q(S) 前提引入规则
Q(S 4,5及基本蕴含公式
Q 前提引入规则
S 6,7及基本蕴含公式
（3）((x)P(x)(((x)(P(x)(Q(x)(R(x)),((x)P(x),((x)Q(x)├ R(a)(R(c)
((x)P(x)(((x)(P(x)(Q(x)(R(x)) 前提引入规则
P(a)(((z)(P(z)(Q(z)(R(z)) 1及存在量词消去规则
((x)P(x) 前提引入规则
P(a) 3及存在量词消去规则
((x)Q(x) 前提引入规则
Q(c) 5及存在量词消去规则
((z)(P(z)(Q(z)(R(z)) 2,4及基本蕴含公式
P(a)(Q(a)(R(a) 7及z/a
P(c)(Q(c)(R(c) 7及z/c
R(a) 4,8及基本蕴含公式
R(c) 6,9及基本蕴含公式
R(a)(R(c) 10,11及基本蕴含公式
六、（1）E((p∧r)?p)
（2）A(p?q) = (E(((p?q))
七、CTL描述:
（1）A((((Pi=eating)((Pi+1=eating)) i=0,1,2,3,4 P5=P0
（2）A( ((Pi=waiting)(A◇(Pi=eating))
（3）E◇(Pi=forking)
《软件形式化方法》期末考试试题
（120分钟）
题号
一
二
三
四
五
六
七
总分
题分
得分
一、填空题。（20分）
1,软件开发是一项包括需求获取、,,系统实现、测试的系统工程，主要经历了三个发展阶段：,,。
2,现代软件工程对于软件的定义中包括：当它被执行时能够提供所要求的功能和性能的 ；使得程序能够满意地处理信息的 ；描述程序的功能需求以及程序的 。软件工程的目标是成功地生产具有,及开销合宜的产品。
3,在形式化方法框架内可以以系统的方式,和 系统；软件开发中的形式化方法主要运用 和 描述“需求的清晰陈述”。
4,VDM是一种功能性规格说明技术，通过 和已建立的 来描述每个运算或函数的功能；与Z语言类似，VDM中的集合表示方法有 和 ；对一个软件系统来说，其VDM描述包括 和 两个部分。
二、对于图中所示有限状态机的状态转移图，给出其关系矩阵和状态转移表。（10分）
三、简述Petri网中的顺序关系、并发关系、冲突关系和混惑关系。（10分）
四、计算下列进程的事件集和迹。（10分）
(P1) μX,{a,b} ·a→X
(P2) (a→STOP{a,b})||(b→STOP{a,b})
五、逻辑演算证明。（15分）
（1）(P∧Q) ∧R├ P∧(Q∧R)
（2）├ (P→(Q→R))? ((P∧Q) →R)
（3）P(a,b) ∧((X)( ((y)P(Y,X) ∨P(X,Y) →P(X,X)) ├P(a,a)
六、对于图中所示的Kripke结构，写出其对应的三元组形式，并分别在状态s0，s1，s2，s3下考察下述CTL公式是否成立。（20）
（1）E○p
（2）Ap(
（3）E?(Ep)(
七、对于某互联网应用系统，每个用户使用系统前必须用口令进行登录。应用Z语言规格一个系统LogSys，该系统可以保存已注册的用户及其口令信息，并且可以跟踪当前已登录系统的在线用户。（15）
（1）定义ΔLogSys、ΞLogSys和InitLogSys；
（2）定义操作模式，用来注册一个新的用户和口令；
（3）定义操作模式，用来注销一个用户及其口令。
参考答案与答题要点一、填空题
1,需求分析 系统设计 程序设计阶段 程序系统阶段
2,指令或计算机程序 数据结构 操作和使用文档 正确性 可用性
3,刻画 开发 验证 集合论 逻辑符号体系
4,一阶谓词逻辑 抽象数据类型 枚举表示法 特征表示法 状态 操作
二、状态转移图和状态转移表
三、M为Petri网PN的一个标识，若存在t1和t2使得M[ t1>M’，且﹁M[ t2>，M’[ t2>，亦即，在M标识下，t1使能，而t2不使能，且t1的引发会使t2使能，即t2的使能以t1的引发为条件，则称t1和t2在M下有顺序关系。
M为Petri网PN的一个标识，若存在t1和t2使得M[ t1>和M[t2>，并满足M[ t1>M1=> M1 [ t2>，且M[ t2>M2=> M2[t1>,则称t1和t2在M下并发。就是说M标识下，t1和t2都使能，且它们当中任一个迁移的引发都不会使另一个迁移不使能。
M为Petri网PN的一个标识，若存在t1和t2使得M[ t1>和M[t2>，并满足M[ t1>M1=>﹁M1 [ t2>，且M[ t2>M2=> ﹁M2[t1>,则称t1和t2在M下冲突。就是说M标识下，t1和t2都使能，但它们当中任一个迁移的引发都会使另一个迁移不使能。
一个Petri网中可能同时存在着并发和冲突，而且并发迁移的引发会引起冲突的消失或出现。像这样并发和冲突混合在一起产生的困惑，无法根据状态的变化判断其间是否出现过冲突，所以将这种情况称为混惑。
四、(P1) 事件集：{a,b}
迹：{< >,< a>,<a,a>,<a,a,a>,…}
(P2) 事件集：{a,b}
迹：{< >,<a>,<b>}
五、（1）(P∧Q) ∧R├ P∧(Q∧R)
P∧Q 前提引入规则
P 1及基本蕴含公式
Q 1及基本蕴含公式
R 前提引入规则
Q∧R 3,4及基本蕴含公式
P∧(Q∧R) 2,5及基本蕴含公式
（2）├ (P→(Q→R))? ((P∧Q) →R)
P→(Q→R) 前提引入规则
(P∨(Q→R) 1及基本等价公式
(P∨((Q∨R) 2及基本等价公式
(P∨(Q∨R 3及基本等价公式
((P∧Q)∨R 4及基本等价公式
(P∧Q) →R 5及基本等价公式
（3）P(a,b) ∧((X)( ((y)P(Y,X) ∨P(X,Y) →P(X,X)) ├P(a,a)
合取因子：P(a,b) (P(y,x)∨P(x,x),(P(x,y)∨P(x,x) (P(a,a)
(P(x,y)∨P(x,x) 前提引入规则
(P(a,b)∨P(a,a) 1及全称量词消去规则
(P(a,a) 前提引入规则
(P(a,b) 3及基本等价公式
P(a,b) 前提引入规则
NIL 4,5归结
六、W={a0,s1,s2,s3} R={<s0,s1>,<s0,s2>,<s1,s0>,<s1,s3>,<s2,s1>,<s3,s3>} L(s0)={p},L(s1)={p,q},L(s2)={p,r}，L(s3)={q}
E○p,s0 s1 s2成立 s3不成立
Ap:( s0 s1 s2 s3 均不成立
E?(Ep),s0 s1( s2成立 s3不成立七、模式定义:
（1）
---------ΔLogSys----------------
registry,registry’,P User
login,login’,P User
---------------------------------------------
login?registry
login’?registry’
----------------------------------------------
---------ΞLogSys----------------
ΔLogSys
---------------------------------------------
registry= registry’
login= login’
---------------------------------------------
---------InitLogSys----------------
registry’,P User
login’,P User
---------------------------------------------
registry’={ }
login’={ }
---------------------------------------------
（2）
---------RegistrySys---------------------
ΔLogSys
name?,seq Char
password?,seq Char
---------------------------------------------
registry’= registry∪{name? ( password?}
login’=login
---------------------------------------------
（3）
---------LogoutSys-----------------------
ΔLogSys
name?,seq Char
---------------------------------------------
login’= {name}login
---------------------------------------------
模拟试题二
《软件形式化方法》期末考试试题
（120分钟）
题号
一
二
三
四
五
六
七
总分
题分
得分
一、填空题。（20分）
1,软件危机是指在计算机软件的开发和维护过程中所遇到的一系列严重的问题，其产生的原因主要包括：,,,；其本质特征是软件的 和 。
2,形式化方法研究如何把（具有清晰数学基础的）严格性（描述形式、技术和过程等）融入软件开发的各个阶段；包括形式化规格,和 三种活动，在软件开发的形式化规格中包含的三种规格为,和 。
3,Petri网适合于描述并发、异步、分布式软件系统规格，是由,和 三个部分组成；特殊的Petri网类型中,和 不能描述冲突,允许冲突和并发同时存在,可以用来描述非对称类型的混惑关系。
4,模式是Z语言规格中一个重要的元素，模式包含和模式连接的前提条件是,即不同模式中 是相同的。
二、构造有限状态机，使其接受的语言为由0和1构成的字符串的集合，分别满足下列条件。（10分）
（1）每个字符串以00结束。
（2）每个字符串中有3个连续的0出现。
三、对图中所示Petri网进行化简。（10分）
四、构造下述系统过程的CSP进程。（10分）
银行的每个客户先开设（open）一个账户，然后该客户就可以多次执行存（deposit）或取（withdraw）操作，最终还可能终止（terminate）该账户。假定不考虑客户每次存或取得款项数目，也不考虑透支的情况。
五、逻辑演算证明。（15分）
（1）(P∨Q) ∧(P∨R)├ P∨ (Q∧R)
（2）P∧(Q?R)├ (P∧Q)?(P∧R)
（3）├ ((x)(P(X) →((Y)P(Y))
六、对于图中所示的Kripke结构，写出其对应的三元组形式，并分别在状态s0，s1，s2，s3下考察下述CTL公式是否成立。（20）
（1）A○p
（2）Ep(
（3）A(p?q)
七、在教材7.3节中描述的电话号码系统中增加下列操作，给出完整的操作模式。（15）
（1）收回电话（RemoveEntry）：收回已经分配给某人的电话；
（2）查询电话用户（FindNames）：查询指定号码的电话用户；
（3）更改电话号码（ChangeEntry）：更改某个用户的电话号码。
参考答案与答题要点一、填空题
1,软件开发成本高 速度缓慢甚至延迟 软件运行的质量差 可靠性难以得到保证 复杂性 多样性
2,形式化验证 程序精化 行为规格 设计规格 程序规格
3,位置 迁移 流关系 状态机 标记图 自由选择网 非对称的自由选择网
4,模式兼容 同一变量的类型二,（1）
（2）
三,（1）
（2）
四、 BANK=open->(x:{deposit,withdraw}(OPER(x))(terminate;
OPER(deposit)=(deposit(STOP);
OPER(withdraw)=(withdraw(STOP)。
五、（1）(P∨Q) ∧(P∨R)├ P∨ (Q∧R)
P∨Q 前提引入规则
P∨R 前提引入规则
P∨ (Q∧R) 1,2及基本蕴含公式
（2）P∧(Q?R)├ (P∧Q)?(P∧R)
Q?R 前提引入规则
(Q∧R)∨(?Q∧? R) 1及基本等价公式
(?Q∨R) ∧(Q∨? R) 2及基本等价公式
P,?Q∨R,Q∨? R 3及前提引入规则
P∧Q 假设前提引入
Q 5及基本蕴含公式
R 4,6及基本蕴含公式
P∧R 4,7及基本蕴含公式
(P∧Q) →(P∧R) 5,8归结
P∧R 假设前提引入
R 10及基本蕴含公式
Q 4,11及基本蕴含公式
P∧Q 4,12及基本蕴含公式
(P∧R) →(P∧Q) 5,8归结
(P∧Q)?(P∧R) 9,14归结
（3）├ ((x)(P(X) →((Y)P(Y))
((x)(P(X) →((Y)P(Y)) 前提引入规则
((x)P(X)∨((Y)P(Y) 1及基本蕴含规则
((x)?P(X)∨((Y)P(Y) 2及量词转换规则
((x) (?P(X)∨P(X)) 3及全称量词消除规则
P(a)∨P(a) 4及全称量词消除规则
T 5及基本等价公式
六、W={a0,s1,s2,s3} R={<s0,s1>,<s0,s2>,<s1,s0>,<s1,s3>,<s2,s1>,<s3,s3>} L(s0)={p},L(s1)={p,q},L(s2)={p,r}，L(s3)={q}
A○p：s0,s2成立 s1,s3不成立
Ep(：s0,s1,s2成立 s3不成立
A(p?q)：s0,s1,s2,s4成立七、模式定义:
（1）
---------RemoveEntry----------------
PhoneDB
name?,Person
---------------------------------------------
name? ∈dom hasphone
hasphone’= {name?}hasphone
---------------------------------------------------------
（2）
---------FindNames----------------
=PhoneDB
number?,Phone
---------------------------------------------
number? ∈ran hasphone
name!= hasphone-1 (|{number}|)
----------------------------------------------------------------------------
（3）
---------ChangeEntry----------------
PhoneDB
name?,Person
newnumber?,Phone
---------------------------------------------
name? ∈dom hasphone
hasphone’=( {name?}hasphone)∪{name? (newnumber?}
----------------------------------------------------------------------------
模拟试题三
《软件形式化方法》期末考试试题
（120分钟）
题号
一
二
三
四
五
六
七
总分
题分
得分
一、填空题。（20分）
1,软件危机是指在计算机软件的 过程中所遇到的一系列严重的问题，应对软件危机的方式分为两种方法,和 。对于软件开发组织和管理的规范化方法中，主要研究,和 三个要素。
2,形式化方法研究如何把（具有清晰数学基础的） （描述形式、技术和过程等）融入软件开发的各个阶段；包括,形式化验证和程序精化三种活动。形式化验证主要技术包含 和 ；程序精化是将 与 相结合，研究从抽象的 推演出具体的面向计算机的 。
3,模式是Z语言规格中一个重要的元素，模式是由,和
组成。
4,Larch方法是软件系统规格的一种 ；Larch方法的程序规格包括 和与目标语言相关的 两个部分。
二、利用有限状态机描述“AB协议”。（15分）
AB协议包含发送端和接收端两个实体。发送端协议实体从发送方用户获取一个报文，将序号寄存器值赋给报文，然后向接收端协议实体发出报文，发送方发出报文之后启动超时时钟，等待认可报文。如果在给定的时间内未收到认可报文，则重发报文；如果收到认可报文，其序号与发出报文序号相同，则发送端实体从发送方用户获取下个报文。接收端协议实体在收到报文之后，如果报文无错误，则想发送端实体发送认可报文，然后将报文递交给接收方用户；如果接收的报文有错误或者序号不正确，则丢失报文。假定所用通道不会中断；报文重复n次后最终能够被接收；认可报文只要发出就能正确收到；报文不会损坏；序号寄存器初始化为0 。
三、构造下图所示Petri网的覆盖树。（10分）
四、利用CSP对“生产者-消费者”系统进行规格。（10分）
五、逻辑演算证明。（15分）
（1）((Q∨R) ∧(P(Q)├(P
（2）(P((Q(S)) ∧ ((R∨P) ∧Q├ R→S
（3）((x)P(x)(((x)(P(x)(Q(x)(R(x)),((x)P(x),((x)Q(x)├ R(a)(R(c)
六、如图中所示的Kripke结构，利用标号算法对公式进行模型检验。（15）
（1）E((p ∧r)?p)
（2）A(p?q) = (E(((p?q))
七、对于哲学家就餐问题，利用CTL描述下述性质。（15）
（1）相邻的两个哲学家不能同时都在用餐；
（2）一个哲学家只要处于等待用餐状态，就可以最终进入用餐状态；
（3）存在一个状态使得该状态下每个哲学家都拿起一把叉子。
参考答案与答题要点一、填空题
1,开发和维护 软件工程 软件形式化 方法 工具 过程
2,严格性 形式化规格 模型检验 定理证明 自动推理 形式化方法形式规格 程序代码
3,模式的名字 声明/说明部分 断言/谓词部分
4,双层规格方法 Larch共享语言 Larch接口语言
二、发送端：{持有报文Shold，等待认可Swait，收到应答Sack}
接收端：{等待报文Rwait，报文正确Rtrue，报文错误Rerror}
计时器：{启动Tstart，停止Sstop，超时Sover}
三,覆盖树：
四、 P<x>=produce?x(write!x ;
C<x>=read?x(consume!x ;
B=P<x>(P<y>|(C<x>(B),
五、（1）((Q∨R) ∧(P(Q)├(P
((Q∨R) ∧(P(Q) 前提引入规则
(Q∧(R 1及基本等价公式
(P∨Q 1及基本等价公式
(Q 2及基本蕴含公式
(P 3,4及基本蕴含公式
（2）(P((Q(S)) ∧ ((R∨P) ∧Q├ R→S
(R∨P 前提引入规则
R(P 1及基本等价公式
R 结论引入规则
P 2,3及基本蕴含公式
P((Q(S) 前提引入规则
Q(S 4,5及基本蕴含公式
Q 前提引入规则
S 6,7及基本蕴含公式
（3）((x)P(x)(((x)(P(x)(Q(x)(R(x)),((x)P(x),((x)Q(x)├ R(a)(R(c)
((x)P(x)(((x)(P(x)(Q(x)(R(x)) 前提引入规则
P(a)(((z)(P(z)(Q(z)(R(z)) 1及存在量词消去规则
((x)P(x) 前提引入规则
P(a) 3及存在量词消去规则
((x)Q(x) 前提引入规则
Q(c) 5及存在量词消去规则
((z)(P(z)(Q(z)(R(z)) 2,4及基本蕴含公式
P(a)(Q(a)(R(a) 7及z/a
P(c)(Q(c)(R(c) 7及z/c
R(a) 4,8及基本蕴含公式
R(c) 6,9及基本蕴含公式
R(a)(R(c) 10,11及基本蕴含公式
六、（1）E((p∧r)?p)
（2）A(p?q) = (E(((p?q))
七、CTL描述:
（1）A((((Pi=eating)((Pi+1=eating)) i=0,1,2,3,4 P5=P0
（2）A( ((Pi=waiting)(A◇(Pi=eating))
（3）E◇(Pi=forking)
