1、程序设计理论各年试题参考答案 Made by 林祺颖 试题预测 （这些为本人意见 ，仅供参考 ） ： 题目前有 #为考试必考内容，即类似的题目一定会出，一定要灵活掌握。 题目前没有符号的为可能考内容，一定要知道怎样做。 题目前有 *符号的为基本不考内容，浏览一下即可。 答案参考（如有任何补充或者感觉不对的地方 ，一定要向我提出来噢） ： 黑色的 为个人 感觉没有问题的部分，如果发现有错误， 那一定要跟我说。 红色 的为个人感觉可以修改或者不确定，甚至不太会做的部分，大家一起讨论。 绿色 的为提示或者需要注意的部分。 联系方式：在群上 找林祺颖，或者加 QQ： 1238260，我基本都在。 下面
2、有些符号为了录入方便，都作了一些替代，标准符号可要看书。如 用 w 代替。 程序设计理论试题 2004 年 01 月 06 日 该卷 答案基本是一个师兄做的， 红色为我补充的部分 1. Show that (P(Nat), ) is not a Well-founded Set, but(S|S is a finite subset of Nat, ) is a well-founded set 解释： P(Nat)为自然数集合的集合。即 Nat 的 Power Set。 取第 1 个集合为 Nat, 第 2 个集合为 Nat-1, 。 ,第 n 个集合为 Nat-1,2,.n-1,则可以产生
3、一个 infinite descending sequence（ 无穷递降序列 ） , 所以 (P(Nat), )不是 Well-founded Set. 设 T=S|S is a finite subset of Nat, 若 (T, )不是 Well-founded Set,则必然存在一个 infinite descending sequence, 设为 a1,a2,an, 则 a1 a2 an , 从而 |a1|a2|an|., 因为 ai 属于 T(i=1),即 ai 是一个有限集，所以 |ai|是一个有限的 自然数， |ai|不能形成一个无限下降的序列，矛盾，所以 (T, )是 We
4、ll-founded Set. 2. Show that for all formulas w1 and w2, the formula w1 w2 and w1 w2 and logically equivalent. 证明 w1w2 与 w1 w2 逻辑等价，即是要证明 |= w1w2 w1 w2. 对于任意的Interpretation I, I(w1w2 w1 w2)() 等价于 I(w1)()I(w2)() I(w1)() I(w2)(), 因为 w1,w2:Bool, 所以 I(w1)()=true 或者 I(w1)()=false, I(w2)()=true 或者I(w2)()=
5、false。 若 I(w1)()=true, I(w2)()=true, 则 I(w1w2 w1 w2)() = (truetrue true true)=true;其余三种情况类似地也有 I(w1w2 w1 w2)() true. 所以 |= w1w2 w1 w2, 从而 w1w2 与 w1 w2 逻辑等价。 *3. Consider evaluation of the logic expressions with only operators go to l1; 则定义 wlp(a,p)= tnt xnxr,.,1,.,1 ; 如果是条件转移语句，设形式如下所示 : l0: if e th
6、en goto l else goto l fi; 则定义 wlp(a,q)如下 : e r 如果 l1=l 且 l1l e r 如果 l1l且 l1=l (ii) 定义 partial correctness 的验证条件 vc(p,a,q)为 p wlp(a,q). 令 B 为谓词逻辑的 basis, p,q 为 WFFB的两个公式， S BL1 是一个 flowchart 程序，对于任意的 Interpretation I, 程序 S 在 Interpretation I 中，对于 p 和 q 是 partial correct 的，当且仅当如果对于 S 中的任意一条路径 a, 都有验证条
7、件 vc(p,a,q) 在 I 中为 valid。 #8.Show that the following is a correct inference rule in Hoare logic using construction sequence in “Inductive Definition of Sets”. What are B and K in this context? And what is the inductively defined set in the context? , , ( ) w h i l e e d o S o d q p r r e S r r e qp
8、for all p,q,r WFFB, e QFFB, and S L2B. 设 WFFB为 well-formed formula 的集合 B= txp x:=tp | p WFFB,x V, t TB K= ( (pr, r eSr, (r e)q ) , pwhile e do S od q)| p,q,r WFFB,e QFFB,S BL2 推导出来的集合是 Hoare calculus 里面 logically valid 的公式集的一个子集。 推导过程： P-r reS1r r e-q rwhile e do S1 od r e pwhile r do S1 od q 程序设计理论
9、试题 2000.1.22（即老师的样题） 1. 1-in0,N a tnN a tnin!)(,:,| ，或者wnnwnfN a tN a tfN a tifS iwwii 试指出 链 S 在 Natw-Natw 上的最小上界。 有些人说 论域 就是 CPO。 对于该题，由于 Nat，且 (+)(a,b) ()=a+b, *为 Nat2-Nat，且 (*)(a,b) ()=a*b， Bool，且 (，有 =， 且 S2 为 a. S;S1 当 (e)()=true b. S 当 (e)()=false 当 S1 为 While e do S od 时， 有 =，且 S2 为 a. S 当 (e
10、)()=true b. 当 (e)()=false #9 当使用通常解释 I 时，有 F(2)= if 2=0 then 1 else 2*F(2-1) fi = if false then 1 else 2*F(1) fi = 2*(if 1=0 then 1 else 1*F(1-1) fi) =2*(if false then 1 else 1*(F(0) fi) =2*1*(F(0) =2*(if 0=0 then 1 else 0*F(0-1) fi) =2*1=2 F(-2)由于不可终止，所以 F(-2)未定义 #10 Vc(q,(test,loop,upd,test),q) q-
11、wlp(test,loop,upd,test),q) wlp(test,q)=q wlp(upd,test),q)=q(y3+y2/y3) wlp(loop,upd,test),q)=q(y3+y2/y3)(y1+1,y2+2/y1,y2) wlp(test,loop,upd,test),q)=(y3 (x=a (y1+1)2(x=a (y1+1)2r reS1r r-e-q r while e do S1 od r-e p while e do S1 od q （可看书 P153） 程序设计理论期末练习题 1. 可参考 老师样题的第 6 题。 *2. 这题很难写。先给个思路： 第一要 建立一
12、个 well-founded set（自然数集），并且需要 最小值为 0。然后 证明对于 x0，每次的计算都 是递减。然后下结论。 #3. 参考书本 P50。 #4. F(x) Nat)-Nat 的函数，并设为 G。 则 G(op) =F(3,x)( F/op)=op(3,4) 则 (F.F(3,x)(*)()=3*4=12。 可看书 P95。 t f 程序设计理论期末考试 (99) 这年考试题目侧重于概念，与之后几年的题目有很大的区别 *1. 问得真直接。不好做。 指称语义：定义了基类，然后由基类影射 到相应的函数，然后由函数 来定义其语义。 操作语义： 定义了抽象机，然后及其相关操作。由抽
13、象机的运行和状态来反映其语义。 异： 指称语义表示的语言要比操作语义要多。 指称语义重点在指称上， 即所对应的函数上。而操作语义的重点在 于抽象机的运行及其状态。 *2. 使用 CPO 的目的是最终能够归到基类， 并且能够归到 F 和 V 这两个最基本的类型。 最小元表示函数影射的开始，也就是寻找对应的语义中的最小语义单位。 Chain 就是其影射过程，也即对应的语义解释过程。 *3. Imperative Language:即命令方式语言。 Algol-Like 语言。 该类语言通过各种相对独立的语句， 语句自身是不会直接或间接调用自己， 可以通过 独立地对每条 语句的解释来进行语义分析。
14、Declarative Language 即声明方式语言。 Lisp-Like 语言。 该类语言使用声明性语句，语句自身会直接或者间接调用自己， 通过对多个变量的映射关系， 来最终确认其对应的语义。 *4个人感觉是正确的。因为如果程序的语义脱离了形式系统， 那么程序的语义就不能解释或者不可理解了。 而程序的正确性也不可验证了。 5. 参考 老师样题。 6. 参考 老师样题。 7. 参考课本 P50。 数据不同，最后结果为 (,(5,2,5,9) *8. 书本 P25。 简单来说就是一个解释 ， (w)()=true,则 为 W 的 Model。 9 Complete。因为定义了一个 ，即每个
15、chain 都存在 lub。 这里要提出一个， R+ 也 是 CPO。 有人提出 链： 1.1， 1.11， 1.111 ，没有 Lub。其实是有的， 。即 11.,911lub 10. M(S)=x mod 2. 11 部分正确性是基于程序 对输入 有 定义下的正确性 ，即程序对合法 的输入是正确的 。而完全正确性是需要证明其程序 对输入 有定义的 ，即程序对于输入是正确的，并且可以终止的 。 基于谓词的正确性 是证明给定的谓词是正确的。 基于公式的正确性是证明公式的守恒。 12 Partial Correct: i:说明程序是 无论有没定义都部分正确 。 Ii:说明程序是处处都没有定义。
16、Terminate: 程序处处有定义。 13. 程序输入是 x=y，输出是 x=y!，所以最后的结果一定是让 x 为 y！， y 在程序中可变 （改变以后可以归回原来的值） ，但最后的结果必定要让 x=y!。 并且 y 要等于原值才是计算阶乘的程序。 14.为了保证每条路径都遍历，即程序的运行情况都可保证。 15. (pSq)()=true iff If (p)()=true and if M(S)() is defined, Then (q)(M(S)()=true. 看书 P150。 程序设计理论期末考试 (2000) 1. 想不到其他方法。用定义证明。 2. 麻烦。直接证。 不写了。 3
17、. i:说明程序是处处都没有定义。 ii:说明程序是无论有没定义都部分正确。 iii. 同 ii iv.同 ii v. 程序处处有定义。 vi. 说明程序是无论有没定义都可终止。 4 程序的执行就是对机器的操作， 即由一种状态转换到另外一种状态。 程序状态 :是程序真实的状态，与机器无关。 机器状态 :机器状态反映了程序状态。 5.输入即 x=2,y=2,z=2 输出要符合 x=2*y y=4*z， 可能的输出为 x=16 y=8 z=2 由于 这题没说中间的结果， z 的值可以改变，所以答案也可以是 8,4,1。甚至 24,12,3 都可以。反正满 足最后的条件就可以了。 6 状态是由 (l
18、1, 1)转换到 (l2, 2) (1)2=1x/0 (2)2=1x/x+1 (3)2=1x,y/y,x (4)定义 l1 下一指令为 l1,再下一指令为 l1. 2=1 且 l2=l1 if x!=0 l2=l1 if x=0 7.老师样题。 8. 1=(begin,3,6,end) wlp:m1 相等 由 continuous 定义可知 ，相等。 相等 -Continuous 由 Continuous 定义可知。书 P77。 (b)不会做。 10.类似于作业。可推出 Refutation。 下面是作业的解答。 :-f(2,2,x) (3) =(m/2,n/2,y/y1) :-f(2,1,y1),f(1,y1,x) (3) =(m/2,n/1,x/y1,y/y2) :-f(2,0,y2),f(1,y2,y1),f(1,y1,x) (2) =(m/2,x/y2) :-f(1,1,y2),f(1,y2,y1),f(1,y1,x) (3) =(m/1,n/1,x/y2,y/y3)
