Giáo trình Công nghệ phần mềm - Phan Huy Khánh (Phần 1)

Qb, w, r (w ≤ r) ∧ ¬W(w) ∧ B(w) → F 
Âiãöu naìy chæïng minh : 
Qb, w, r ∧ (w ≤ r) ∧ ¬W(w) ∧ B(w) { hoaïnvë(b, w) ; b := b+1 ; w := w+1 } Qb, w, r
(iii) Træåìng håüp R(w) 
Ta coï : 
Qb, w, r −1 { r := r −1 } Qb, w, r
Màût khaïc theo bäø âãö : 
Pb, w, r −1 ~ Pb, w, r ∧ ((r ≤ N) → R(r)) 
Aïp duûng tiãn âãö âënh nghéa båíi pheïp hoaïn vë cho Qb, w, r −1 : 
G { hoaïnvë(r, w) } Qb, w, r −1
våïi : 
G = E1 ∧ (1 ≤ b ≤ w) ∧ (w−1 ≤ r−1 ≤ N) ∧ Pb, w, r ∧ ((r ≤ N) → R(w)) 
 ∧ (1 ≤ r ≤ N) ∧ (1 ≤ w ≤ N) 
Thæûc tãú ta coï : 
Pb, w, r ∧ (b ≤ w) ∧ (w ≤ r) ∧ (1≤w≤ N) ∧ (1≤ r ≤N) 
{ hoaïnvë(r, w) } Pb, w, r ∧ (b ≤ w) ∧ (w ≤ r) 
Ta coï : 
G ~ E1 ∧ (1 ≤ b ≤ w) ∧ (w ≤ r ≤ N) ∧ R(w) ∧ Pb, w, r
Vaí laûi : 
E1 ∧ ¬W(w) ∧ ¬B(w) ∧ (1≤ w ≤ N) → R(w) 
Error! Reference source not found. 79 
Nhæ váûy : 
Qb, w, r ∧ (w ≤ r) ∧¬W(w) ∧ ¬B(w) → G 
Âiãöu naìy chæïng minh : 
Qb, w, r ∧ (w ≤ r) ∧ ¬W(w) ∧ ¬B(w) { hoaïnvë(r, w) ; r := r −1 } Qb, w, r
Tæì 3 kãút quaí trãn ta suy ra : 
Qb, w, r ∧ (w ≤ r) { A2 } Qb, w, r
(β) Chæïng minh tênh âuïng âàõn cuía chæång trçnh (I) 
Ta âaî coï : 
Qb, w, r { A2 } Qb, w, r ∧ (w > r) 
(i) Âiãöu kiãûn sau 
Ta coï : 
Qb, w, r ∧ (w > r) → (1 ≤ b ≤ w) ∧ (w=r+1) ∧ (r ≤ N) ∧ Pb, w, r
vaì : 
Pb, w, r∧ (w=r+1) → (1 ≤ α < b → B(α)) ∧ (b ≤ α < r → W(α)) ∧ (r < α ≤ Ν → R(α)) 
Nhæ váûy : 
Qb, w, r ∧ (w > r) → S1
trong âoï : 
Qb, w, r { A1 } S1
(ii) Khåíi gaïn 
Ta coï : 
E1 ∧ (0 ≤ n ≤ N) ∧ (n < α ≤ N → R(α)) { w := 1; b := 1; r := n } Qb, w, r
vaí laûi : 
(n=N) → (0 ≤ n ≤ N) ∧ (n < α ≤ N → R(α)), 
do âoï : 
E1 ∧ (n=N) { chæång trçnh (I) } S1
Nhæ váûy ta âaî chæïng minh xong tênh âuïng âàõn tæìng pháön. 
c) Chæïng minh dæìng 
Chæång trçnh (I) chè coï mäüt voìng làûp A1 vaì thán cuía voìng làûp laì A2. 
Giaí sæí : WQbwr ∧ (w ≤ r) = X1 vaì haìm m : X1 → N sao cho m(x) = r − w. 
TS. PHAN HUY KHAÏNH biãn soaûn 79 
80 Cäng nghãû Pháön mãöm 
Chuï yï : Viãûc chæïng minh dæìng laì chè ra ràòng kêch thæåïc cuía vuìng chæa xæí lyï r − 
w giaím dáön mäùi láön thæûc hiãûn A2. 
Âãø chæïng minh viãûc dæìng cuía A1, chè cáön chè ra ràòng : 
Qb, w, r ∧ (w ≤ r) ∧ (r −w = m0) { A2 } (w > r) ∨ (r −w < m0) ∀ m0 ∈ N 
Chuï yï ràòng : 
(r −w = m0) { w:= w+1 } (r −w = m0−1) træåìng håüp cuía W(w) vaì B(w) 
vaì (r −w = m0) { r := r −1 } (r −w = m0−1) træåìng håüp cuía R(w) 
Ta chæïng minh âæåüc ràòng : 
Qb, w, r ∧ (w ≤ r) ∧ (r −w = m0) { A2 } (r −w = m0−1) ∀ m0 ∈ N 
Tæì âoï chæång trçnh (I) dæìng. 
d) Chæïng minh chæång trçnh (I) thoaí maîn âiãöu kiãûn cuía baìi toaïn 
Báy giåì chè coìn phaíi chæïng minh ràòng âiãöu kiãûn “mäùi vë tæì B, W vaì R chè âæåüc 
xeït tênh nhiãöu nháút mäüt láön cho mäùi viãn bi” chæa xuáút hiãûn trong S1 cuîng thoaí 
maîn. 
Tháût váûy, åí trãn, ta âaî suy ra âæåüc ràòng A2 âæåüc thæûc hiãûn âuïng N láön (giaï trë 
cuía r −w giaím 1 mäùi láön, giaím tæì N−1 âãún 0). Màût khaïc, viãûc thæûc hiãûn A2 xeït tênh 
(nhiãöu nháút mäüt láön) caïc vë tæì liãn quan âãún chè mäüt viãn bi. Trong quaï trçnh sàõp 
xãúp, maìu cuía N viãn bi laì hoaìn toaìn xaïc âënh vaì vç coï N láön thæûc hiãûn, mäùi thæûc 
hiãûn cuía A2 chè liãn quan âãún 1 viãn bi phán biãût. 
III.3. In ra mäüt danh saïch theo thæï tæû ngæåüc 
Giaí sæí ta coï mäüt danh saïch tuyãún tênh gäöm caïc pháön tæí coï cáúu truïc vaì mäüt con 
troí chè âãún pháön tæí âáöu tiãn cuía danh saïch nhæ sau : 
const n = ... { âäü daìi låïn nháút cuía danh saïch } 
type KiãøuPháönTæí = ... { kiãøu cuía caïc pháön tæí trong danh saïch } 
KiãøuConTroí = 0..n; { kiãøu cuía con troí, 0 laì giaï trë nil } 
PháönTæí = record 
NäüiDung: KiãøuPháönTæí; 
TiãúpTheo: KiãøuConTroí; {troí âãún pháön tæí tiãúp theo } 
end; 
Danhsaïch = array[1..n] of PháönTæí; 
var Ds : Danhsaïch; { danh saïch caïc pháön tæí } 
Pâáöu : KiãøuConTroí; { con troí chè âãún pháön tæí âáöu tiãn cuía danh 
saïch } 
Error! Reference source not found. 81 
Giaí thiãút ràòng danh saïch chæïa êt nháút mäüt pháön tæí (âáöu danh saïch PÂáöu ≠ 
nil). Baìi toaïn âàût ra laì in näüi dung danh saïch theo thæï tæû ngæåüc laûi. Vê duû, nãúu ta 
coï : 
Pâáöu 
x1 • x2 • x3 • x4 nil 
thç chæång trçnh seî in ra nhæ sau : x4, x3, x2, x1. 
Ta seî âæa ra ba låìi giaíi TILDA1, TILDA2 vaì TILDA3 cho danh saïch coï âäü daìi n 
pháön tæí. Âäúi våïi mäùi låìi giaíi, ta seî phán têch thåìi gian vaì bäü nhåï cáön thiãút âãø thæûc 
hiãûn chæång trçnh. 
Caí ba låìi giaíi âãöu sæí duûng voìng làûp våïi báút biãún coï daûng sau : 
∧ 
 (caïc træåìng näüi dung caïc baín ghi αk+1, ..., αn âæåüc in theo chiãöu ngæåüc laûi) 
Pâáöu 
α1 α2 α3 αk αk+1 αn 
. . . . . . 
Mäùi bæåïc cuía voìng làûp laì tçm pháön tæí αk vaì viãút näüi dung (αk). Ba chæång trçnh 
phán biãût nhau cå baín åí caïch tiãúp cáûn âãún αk. 
III.3.1.TILDA1 
Ta sæí duûng mäüt danh saïch con troí, âáöu tiãn danh saïch åí traûng thaïi räùng, sau âoï 
hoaût âäüng våïi hai thao taïc nhæ sau : 
put(expr) âàût vaìo âènh danh saïch giaï trë cuía biãøu thæïc expr. 
get(x) nãúu danh saïch khaïc räùng, láúy giaï trë åí âènh danh saïch âãø gaïn cho 
biãún x, nãúu khäng, thao taïc khäng xaïc âënh. 
Chæång trçnh TILDA1 gäöm hai voìng làûp : 
(a) Voìng làûp thæï nháút : 
∧ (Danhsaïch = α1α2 ... αk − 1αk)
Pâáöu x
α1 α2 αk αk+1 αn
. . . . . . 
(b) Voìng làûp thæï hai : 
TS. PHAN HUY KHAÏNH biãn soaûn 81 
82 Cäng nghãû Pháön mãöm 
∧ 
 (Danhsaïch = α1α2 ... αk) 
(caïc træåìng näüi dung caïc 
baín ghi αk+1, ..., αn âaî 
âæåüc in theo chiãöu ngæåüc 
laûi) 
Pâáöu 
α1 α2 αk αk+1 αn
. . . . . . 
Mäùi bæåïc cuía voìng làûp laì tçm pháön tæí αk vaì viãút näüi dung (αk). Ba chæång trçnh 
phán biãût nhau cå baín åí caïch tiãúp cáûn âãún αk. 
IV. Caïc tiãn âãö vaì quy tàõc suy diãùn 
Muûc naìy seî nghiãn cæïu caïc váún âãö sau : 
• − Khaïi niãûm vãö âiãöu kiãûn træåïc yãúu nháút vaì âiãöu kiãûn sau maûnh nháút cuía 
mäüt daîy lãûnh. 
• − Caïc kiãøu tiãn âãö gaïn khaïc nhau. 
• − Caïc tiãn âãö vaì quy tàõc suy diãùn cho mäüt säú cáúu truïc ngän ngæî láûp trçnh 
(khäúi, thuí tuûc). 
• − Phán têch chæång trçnh. 
IV.1. Âiãöu kiãûn træåïc yãúu nháút vaì âiãöu kiãûn sau maûnh nháút cuía mäüt 
daîy lãûnh 
Trong muûc træåïc, ta âaî kyï hiãûu : 
− WE táûp håüp caïc giaï trë caïc biãún cuía mäüt chæång trçnh thoaí maîn âiãöu kiãûn 
E, 
− fP laì haìm tênh âæåüc båíi daîy caïc lãûnh P cuía mäüt chæång trçnh. 
Nãúu fP âæåüc âënh nghéa cho moüi giaï trë cuía WE , P khäng quáøn vaì khäng thæûc 
hiãûn caïc pheïp tênh vä âënh (vê duû chia cho 0) nãúu âiãöu kiãûn træåïc E thoaí maîn. Tênh 
cháút naìy âæåüc kyï hiãûu laì termEP. 
Báy giåì ta xeït phaït biãøu E {P} S. Ta coï caïc tênh cháút sau âáy : 
(i) E {P} S laì true nãúu vaì chè nãúu fP (WE) ⊆ WS
(ii) Nãúu termEP thç : 
E {P} S laì true nãúu vaì chè nãúu WE ⊆ fP−1 (WS) 
Vê duûû 15 : 
(1) Cho phaït biãøu (q > 0) { q := q+1 } (q > 0), trong âoï q laì biãún duy nháút cuía 
chæång trçnh. Ta coï : 
WE = WS =N+ , fq := q+1(N+) = N+ −{1} ⊆ N+ , 
Error! Reference source not found. 83 
vaì N+ ⊆ f−1q: := q+1(N+) = N 
(2) Cho phaït biãøu (q ≥ 0) ∧ (y ≥ 0) { q := q div y } (q ≥ 0) ∧ (y ≥ 0), trong âoï q vaì 
y laì caïc biãún duy nháút cuía chæång trçnh. Ta coï : 
WE = WS =N × N , fq := q div y (N × N) = N × N+ ⊂ WS , 
nhæng f−1q: := q div y (N × N) = N × N+ ⊇⁄ WE
Trong træåìng håüp WE = fP−1 (WS), E laì âiãöu kiãûn træåïc yãúu nháút (la plus faible 
preïcondition) phaíi âæåüc thoaí maîn træåïc khi thæûc hiãûn P âãø cho S âæåüc thoaí maîn 
sau âoï. 
Thæûc tãú, nãúu E’ {P} S vaì termE ’P thç WE ’ ⊆ fP−1 (WS) = WE vaì nhæ váûy E’ → E. 
Màût khaïc, nãúu fP(WE) = WS , S laì âiãöu kiãûn sau maûnh nháút (la plus forte 
postcondition) phaíi âæåüc thoaí maîn sau khi thæûc hiãûn P nãúu E laì âuïng træåïc. 
Thæûc tãú, nãúu E {P} S’ thç fP(WE) = WS ⊆ WS ’ , nhæ váûy S → S’. 
Ta kyï hiãûu hai haìm fppre vaì fppost nhæ sau : 
− våïi mäüt daîy lãûnh vaì våïi mäüt âiãöu kiãûn sau, fppre traí vãö âiãöu kiãûn træåïc yãúu 
nháút tæång æïng 
− våïi mäüt âiãöu kiãûn træåïc vaì mäüt daîy lãûnh, fppost traí vãö âiãöu kiãûn sau sau maûnh 
nháút tæång æïng. 
Chuï yï ràòng caïc haìm fppre(P, S) vaì fppost(E, P) âæåüc âënh nghéa gáön nhæ tæång 
âæång. 
Báy giåì ta seî trçnh baìy caïc tênh cháút cuía caïc haìm fppre vaì fppost. 
IV.1.1. Haìm fppre 
Våïi moüi âiãöu kiãûn S vaì daîy lãûnh P, pfpost(pfpre(P, S), P) → S 
Chæïng minh : 
Âàût E ~ pfpre(P, S). 
Ta coï WE = fP−1 (WS), tæì âoï suy ra fP(WE) = fP(fP−1 (WS)) ⊆ WS
Hay coï thãø noïi E ~ pfpre(P, S), tæì âoï suy ra pfpost(E, P) → S âpcm
IV.1.2. Haìm fppost 
Våïi moüi âiãöu kiãûn E vaì daîy lãûnh P, E → pfpre(P, pfpost(E, P)). 
Chæïng minh : 
Âàût S ~ pfpost(E, P). 
Ta coï WS = fP(WE), tæì âoï suy ra fP−1 (WS)= fP−1 (fP(WE)) ⊇ WE
TS. PHAN HUY KHAÏNH biãn soaûn 83 
84 Cäng nghãû Pháön mãöm 
Hay coï thãø noïi S ~ pfpost(E, P), tæì âoï suy ra E → pfpre(P, S) âpcm
Baìi táûp : 
1. Cho âiãöu kiãûn E vaì mäüt daîy lãûnh P, nhæîng âiãöu kiãûn naìo laìm thoaí maîn fP sao cho : 
E ~ pfpre(P, pfpost(E, P)) ? 
IV.1.3. Sæí duûng âiãöu kiãûn træåïc yãúu nháút vaì âiãöu kiãûn sau maûnh nháút âãø 
chæïng minh tênh âuïng âàõn cuía chæång trçnh 
a) Træåìng håüp âiãöu kiãûn træåïc yãúu nháút 
Sau khi âënh nghéa haìm pfpre, våïi moüi âiãöu kiãûn E vaì S, vaì moüi daîy lãûnh P, ta 
coï : 
( E {P} S ∧ termEP ) ~ ( E → pfpre(P, S) ) 
âàûc biãût : 
termEP ~ ( E → pfpre(P, true) ) 
Âiãöu naìy coï nghéa ràòng táûp håüp caïc giaï trë cuía pfpre(P, true) laì miãön xaïc âënh 
cuía haìm fP (nghéa laì táûp håüp caïc giaï trë sao cho chæång trçnh P âæa ra mäüt kãút 
quaí). 
Khaí nàng biãøu diãùn pfpre(P, S), ∀ P vaì ∀ S, cho pheïp chæïng minh tênh âuïng 
âàõn (CMTÂÂ) toaìn cuûc cuía chæång trçnh. 
Mäüt hãû thäúng CMTÂÂ toaìn cuûc sæí duûng âiãöu kiãûn træåïc yãúu nháút bao gäöm : 
(a) Våïi mäùi lãûnh så cáúp, caïc tiãn âãö cho âiãöu kiãûn træåïc yãúu nháút æïng våïi mäüt 
âiãöu kiãûn sau âaî cho. Âäúi våïi pheïp gaïn, caïc tiãn âãö âaî cho åí muûc I noïi chung 
seî thay thãú vai troì naìy. 
(b) Caïc quy tàõc suy diãùn cho pheïp xáy dæûng âiãöu kiãûn træåïc yãúu nháút cuía mäüt 
lãûnh khäng så cáúp P, xuáút phaït tæì caïc âiãöu kiãûn træåïc yãúu nháút cuía caïc lãûnh 
trong P. 
Vê duûû 16 : 
Giaí sæí cáön xaïc âënh : pfpre(if B then P else Q, S) 
Nãúu B cho mäüt kãút quaí, ta coï : 
pfpre(if B then P else Q, S) 
~ (B ∧ pfpre(P, S) ∨ (¬B ∧ pfpre(Q, S)) 
Nhæng viãûc tênh B âãø cho mäüt kãút quaí nãúu vaì chè nãúu pfpre(if B then , 
true) laì âuïng. 
Nhæ váûy trong træåìng håüp täøng quaït : 
Error! Reference source not found. 85 
pfpre(if B then P else Q, S) 
~if pfpre(if B then , true) 
then (B ∧ pfpre(P, S) ∨ (¬B ∧ pfpre(Q, S)) else false 
Khäng coï quy tàõc âån giaín cho voìng làûp while. 
Âäü phæïc taûp cuía caïc quy tàõc âæa ra âãø xaïc âënh dkt cuía mäüt voìng làûp while coï 
thãø âæåüc minh hoaû nhæ sau : 
− Váún âãö dæìng cuía voìng làûp while træìu tæåüng khäng laì quyãút âënh âæåüc. 
Vç váûy, âiãöu kiãûn 
 pfpre(while B do P, true) 
khäng tênh âæåüc cho moüi B, moüi P. 
− Viãûc giaíi quyãút mäüt säú baìi toaïn näøi tiãúng âæa vãö viãûc chæïng minh mäüt chæång trçnh 
laì dæìng. Vê duû, ngæåìi ta khäng biãút nãúu : 
pfpre(while n1 do 
n:=if not odd(n) then n div 2 else 3*n+1, true)~(n >= 1) 
Âáy laì sæû giaí âënh (conjecture) cuía Collatz. 
Chuï yï : Caïc tiãn âãö vaì caïc quy tàõc suy diãùn xeït åí muûc I cho pheïp chæïng minh tênh 
âuïng âàõn cuía caïc phaït biãøu E {P} S, trong âoï E ≠ pfpre(P, S). Vê duû, ta âaî 
chæïng minh tênh âuïng âàõn tæìng pháön ràòng : 
(a ≥ 0) {Div} (a = bq + r) ∧ (q ≥ 0) ∧ (0 ≤ r < b) 
b) Træåìng håüp âiãöu kiãûn sau maûnh nháút 
Theo âënh nghéa cuía pfpost, ta coï : E {P} S ~ (pfpost(E, P) → S) 
Nhæ váûy, mäüt hãû thäúng chæïng minh tênh âuïng âàõn dæûa trãn viãûc tênh toaïn caïc 
âiãöu kiãûn sau maûnh nháút cho pheïp chæïng minh tênh âuïng âàõn tæìng pháön. 
Âäúi våïi lãûnh âiãöu kiãûn, quy tàõc suy diãùn âæåüc cho båíi tênh cháút : 
pfpost(E, if B then P else Q) 
~ pfpost(E ∧ B, P) ∧ pfpost(E ∧ ¬B,Q) 
våïi giaï trë ràòng B luän luän cho mäüt kãút quaí. 
Trong træåìng håüp täøng quaït : 
pfpost(E, if B then P else Q) 
~ pfpost(E ∧ (if pfpre(if B then, true) then B else false), P) 
 ∨ pfpost(E ∧ (if pfpre(if B then, true) then ¬B else 
false), Q) 
TS. PHAN HUY KHAÏNH biãn soaûn 85 
86 Cäng nghãû Pháön mãöm 
IV.2. Caïc tiãn âãö gaïn 
IV.2.1. Âiãöu kiãûn træåïc yãúu nháút vaì âiãöu kiãûn sau maûnh nháút cuía lãûnh gaïn 
Âiãöu kiãûn træåïc E âæåüc tênh toaïn theo quy tàõc âaî trçnh baìy åí muûc I âãø taûo ra 
caïc tiãn âãö gaïn laì âiãöu kiãûn træåïc yãúu nháút cuía mäüt lãûnh gaïn x := vaì cuía mäüt 
âiãöu kiãûn sau S, khi âaûi læåüng termE(x := ) coï giaï trë true. Trong træåìng håüp 
naìy, tiãn âãö âæåüc kyï hiãûu båíi : 
pfpre(x := , S) { x := } S 
Trong træåìng håüp täøng quaït, ta coï : 
pfpre(x := , S) ~ if pfpre(x := , true) then S(x ⁄ ) else false. 
Âiãöu kiãûn pfpre(x := , true) thãø hiãûn : 
− x vaì caïc toaïn haûng cuía âæåüc âënh nghéa : 
chè säú cuía maíng nàòm giæîa cáûn dæåïi vaì cáûn trãn, caïc con troí chè âãún caïc biãún 
khaïc nil, v.v..., 
− moüi pheïp toaïn thæûc thi âãöu cho kãút quaí : 
coï sæû tæång thêch vãö kiãøu cuía caïc toaïn haûng, khäng coï pheïp chia cho 0, v.v... 
ÅÍ âáy ta khäng tháúy sæû vi phaûm vãö tênh håüp thæïc cuía caïc tiãn âãö âaî nãu trong 
muûc I vãö tênh âuïng âàõn tæìng pháön : nãúu termE(x := ) coï giaï trë false, phaït biãøu 
E { x := } S laì true. Ngæåìi ta coï thãø cuíng cäú âiãöu kiãûn træåïc cuía caïc tiãn âãö naìy 
båíi caïc âiãöu kiãûn do pfpre(x := , true) âæa âãún. 
Vê duû, nãúu m vaì n láön læåüt laì cáûn dæåïi vaì cáûn trãn cuía maíng a, thay vç : 
(y > 0) { x := a[j] } (y > 0) vaì 
(a[j] = y) { x := a[j] } (x = y) 
Ta coï thãø viãút : (m ≤ j ≤ n) ∧ (y > 0) { x := a[j] } (y > 0) 
if (m ≤ j ≤ n) then (a[j] = y) else false { x := a[j] } (x = y) 
Theo mãûnh âãö III.1.1, nãúu E (x := ) S laì mäüt tiãn âãö, S khäng nháút thiãút laì 
âiãöu kiãûn sau maûnh nháút æïng våïi E. Nhæ váûy caïc tiãn âãö gaïn noïi chung khäng thãø 
kyï hiãûu : 
E (x := ) pfpost(E, x := ) 
Chàóng haûn ta coï tiãn âãö : (1−x ≥ 0) { x := 1 ⁄ x } (x ≥ 0) 
Ta coï : (1−x ≥ 0) ~ (x > 0), nhæng pfpost(x > 0, x := 1 ⁄ x) ~ (x > 0) 
Báy giåì ta seî xeït caïc quy tàõc xáy dæûng caïc tiãn âãö tæì âiãöu kiãûn træåïc vãö âiãöu 
kiãûn sau. Caïc tiãn âãö naìy seî luän luän âæåüc kyï hiãûu båíi : 
E (x := ) pfpost(E, x := ) 
nhæng khäng thãø kyï hiãûu båíi : pfpre(x := , S) { x := } S 
Error! Reference source not found. 87 
IV.2.2. Quy tàõc tênh toaïn âiãöu kiãûn sau maûnh nháút cuía mäüt pheïp gaïn 
Våïi lãûnh gaïn x := , chè coï biãún x bë thay âäøi. Nhæ váûy, fx := laì mäüt haìm tæì 
táûp håüp W caïc giaï trë cuía caïc biãún cuía chæång trçnh vaìo chênh noï, âàût âäöng nháút 
caïc thaình pháön, træì biãún x. 
Ta kyï hiãûu πx fx := laì pheïp chiãúu cuía fx := vaìo thaình pháön naìy. 
Vê duû, våïi lãûnh q := q+1 cuía chæång trçnh Div åí muûc I, ta coï : 
fq := q+1 (a, b, q, r) = (a, b, q+1, r) vaì πq fq := q+1 (a, b, q, r) = q+1 
Tæång tæû, quy tàõc âiãöu kiãûn træåïc vãö tiãn âãö gaïn âaî cho åí muûc I coï thãø viãút : 
E ~ S(x ⁄ πx fx := ) 
Báy giåì ta seî âënh nghéa hai quy tàõc tênh toaïn âiãöu kiãûn sau maûnh nháút cuía 
mäüt lãûnh gaïn. 
a) Træåìng håüp âàûc biãût 
Nãúu haìm thu heûp fx := vaìo WE laì toaìn cuûc vaì âån aïnh, seî täön taûi haìm ngæåüc 
f−1 x := 
Trong træåìng håüp naìy, coï thãø sæí duûng quy tàõc sau âáy âãø tênh pfpost : 
pfpost(E, x := ) ~ E(x ⁄ πxf−1 x := ) 
nghéa l1 ta nháûn âæåüc âiãöu kiãûn sau maûnh nháút cuía mäüt âiãöu kiãûn træåïc E vaì mäüt 
pheïp gaïn x := båíi viãûc thay thãú nhæîng nåi x xuáút hiãûn trong âiãöu kiãûn E båíi 
haìm ngæåüc cuía fx := . 
Tæì quy tàõc tênh pfpost, ta coï tiãn âãö gaïn tæì âiãöu kiãûn træåïc vaì âiãöu kiãûn sau 
nhæ sau : 
E { x := } E(x ⁄ πxf−1 x := ) 
Sæ täön taûi haìm ngæåüc cuía f−1 x := cho pheïp tçm âæåüc giaï trë cuía x træåïc khi 
thæûc hiãûn pheïp gaïn, tæì caïc giaï trë caïc biãún sau khi gaïn. 
Chuï yï : pfpost(q ≥ 0, q := q+1) ~ (q−1 ≥ 0) 
pfpost(q ≥ 0, q := q∗2) ~ ( q−2 ≥ 0) 
pfpost(q = 0, q := q+a) ~ (q−a = 0) 
Ta nháûn âæåüc caïc tiãn âãö sau âáy : 
(q ≥ 0) { q := q+1 } (q−1 ≥ 0) 
(q ≥ 0) { q := q∗2 } ( x−2 ≥ 0) 
(q = 0) { q := q+a } (q−a = 0) 
Quy tàõc trãn khäng duìng âæåüc cho caïc pheïp gaïn nhæ q := 0, hoàûc q := q div 2. 
TS. PHAN HUY KHAÏNH biãn soaûn 87 
88 Cäng nghãû Pháön mãöm 
Ta coï thãø duìng quy tàõc âãø chæïng minh chæång trçnh theo chiãöu bàõt âáöu − kãút 
thuïc. 
Vê duû, âãø chæïng minh (x > 0) { x := x∗2 } (x > 0) : 
• Xeït quy tàõc tæì âiãöu kiãûn sau vãö âiãöu kiãûn træåïc : 
(2x > 0) { x := x∗2 } (x > 0) 
Sæí duûng quy tàõc âiãöu kiãûn træåïc, ta nháûn âæåüc kãút quaí vç : 
(2x > 0) → (x > 0) 
• Xeït quy tàõc tæì âiãöu kiãûn træåïc vãö âiãöu kiãûn sau : 
(x > 0) { x := x∗2 } ( x−2 > 0) 
Sæí duûng quy tàõc âiãöu kiãûn sau, ta nháûn âæåüc kãút quaí vç : ( x−2 > 0) → (x > 0) 
Chuï yï : Caïc tiãn âãö gaïn âaî âæa ra trong caïc vê duû trãn coï thãø nháûn âæåüc tæì âiãöu 
kiãûn sau båíi tiãn âãö gaïn åí muûc I. Trong caïc vê duû naìy, haìm fx := : W → 
W laì âån aïnh. 
Vê duû sau âáy chè ra ràòng nãúu haìm fx := : W → W khäng laì âån aïnh, 
ngæåìi ta khäng coìn coï tênh cháút naìy. 
Vê duûû 17 : 
Haìm fx := x div 2 laì toaìn thãø, nhæng khäng âån aïnh. Thu heûp cuía noï vaìo Wx = 2y laì 
âån aïnh. 
Aïp duûng quy tàõc tênh pfpost, ta coï tiãn âãö : (x = 2y) { x := x div 2 } (2x = 2y) 
tæång âæång våïi : (x = 2y) { x := x div 2 } (x = y) 
Tuy nhiãn, xuáút phaït tæì âiãöu kiãûn sau (2x = 2y) vaì sæí duûng tiãn âãö gaïn åí muûc I, 
ta coï tiãn âãö : 
(2 ⎣x−2⎦ = 2y) { x := x div 2 } (2x = 2y) 
tæång âæång våïi : (2 ⎣x−2⎦ = 2y) { x := x div 2 } (x = y) 
b) Træåìng håüp täøng quaït 
Nãúu khäng täön taûi haìm ngæåüc cuía fx := , seî khäng thãø tçm âæåüc giaï trë ban 
âáöu cuía x, xuáút phaït tæì giaï trë caïc biãún sau khi thæûc hiãûn pheïp gaïn. 
Error! Reference source not found. 89 
V. Baìi táûp 
Baìi 1 : Sæí duûng caïc quy tàõc trãn âáy, chæïng minh caïc tênh cháút sau : 
1. Nãúu E {P} S vaì E’ {P} S’ laì caïc âënh lyï, thç E ∧ E’ {P} S ∧ S’ vaì E ∨ E’ {P} S ∨ S’ 
cuîng laì caïc âënh lyï. 
2. Nãúu E {P} F vaì G {Q} S laì caïc âënh lyï vaì nãúu F → G, thç E {P ; Q} S laì mäüt âënh 
lyï. 
3. Sæí duûng quy tàõc “;”, chæïng minh ràòng : (y = 2) { x := y+1 ; z :=x+y } (z = 5) 
4. Sæí duûng quy tàõc âiãöu kiãûn træåïc, chæïng minh ràòng : (q ≥ 0) { q := q + 1 } (q ≥ 0) 
5. Pheïp thãú sæí duûng trong quy tàõc trãn âáy coï thãø âæåüc viãút E = S (x ⁄ ). Trong 
âiãöu kiãûn âàûc biãût cuía mäüt biãøu thæïc âiãöu kiãûn træåïc, pheïp thãú naìy âæåüc âënh 
nghéa båíi : 
S (x ⁄ if a then e1 else e2) (a ∧ S (x ⁄ e=ân 1)) ∨ (¬a ∧ S (x ⁄ e2)) 
Sæí duûng quy tàõc trãn âáy âãø chæïng minh : 
(z ≥ 0) { z := if b > 0 then z + b else z − b } (z ≥ 0) 
Baìi 2 : Chæïng minh Div dæìng : 
Bàòng caïch sæí duûng haìm m’(w) = A
B
⎢
⎣⎢
⎥
⎦⎥
 − q, trong âoï A
B
⎢
⎣⎢
⎥
⎦⎥
 laì pháön nguyãn cuía pheïp 
chia A
B
. 
Chæïng minh sau khi ra khoíi voìng làûp, m’(w) = 0. 
Baìi 3 : Tæì chæång trçnh P trong muûc II.2.1, haîy : 
1. Chæïng minh hçnh thæïc chæång trçnh P. 
2. Cho biãút säú láön täúi âa thæûc hiãûn voìng làûp cuía P. 
3. Sæí duûng chæång trçnh Div cuía muûc træåïc âãø suy diãùn tæì P mäüt chæång trçnh 
tênh ÆSCLN cuía hai säú nguyãn dæång A vaì B båíi viãûc tênh säú dæ liãn tiãúp. 
Baìi 4 : Tæì chæång trçnh (Ibis) trong muûc II.2.2, haîy : 
1. Chæïng minh ràòng chæång trçnh (Ibis) thoaí maîn caïc raìng buäüc cuía baìi toaïn. 
2. Chæïng minh ràòng chæång trçnh (Ibis) khäng coìn thoaí maîn nãúu thay thãú voìng làûp 
trong cuìng båíi : 
while R(r) and (w<=r) do r:=r-1; 
if w<r then begin hoaïnvë(r, w); r:=r-1 end; 
Chæïng minh ràòng chæång trçnh naìy coï thãø dáùn âãún tênh R(0). 
TS. PHAN HUY KHAÏNH biãn soaûn 89