程序设计理论各年试题参考答案文档格式.docx
《程序设计理论各年试题参考答案文档格式.docx》由会员分享，可在线阅读，更多相关《程序设计理论各年试题参考答案文档格式.docx（18页珍藏版）》请在冰点文库上搜索。
证明w1à
w2与
w1∨w2逻辑等价，即是要证明|=w1à
w2
w1∨w2.对于任意的InterpretationI,I（w1à
w1∨w2）（σ）等价于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（w1à
w1∨w2）（σ）=（trueà
true
true∨true）=true;
其余三种情况类似地也有I（w1à
w1∨w2）（σ）＝true.
所以|=w1à
w1∨w2,从而w1à
w1∨w2逻辑等价。
*3.Considerevaluationofthelogicexpressionswithonlyoperators&
&
|and||inCprogramminglanguage.ConstructanabstractmachineforevaluationoftheexpressionsandtrytodefinethemeaningfunctionM（e）:
foranygivenexpressione.
这题不会写。
师兄也没给出答案。
^_^
题目意思是，对于一个只有&
|,||操作的C语言逻辑表达式，建立起抽象机，并且给出对于给定的表达式e，给出对应的meaningfunctionM（e）:
的定义
#4.Presentthepartialorder（
）graphically.Howmanyelementsdoesithave?
Howmanyelementsaremaximal?
这是一个定义在由Boolω映射到Boolω的函数的偏序集。
并且是具有<
=关系，所以某些映射是不能成立的，如{（ω,ture）,（true,ω）..}
Boolω
Boolω共有11个元素，用ai（1<
=i<
=11）表示如下:
a1:
{（ω,ω）,（true,ω）,（false,ω）}a2:
{（ω,ω）,（true,ω）,（false,true）}
a3:
{（ω,ω）,（true,ω）,（false,false）}a4:
{（ω,ω）,（true,true）,（false,ω）}
a5:
{（ω,ω）,（true,true）,（false,true）}a6:
{（ω,ω）,（true,true）,（false,false）}
a7:
{（ω,ω）,（true,false）,（false,ω）}a8:
{（ω,ω）,（true,false）,（false,true）}
a9:
{（ω,ω）,（true,false）,（false,false）}
a10:
{（ω,true）,（true,true）,（false,true）}
a11:
{（ω,false）,（true,false）,（false,false）}
a5
a2a6
a3a8
a1
a4a10
a7a11
a9
共有4个极大元。
#5.Designalogicprogramwithanequivalentmeaningasthefollowingfunctionalprogram:
F（x）
if（x=0）then1elsex*F（x-1）fi.
WriteoutthecomputationsequenceofthefunctionalprogramforcomputingF
（2）.Constructaderivation（refutation）forthesamecomputationforthelogicprogram.
（a）函数程序计算序列:
F
（2）=>
（if2=0then1else2*F（2-1）fi）
=>
（iffalsethen1else2*F
（1）fi）（2=0,false）,（2-1,1）
2*F
（1）（iffalsethen1else2*F
（1）fi,2*F
（1））
2*（if1=0then1else1*F（1-1）fi）
2*（iffalsethen1else1*F（0）fi）（1=0,false）,（1-1,0）
2*（1*F（0））（iffalsethen1else1*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）
这里要注意，最后会出现不为空的情况（即不是Refutation），有一种理解是具有默认的式子：
true:
-.另一种是需要加式子m:
-
（c）逻辑程序的derivation:
GPθ
F（2,x）F（x1,n1）ß
F（x1-1,m1）,n1=x1*m1{x1/2,n1/x}
=>
F（1,m1）,x=2*m1F（x2,n2）ß
F（x2-1,m2）,n2=x2*m2{x2/1,n2/m1}
F（0,m2）,m1=1*m2,x=2*m1F（0,1）ß
{m2/1}
m1=1*m2,x=2*m1
m1=2,x=4
再根据true:
-和替换（m1/2,x/4），可以归到□。
6.GiveanexampleofafunctionalprogramforwhichthesemanticfunctionalΦistheidentityfunction.Explainwhy?
假设在UsualInterpretationI=（Nat,I0）下，定义函数程序为:
F（x）<
=F（x）
则指称语义函数Φ:
[Natωà
Natω]à
[Natωà
Natω],定义为
Φ（F）=[λF.[λx.F（x）]]
下面证明Φ是恒等函数，即对于任意的f,都有Φ（f）=f.
在InterpretationI下，对于任意的f∈[Natωà
Natω],和任意的n∈Natω,都有
Φ（f）（n）=I（[λF.[λx.F（x）]]）（γ[F/f][x/n]）,即
Φ（f）（n）=ω,n=ω;
=f（n）n≠ω;
所以对于任意的n∈Natω,如果n=ω,则Φ（f）（n）＝ω＝f（n）,如果n≠ω,也同样有Φ（f）（n）＝f（n）,所以Φ（f）=f,即Φ是恒等函数
#7.Givetheformaldefinitionofprogrampartialcorrectnessintermsofformulawlp（α,p）,whereαisapathinthegivenprogram.
这题首先必须要加入这个：
Partialcorrectness就是指对于输入q，ifM（S）isdefinedandI（p）（M（S）（σ））=truethenI（wlp（α,p））（r）=true
然后下面的内容是wlp和vc的定义，不是该题的重点，是否写上看情况吧。
令B是谓词逻辑的basis,p,q是WFFB的两个公式，S∈
是一个flowchart程序,a=（l0,l1,…lk）是程序S中的一条路径，
（i）根据k的取值递归地定义wlp（a,p）如下:
如果k=0,则定义wlp（a,p）=p;
当k>
0时，设β=（l1,l2,…lk）,r=wlp（β,p）,根据l0处的语句类型，分成两种情况来定义wlp（a,p）.
如果是平行的赋值语句，设形式如下所示:
l0:
（x1,x2,…xn）:
=（t1,t2,…tn）;
gotol1;
则定义wlp（a,p）=
;
如果是条件转移语句，设形式如下所示:
l0:
ifethengotolelsegotol’fi;
则定义wlp（a,q）如下:
e
r如果l1=l且l1≠l’
e
r如果l1≠l且l1=l’
（ii）定义partialcorrectness的验证条件vc（p,a,q）为p
wlp（a,q）.
令B为谓词逻辑的basis,p,q为WFFB的两个公式，S∈
是一个flowchart程序，对于任意的InterpretationI,程序S在InterpretationI中，对于p和q是partialcorrect的，当且仅当如果对于S中的任意一条路径a,都有验证条件vc（p,a,q）在I中为valid。
#8.ShowthatthefollowingisacorrectinferenceruleinHoarelogicusingconstructionsequencein“InductiveDefinitionofSets”.WhatareBandKinthiscontext?
Andwhatistheinductivelydefinedsetinthecontext?
forallp,q,r∈WFFB,e∈QFFB,andS∈L2B.
设WFFB为well-formedformula的集合
B={{
}x:
=t{p}|p∈WFFB,x∈V,t∈TB}
K={（（pà
r,{r∧e}S{r},（r∧
e）à
q）,{p}whileedoSod{q}）|
p,q,r∈WFFB,e∈QFFB,S∈
}
推导出来的集合是Hoarecalculus里面logicallyvalid的公式集的一个子集。
推导过程：
P->
r
{r^e}S1{r}
r^
e->
q
{r}whileedoS1od{r^
e}
{p}whilerdoS1od{q}
程序设计理论试题2000.1.22（即老师的样题）
1.
试指出链S在Natw->
Natw上的最小上界。
有些人说论域就是CPO。
对于该题，由于<
=为平坦半序，所以每条链都有lub，最小元是w。
所以可以构成CPO。
S的最小上界为：
#2.利用归一算法。
首先找到D1={f（a）,x}，取θ1={x/f（a）}，得Sθ1={p（f（a）,g（f（a））,p（f（a）,y））
然后找到D2={g（f（a））,y},取θ2={y/g（f（a））}，得Sθ1θ2={p（f（a）,g（f（a）））
即S可以归一。
且θ=（x/f（a）,y/（g（f（a）））
在某份答案中说这是不能归一，这显然是错误的。
这里的答案是正确的。
在老师讲义上说不能归一，课堂上他明确表示第二条式x是a的时候才是不能归一。
现在是可以归一的。
3.二进制数句法：
对于二进制数集合B，有
a.0和1属于B
b.如果a属于B并且a不等于0，则a0，a1属于B。
很多份答案（可能包括老师答案）都没有表示a不等于0，个人感觉是错误的，因为如01，001，这类数不是二进制数。
这些要排除。
对于B，我们给定一个解释I，其中+，*，为自然数中的加法和乘法：
a.φ（0）=0nat,φ（0）=1nat
b.如果a属于B并且a不等于0，则φ（a0）=φ（a）*2nat,φ（a1）=φ（a）*2+1。
c.φ（*）（a,b）=a*b,φ（+）（a,b）=a+b
指称函数：
[λxn…x1x0.xn*2^n+xn-1*2^（n-1）+…+x1*2+x0]
某些答案只写了一个递归的“指称函数”，感觉不对。
#4.S的语义范函为：
ФI（S）：
D*D*，具体为：
ФI（S）=I（[F.[x.ifx=0then1elsex*F（x-1）fi]]）（）对任意的赋值I
ФI（S）（f）（n）=I（ifx=0then1elsex*F（x-1）fi）（[F/f][x/n]）
程序的Meaningfunction
对任意的赋值I,MI（S）=ФI（S）=I（[F.[x.ifx=0then1elsex*F（x-1）fi]]）（）={ФIi（S）（）|iNat}
其中
MI（S）（n）=（{ФIi（S）（）|iNat}）（n）=
5．设B为谓词逻辑的基，I为基的一个解释，为相应的状态集，S为L1B或L2B的程序，MI（S）为程序的语义函数，谓词：
Bool和：
Bool分别为前置条件和后置条件。
则：
1）程序S和谓词的最弱前置条件是指：
谓词：
Bool，满足（）=true当且仅当MI（S）（）有定义且（MI（S）（））=true。
2）程序S和谓词的最强后置条件是指：
Bool，满足（）=true当且仅当存在一个状态’使得（’））=true且MI（S）（’）=。
#6.对于基B（F,P）,解释I为通常的解释。
则Φ（0）（σ）=0,Φ
（1）（σ）=1,…,
+为Nat2->
Nat，且Φ（+）（a,b）（σ）=a+b,
*为Nat2->
Nat，且Φ（*）（a,b）（σ）=a*b，
<
=为Nat2->
Bool，且Φ（<
=）（a,b）（σ）=a<
=b
该公式的语义为Φ（Vx.（0<
=x））=trueiff所有的x属于Nat，Φ（<
=）（0,x）（σ）=true，即0小于等于x（不建议写成x大于等于0）。
7．（P（3,1））=（y:
=1;
ify=1thenx:
=1elsex:
=2fi）（3,1）
=（ify=1thenx:
=（iftruethenx:
=（x:
=1）（3,1）
=（1,1）
#8.对于格局（S1，σ），并对格局（S1，σ）转移到（S2，σ’）,有：
当S1为whileedoSod;
S’时，S’<
>
ε，有σ=σ’，且
S2为a.S;
S1当Φ（e）（σ）=true
b.S’当Φ（e）（σ）=false
当S1为WhileedoSod时，有σ=σ’，且
S2为a.S当Φ（e）（σ）=true
b.ε当Φ（e）（σ）=false
#9．当使用通常解释I时，有
F
（2）=if2=0then1else2*F（2-1）fi
=iffalsethen1else2*F
（1）fi
=2*（if1=0then1else1*F（1-1）fi）
=2*（iffalsethen1else1*（F（0）fi）
=2*1*（F（0））
=2*（if0=0then1else0*F（0-1）fi）
=2*1=2
F（-2）由于不可终止，所以F（-2）未定义
#10．Vc（q,（test,loop,upd,test）,q）
q->
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->
（x=a^（y1+1）^2<
=c^y3+y2+2=（y1+1+1）^2^y2+2=2*（y1+1）+1））
vc（…）=
（x=a^y1^2<
=x^y3=（y1+1）^2^y2=2*y1+1^y3<
=x1）->
（x=a^（y1+1）^2<
=x^y3+y2+2=（y1+1+1）^2^y2+2=2*（y1+1）+1）
（可看书本P135）
#11．p->
r^-e->
{r}whileedoS1od{r^-e}
{p}whileedoS1od{q}
（可看书P153）
程序设计理论期末练习题
1.可参考老师样题的第6题。
*2.这题很难写。
先给个思路：
第一要建立一个well-foundedset（自然数集），并且需要最小值为0。
然后证明对于x<
0，程序无定义。
最后证明对于x>
0，每次的计算都是递减。
然后下结论。
#3.参考书本P50。
#4.F（x）<
-ifx=0then1elsex*F（x）fi
M（S）（3）:
F（3）=…=6.可参考老师样题第9题。
*5.P是程序，G是目标。
当我们称是P∪G的AS，是指对G的变量的一个替换。
而CAS，是指一个AS，并且是对P的所有的变量的替换。
AS是程序的中间过程，而CAS是程序运行的结果。
6.对于（Eω，）而言，ω为最小元，（Eω，）上有两条链均有限（见图），故（Eω，）构成一个论域。
对（Dω→Eω，）而言，由定理，若（Eω，）构成一个论域，Dω是一个集合，则（Dω→Eω，）亦构成一个论域，其最小元：
Dω→Eω，（0）=，
（1）=，（）=。
7.有问题的题目。
不过估计是x*F（x），老师样题4。
#8．又是一个很长的证明过程。
给思路：
首先需要指出有3种关键路径，（begin,test）,（test,loop,upd,test）,（test,end），然后对每种路径都要证明该式成立。
最后即可得出结论。
#9.这里不写证明了。
可参考老师样题中的10。
#10．书本P152。
#11．有问题的题目。
把它改成Φ（[λF.F（3,x）]（*））（γ）,且γ（x）=4
定义[λF.F（3,x）]为一个（Nat2->
Nat）->
Nat的函数，并设为Gγ。
则Gγ（op）=Φ[F（3,x）]（γ[F/op]）=op（3,4）
则Φ（[λF.F（3,x）]（*））（γ）=3*4=12。
可看书P95。
程序设计理论期末考试（99）
这年考试题目侧重于概念，与之后几年的题目有很大的区别
*1.问得真直接。
不好做。
指称语义：
定义了基类，然后由基类影射到相应的函数，然后由函数来定义其语义。
操作语义：
定义了抽象机，然后及其相关操作。
由抽象机的运行和状态来反映其语义。
异：
指称语义表示的语言要比操作语义要多。
指称语义重点在指称上，即所对应的函数上。
而操作语义的重点在于抽象机的运行及其状态。
*2.使用CPO的目的是最终能够归到基类，并且能够归到F和V这两个最基本的类型。
最小元表示函数影射的开始，也就是寻找对应的语义中的最小语义单位。
Chain就是其影射过程，也即对应的语义解释过程。
*3.ImperativeLanguage:
即命令方式语言。
Algol-Like语言。
该类语言通过各种相对独立的语句，语句自身是不会直接或间接调用自己，可以通过独立地对每条语句的解释来进行语义分析。
DeclarativeLanguage即声明方式语言。
Lisp-Like语言。
该类语言使用声明性语句，语句自身会直接或者间接调用自己，通过对多个变量的映射关系，来最终确认其对应的语义。
*4．个人感觉是正确的。
因为如果程序的语义脱离了形式系统，那么程序的语义就不能解释或者不可理解了。
而程序的正确性也不可验证了。
5.参考老师样题。
6.参考老师样题。
7.参考课本P50。
数据不同，最后结果为（ε,（5,2,5,9））
*8.书本P25。
简单来说就是一个解释φ，φ（w）（σ）=true,则φ为W的Model。
9．Complete。
因为定义了一个∞，即每个chain都存在lub。
这里要提出一个，R+∪{∞}也是CPO。
有人提出链：
1.1，1.11，1.111…，没有Lub。
其实是有的，
10.M（S）=xmod2.
11．部分正确性是基于程序对输入有定义下的正确性，即程序对合法的输入是正确的。
而完全正确性是需要证明其程序对输入有定义的，即程序对于输入是正确的，并且可以终止的。
基于谓词的正确性是证明给定的谓词是正确的。
基于公式的正确性是证明公式的守恒。
12．PartialCorrect:
i:
说明程序是无论有没定义都部分正确。
Ii:
说明程序是处处都没有定义。
Terminate:
程序处处有定义。
13.程序输入是x=y，输出是x=y!
，所以最后的结果一定是让x为y！
，y在程序中可变（改变以后可以归回原来的值），但最后的结果必定要让x=
升级会员 