A Discipline of Programming 筆記,1-4章

04-03

看的中英對照譯本，編程的修鍊。@霧雨魔理沙推薦過的書。讀了10幾章了感覺確實不錯。

序

在任何情況下，作者都覺得應該把重複結構本身作為語言的一種構造

重複結構是需要變數賦值的最根本原因。

賦值語句的"動態"性質讓數學家找不到合適的理論，所以不喜歡它。

直到現在，理論計算科學家也認為遞歸比重複"更自然"

不要用尾遞歸去描述循環了，循環和變數才是更加自然和接近事實的概念。

while B do S

rather than

procedure whiledo(c,s);begin if c then begin s;whiledo(c,s);endend

第2章

condition and predicate

predicate "x=y" and "y=x" represent the same condition

a state for which a predicate is true

a state that satisfies a condition

Each predicate is assumed to be defined in each point of the state space under

consideration:in each point the value of a predicate is either "true" or

"false"

say predicate P and Q equal when they denote to the same condition

we reserve the name "T" and "F"

T is the predicate that is true in all points of the state space

F is the predicate that is false in all points of the state space

我的理解：predicate相當於term，condition相當於語義

true 和 false 是 value

第3章

確定性機器:將其激活後，機器發生的事情完全由他的初始狀態決定。如果在同一個初始狀態激活它兩次，發生的情況都一模一樣。

非確定性機器：在給定的初始狀態激活它，發生的事情是一類可能發生的事情之一，初始狀態只是確定了可能發生的事的集合。

We are primarily interested in sustems that,when started in an "initial

state",will end up in a "final state",which,as a rule,depends on the choice of

the initial state.

(desired) post condition + limits provided by a practical system

GCD(x,y)=GCD(X,Y) and 0<x<=500and 0<y<=500

最弱前條件

the condition that characterizes the set of ALL initial states such that

activation will certainly result in a PROPERLY TERMINATING happening leaving

the system in a final state satisfying a given post-condition is called the

weakest pre-condition corresponding to that post-condition.

If the system(machine,mechanism) is denoted by "S",and the desired

post-condition by "R",then weakest pre-condition is denoted by

wp(S,R)

則，如果初始狀態滿足wp(S,R)，則該系統就能保證設備S激活後，最終使條件R成立

如果初始狀態不滿足wp(S,R),則系統最終一定不能使條件R成立，或者停在不滿足R的狀態，或者不終止。

設備的語義：採用規則的形式，說明如何從給定的後條件推導出與之對應的最弱前條件wp(S,R)。

For a fixed machanism S such a rule,which is fed with the predicate R denoting

the post-condition delivers a predicate wp(S,R) denoting the corresponding

weakest precondition, is called a predicate transformer

//公理語義？

在很多情況下，我們感興趣的並不是一個設備的完全的語義，因為我們總是把S用於某種特殊的目的。

是希望某個非常特殊的後條件R成立，並為此設計了S。

即使對於這個特殊的後條件R，我們關心的也常常不是wp(S,R)的確切形式，而是關心某個更強一些的條件P，滿足

P => wp(S,R) is true for all states

predicate p => Q reads P implies Q is only false in those points in state

space where condition P holds,but Q does not.and is true anywhere else.

If for a given P,S and R, relation P => wp(S,R) holds,this can often be

proved without explicit formulation of wp(S,R).And this is a good thing.

Properties of predicate transformer

1, 對於任意設備S，wp(S,F) = F

Law of Excluded Miracle

反證法，假設成立，則存在某個狀態滿足wp(S,F),取該狀態為S的初始狀態，則最終系統能結束運行，且對於該終止狀態，predicate

F 為true。這與F的定義矛盾，在所有狀態下，F都應為false。所以原命題成立。

2,對任意設備S，任意後條件Q和R，如果

Q => R for all states

那麼

wp(S,Q) => wp(S,R) for all states

從任何滿足wp(S,Q)的初始狀態激活系統S,結束狀態滿足Q,則結束狀態也滿足R。即該初始狀態也滿足wp(S,R)

即wp(S,Q)為真時，wp(S,R)也為真

3，對於任意設備S，(wp(S,Q) and wp(S,R)) = wp(S,Q and R)

顯然，左推右成立

右推左：

(Q and R) => Q

wp(S,Q and R) => wp(S,Q)

wp(S,Q and R) => wp(S,R)

A=>B A=>C 可得A=>(B and C)

所以右推左成立

4,對於任意設備S，(wp(S,Q) or wp(S,R)) => wp(S,Q or R)

Q => Q or R

R => Q or R

所以 wp(S,Q) => wp(S,Q or R)

wp(R,Q) => wp(S,Q or R)

4『，對於任意確定性設備S，及任意後條件Q和R有

(wp(S,Q) or wp(S,R)) = wp(S,Q or R)

右推左：對於確定性設備，對於一個滿足wp(S,Q or

R)的初始狀態，該狀態存在唯一的一個最終狀態either 滿足Q or

滿足R。or同時滿足兩者。即初始狀態狀態滿足either滿足

wp(S,Q) 或 wp(S,R) 或者兩者都滿足。即初始狀態滿足wp(S,Q) or wp(S,R)

the design of a mechanism that is to have a purpose must be a goal-directed

http://activity.In our special case it means that we can expect our post-condition to

be the starting point of our design considerations.

寬鬆前條件

對於確定性設備S和某個後條件R，初始狀態將落到三個不相交的集合之一：

(a) S的激活達到滿足R的最終狀態

(b) S的激活達到不滿足R的最終狀態

第一個集合由 wp(S,R) 表示

第二個集合由 wp(S,non R) 表示

wp(S,R) or wp(S,non R) = wp(S, R or non R) = wp(S,T)

因此第三個集合由 non wp(S,T) 刻畫

寬鬆前條件：只保證系統不會產生錯誤的結果。不會到達一個不滿足R的最終狀態

最弱寬鬆前條件 wlp(S,R)

wlp(S,T) = T

理解：任何初始狀態都不會到達一個不滿足T的最終狀態。

wlp(S,F) and wp(S,T) = F

如果不是這樣：一個初始狀態就能既保證終止，又保證不終止

(a) wp(S,R) = wlp(S,R) and wp(S,T)

激活將保證後條件R成立

(b) wp(S,non R) = wlp(S,non R) and wp(S,T)

激活將保證後條件non R成立

激活將不能正常終止

(ab) wp(S,T) and non wlp(S,R) and non wlp(S,non R)

激活將導致終止，但該初始狀態不確定最終狀態是否滿足R

(ac) wlp(S,R) and non wp(S,T)

如果激活後能終止，則最終狀態滿足R，但不確定從該初始狀態出發能否一定終止。

(bc) wlp(S,non R) and non wp(S,T)

如果激活後能終止，則最終狀態滿足non R，但不確定從該初始狀態出發能否一定終止。

(abc) non (wlp(S,R) or wlp(S,non R) or wp(S,T))

這種初始狀態的行為不確定，激活後可能終止或不終止。若終止，終止後，可能滿足R或不滿足R

後四種情況只存在於非確定性機器中

第4章

predicate transformer

wp(skip,R) = R 對所有的後條件R

wp(abort,R) = F 對所有的後條件R

考慮取R=T,表示後條件沒有任何限制，只表示存在後條件。

而調用這個名為abort的設備，在這種情況下也找不到任何初始狀態使得運行後存在最終狀態。

所以調用這個設備，它不能達到任何最終狀態，即失敗。

<statement> ::= skip|abort

R E->x 表示把predicate R中的變數x都換成表達式E得到的結果

wp(x:=E,R) = R E->x

例如，wp(a:=7,a=7) = {7=7}

很像公理語義

並發賦值 concurrent assignment

x1,x2 := E1,E2

交換x,y的值

x,y := y,x

wp(S1;S2,R) = wp(S1,wp(S2,R))

如果只有

;，那麼一個語句被執行的唯一條件就是它的上一個語句能夠正常終止。位置了實現我們需要的靈活性，必須能讓一個語句的執行依賴於當前系統的狀態。引入guarded command

<guarded command> ::= <guarding head>{;<statement>}

{} reads followed by zero or more instances of the enclosed.

when we have enough sufficiently tolerant guards such that the truth of Q

implies the truth of at least one guard,we have for each initial state

satisfying Q a mechanism that will bring the system in a state satisfying

R,one of the guarded commands whose guard is initially true.

<guarded command set> ::= <guard command>{[] <guarded command>}

<statement> ::= if <guarded command set> fi

1,assumed all guards are defined;if not,if the evaluation of a guard lead to a

not properly terminating,then the whole construct is allowed to fail to

terminate properly.

2,In genneral,our construct will give rise to nondeterminacy.fot each initial

state when more than one guard is true.because it is left undefined which of

the corresponding statement lists will then be selected for activation.No

nondeterminacyis introduced if any of two guards exclude each other.

3,If the initial state is such that none of the guards is true,Activation in

such an initial state will lead to abortion.

if B1->SL1 [] ... [] Bn->SLn fi

wp(IF,R) = (E j:1<=j<=n:Bj) and (A j:1<=j<=n:Bj => wp(SLj,R))

wp(IF,R) is true for every point in state space where there exists at least

one j in range[1,n] such that Bj is true

and where for all j in range[1,n]such that Bj is true,wp(SLj,R) is true as

well.

我的理解：只要執行到這裡，Bj為真，wp(SLj,R)就一定為真。也就是可以執行SLj。但不一定執行。且SLj能終止。實現里是多個Bj為真時，任選一個執行。強行引入非確定性。。。如果改成Bj為真就執行SLj可能更好理解一點？

do B1->SL1 [] ... [] Bn->SLn od

當存在Bj為真時，就繼續執行該語句。直到所有Bj都為假。當存在多個為真的guard時，選擇一個相應的SL執行。