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,则可以产生一个 infinite descending sequence
3、（无穷递降序列）, 所以(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, )是 Well-founded Set.2. Show that for all formul
4、as w1 and w2, the formula w1 w2 and w1 w 2 and logicallyequivalent.证明 w1w2 与 w1w2 逻辑等价，即是要证明|= w1w2 w1w2. 对于任意的Interpretation I, I(w1w2 w1w2)() 等价于 I(w1)()I(w2)() I(w1)()I(w2)(), 因为 w1,w2:Bool, 所以 I(w1)()=true 或者 I(w1)()=false, I(w2)()=true 或者 I(w2)()=false。若 I(w1)()=true, I(w2)()=true, 则 I(w1w2 w1w
5、2)() = (truetrue truetrue)=true;其余三种情况类似地也有 I(w1w2 w1w2)()true.所以|= w1 w2 w1w2, 从而 w1w2 与 w1w2 逻辑等价。*3. Consider evaluation of the logic expressions with only operators goto l1;则定义 wlp(a,p)= ;tnxr,.1如果是条件转移语句，设形式如下所示:l0: if e then goto l else goto l fi;则定义 wlp(a,q)如下: e r 如果 l1=l 且 l1le r 如果 l1l 且 l
6、1=l(ii) 定义 partial correctness 的验证条件 vc(p,a,q)为 p wlp(a,q).令 B 为谓词逻辑的 basis, p,q 为 WFFB 的两个公式，S 是一个 flowchart 程序，对于BL1任意的 Interpretation I, 程序 S 在 Interpretation I 中，对于 p 和 q 是 partial correct 的，当且仅当如果对于 S 中的任意一条路径 a, 都有验证条件 vc(p,a,q) 在 I 中为 valid。#8.Show that the following is a correct inference ru
7、le 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?,() while doS qprrefor all p,q,rWFF B, eQFF B, and SL 2B.设 WFFB 为 well-formed formula 的集合B= x:=tp | pWFFB,xV, tTBtxK= ( (pr, reSr,
8、 (r e)q ) , pwhile e do S od q)|p,q,rWFF B,eQFF B,S L2推导出来的集合是 Hoare calculus 里面 logically valid 的公式集的一个子集。推导过程：P-rreS1rr e-qrwhile e do S1 od r epwhile r do S1 od q程序设计理论试题 2000.1.22（即老师的样题）1. 1-in0,Natat!)(,:,| ，或 者wnfNattfatifSiwi试指出链 S 在 Natw-Natw 上的最小上界。有些人说论域就是 CPO。对于该题，由于Nat，且 (+)(a,b) ()=a+b
9、, *为 Nat2-Nat，且 (*)(a,b) ()=a*b，Bool，且 (，有 =， 且S2 为 a. S;S1 当 (e)()=trueb. S 当 (e)()=false当 S1 为 While e do S od 时，有 =，且S2 为 a. S 当 (e)()=trueb. 当 (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 els
10、e 1*(F(0) fi)=2*1*(F(0)=2*(if 0=0 then 1 else 0*F(0-1) fi)=2*1=2F(-2)由于不可终止，所以 F(-2)未定义#10Vc(q,(test,loop,upd,test),q)q-wlp(test,loop,upd,test),q)wlp(test,q)=qwlp(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)2rreS1rr-
11、e-qr while e do S1 od r-ep while e do S1 od q（可看书 P153）程序设计理论期末练习题1. 可参考老师样题的第 6 题。*2. 这题很难写。先给个思路：第一要建立一个 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。程序设计理论期末考试(99)这年考试题目侧重于概念，与之后
12、几年的题目有很大的区别*1. 问得真直接。不好做。指称语义：定义了基类，然后由基类影射到相应的函数，然后由函数来定义其语义。操作语义：定义了抽象机，然后及其相关操作。由抽象机的运行和状态来反映其语义。异：指称语义表示的语言要比操作语义要多。指称语义重点在指称上，即所对应的函数上。而操作语义的重点在于抽象机的运行及其状态。*2. 使用 CPO 的目的是最终能够归到基类，并且能够归到 F 和 V 这两个最基本的类型。最小元表示函数影射的开始，也就是寻找对应的语义中的最小语义单位。Chain 就是其影射过程，也即对应的语义解释过程。*3. Imperative Language:即命令方式语言。Al
13、gol-Like 语言。该类语言通过各种相对独立的语句，语句自身是不会直接或间接调用自己，可以通过独立地对每条语句的解释来进行语义分析。Declarative Language 即声明方式语言。 Lisp-Like 语言。该类语言使用声明性语句，语句自身会直接或者间接调用自己，通过对多个变量的映射关系，来最终确认其对应的语义。*4个人感觉是正确的。因为如果程序的语义脱离了形式系统，那么程序的语义就不能解释或者不可理解了。而程序的正确性也不可验证了。5. 参考老师样题。6. 参考老师样题。7. 参考课本 P50。数据不同，最后结果为 (,(5,2,5,9)*8. 书本 P25。简单来说就是一个解
14、释 ，(w)()=true,则 为 W 的 Model。9Complete。因为定义了一个，即每个 chain 都存在 lub。这里要提出一个，R +也是 CPO。有人提出链：1.1，1.11，1.111，没有 Lub。其实是有的，。即 1.,9lub10. M(S)=x mod 2.11部分正确性是基于程序对输入有定义下的正确性，即程序对合法的输入是正确的。而完全正确性是需要证明其程序对输入有定义的，即程序对于输入是正确的，并且可以终止的。基于谓词的正确性是证明给定的谓词是正确的。基于公式的正确性是证明公式的守恒。12Partial Correct: i:说明程序是无论有没定义都部分正确。
15、Ii:说明程序是处处都没有定义。Terminate: 程序处处有定义。13. 程序输入是 x=y，输出是 x=y!，所以最后的结果一定是让 x 为 y！，y 在程序中可变（改变以后可以归回原来的值） ，但最后的结果必定要让 x=y!。并且 y 要等于原值才是计算阶乘的程序。14.为了保证每条路径都遍历，即程序的运行情况都可保证。15. (pSq)()=true iffIf (p)()=true and if M(S)() is defined,Then (q)(M(S)()=true.看书 P150。程序设计理论期末考试(2000)1. 想不到其他方法。用定义证明。2. 麻烦。直接证。不写了。
16、3. i:说明程序是处处都没有定义。 ii:说明程序是无论有没定义都部分正确。iii. 同 ii iv.同 iiv. 程序处处有定义。 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状态是由(l1, 1)转换到(l2, 2)(1)
17、2=1x/0(2)2=1x/x+1(3)2=1x,y/y,x(4)定义 l1 下一指令为 l1,再下一指令为 l1.2=1 且l2=l1 if x!=0l2=l1 if x=07.老师样题。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)
