程序设计理论各年试题参考答案文档格式.docx

1、证明w1w2与w1w2逻辑等价，即是要证明|= w1w2w1w2. 对于任意的Interpretation I, I（w1w1w2）（） 等价于 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（w1w1w2）（） = （truetrue truetrue）=true;其余三种情况类似地也有I（w1w1w2）（）true.所以|= w1w1w2, 从而w1w1w2逻辑等价。*3

2、. Consider evaluation of the logic expressions with only operators &,| and | in C programming language. Construct an abstract machine for evaluation of the expressions and try to define the meaning function M（e） : for any given expression e.这题不会写。师兄也没给出答案。_题目意思是，对于一个只有&,|,|操作的C语言逻辑表达式，建立起抽象机，并且给出对于给

3、定的表达式e，给出对应的meaning function M（e） :的定义#4. Present the partial order （） graphically. How many elements does it have? How many elements are maximal?这是一个定义在由Bool映射到Bool的函数的偏序集。并且是具有=关系，所以某些映射是不能成立的，如（,ture）,（true, ）.BoolBool共有11个元素，用ai（1=i（if 2=0 then 1 else 2*F（2-1）fi） =（if false then 1 else 2*F（1） fi

4、） （2=0,false）,（2-1,1）2*F（1） （if false then 1 else 2*F（1） fi, 2*F（1）2*（if 1=0 then 1 else 1*F（1-1） fi）2*（if false then 1 else 1*F（0） fi） （1=0,false）,（1-1,0）2*（1*F（0） （if false then 1 else 1*F（0） fi, 1*F（0）2*（1*1） （F（0）,1）2 （2*（1*1）,2）（b）对应逻辑程序如下:F（0,1）.F（x,n）F（x-1,m）,n=x*m目标是 F（2,x）这里要注意，最后会出现不为空的情况（

5、即不是Refutation），有一种理解是具有默认的式子：true:-. 另一种是需要加式子m:-（c）逻辑程序的derivation: G P F（2,x） F（x1,n1）F（x1-1,m1）,n1=x1*m1 x1/2,n1/x= F（1,m1）,x=2*m1 F（x2,n2）F（x2-1,m2）,n2=x2*m2 x2/1,n2/m1 F（0,m2）,m1=1*m2,x=2*m1 F（0,1） m2/1 m1=1*m2,x=2*m1 m1=2, x=4 再根据true:-和替换（m1/2,x/4），可以归到。6. Give an example of a functional prog

6、ram for which the semantic functional is the identity function. Explain why?假设在Usual Interpretation I=（Nat,I0）下，定义函数程序为:F（x） 0时，设=（l1,l2,lk）, r=wlp（,p）, 根据l0处的语句类型，分成两种情况来定义wlp（a,p）. 如果是平行的赋值语句，设形式如下所示:l0: （x1,x2,xn）:=（t1,t2,tn）; goto l1;则定义wlp（a,p）=; 如果是条件转移语句，设形式如下所示: l0: if e then goto l else got

7、o l fi; 则定义wlp（a,q）如下: e r 如果l1=l且l1ler 如果l1l且l1=l（ii） 定义partial correctness的验证条件vc（p,a,q）为 pwlp（a,q）. 令B为谓词逻辑的basis, p,q为WFFB的两个公式，S是一个flowchart程序，对于任意的Interpretation I, 程序S在Interpretation I中，对于p和q是partial correct的，当且仅当如果对于S中的任意一条路径a, 都有验证条件vc（p,a,q） 在I中为valid。#8.Show that the following is a correc

8、t 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?for all p,q,rWFFB, eQFFB, and SL2B.设WFFB为well-formed formula的集合B=x:=tp | pWFFB,xV, tTBK= （ （pr, reSr, （re）q ） , pwhi

9、le e do S od q）|p,q,rWFFB,eQFFB,S 推导出来的集合是Hoare calculus里面logically valid的公式集的一个子集。推导过程：P-rreS1rre-qrwhile e do S1 od repwhile r do S1 od q程序设计理论试题 2000.1.22（即老师的样题）1.试指出链S在Natw-Natw上的最小上界。有些人说论域就是CPO。对于该题，由于Nat，且（+）（a,b） （）=a+b, *为Nat2-Nat，且（*）（a,b） （）=a*b，Bool，且（=）（a,b） （）=a=b该公式的语义为（Vx.（0=x）=true

10、 iff 所有的x属于Nat，（=）（0,x） （）=true，即0小于等于x（不建议写成x大于等于0）。7（P（3,1）= （y:=1;if y=1 then x:=1 else x:=2 fi）（3,1） =（if y=1 then x: =（if true then x: =（x:=1）（3,1） =（1,1）#8. 对于格局（S1，），并对格局（S1，）转移到（S2，）,有： 当S1为while e do S od ;S 时，S，有=， 且 S2为a. S;S1 当（e）（）=trueb. S 当（e）（）=false当S1为While e do S od 时，有=，且 S2为a. S

11、 当（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 else 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

12、,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=c y3+y2+2=（y1+1+1）2 y2+2=2*（y1+1）+1）vc（）=（x=a y12=x y3=（y1+1）2 y2=2*y1+1 y3（x=a （y1+1）2r-e-r while e do S1 od r-ep while e do S1 od q（可看书P153）程序设计理

13、论期末练习题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）这年考试题目侧重于概念，与之后几年的题目有很大的区别*1. 问得真直接。不好做。指称语义：定义了基类，然后由基类影射到相应的函数，然后由函数来定义其语义。操作语义：定义了抽象

14、机，然后及其相关操作。由抽象机的运行和状态来反映其语义。异：指称语义表示的语言要比操作语义要多。指称语义重点在指称上，即所对应的函数上。而操作语义的重点在于抽象机的运行及其状态。*2. 使用CPO的目的是最终能够归到基类，并且能够归到F和V这两个最基本的类型。最小元表示函数影射的开始，也就是寻找对应的语义中的最小语义单位。Chain就是其影射过程，也即对应的语义解释过程。*3. Imperative Language:即命令方式语言。Algol-Like语言。该类语言通过各种相对独立的语句，语句自身是不会直接或间接调用自己，可以通过独立地对每条语句的解释来进行语义分析。Declarative

15、Language即声明方式语言。Lisp-Like语言。该类语言使用声明性语句，语句自身会直接或者间接调用自己，通过对多个变量的映射关系，来最终确认其对应的语义。*4个人感觉是正确的。因为如果程序的语义脱离了形式系统，那么程序的语义就不能解释或者不可理解了。而程序的正确性也不可验证了。5. 参考老师样题。6. 参考老师样题。7. 参考课本P50。数据不同，最后结果为 （,（5,2,5,9）*8. 书本P25。简单来说就是一个解释，（w）（）=true,则为W的Model。9Complete。因为定义了一个，即每个chain都存在lub。这里要提出一个，R+也是CPO。有人提出链：1.1，1.1

16、1，1.111，没有Lub。其实是有的，10. M（S）=x mod 2.11部分正确性是基于程序对输入有定义下的正确性，即程序对合法的输入是正确的。而完全正确性是需要证明其程序对输入有定义的，即程序对于输入是正确的，并且可以终止的。基于谓词的正确性是证明给定的谓词是正确的。基于公式的正确性是证明公式的守恒。12Partial Correct: i:说明程序是无论有没定义都部分正确。 Ii:说明程序是处处都没有定义。Terminate: 程序处处有定义。13. 程序输入是x=y，输出是x=y!，所以最后的结果一定是让x为y！，y在程序中可变（改变以后可以归回原来的值），但最后的结果必定要让x=