Giáo trình Công nghệ phần mềm (Phần 2)

65 trang ngocly 120

Download

Bạn đang xem 20 trang mẫu của tài liệu "Giáo trình Công nghệ phần mềm (Phần 2)", để tải tài liệu gốc về máy bạn click vào nút DOWNLOAD ở trên

Tài liệu đính kèm:

giao_trinh_cong_nghe_phan_mem_phan_2.pdf

Nội dung text: Giáo trình Công nghệ phần mềm (Phần 2)

CHÆÅNG 4 Thæí nghiãûm chæång trçnh Nhæ âaî trçnh baìy trong chæång træåïc, ngæåìi ta thæåìng sæí duûng caïc kyî thuáût ténh (static techniques) vaì kyî thuáût âäüng (dynamic techniques) trong quaï trçnh V&V âãø kiãøm tra tênh âuïng âàõn cuía mäüt saín pháøm pháön mãöm. Chæång naìy seî trçnh baìy mäüt phæång phaïp ténh laì khaío saït (inspection) chæång trçnh, våïi vai troì nhæ laì mäüt pheïp chæïng minh phi hçnh thæïc vaì, mäüt phæång phaïp âäüng laì thæí nghiãûm(testing) chæång trçnh. I. Khaío saït Khaío saït (hay thanh tra) laì nhuîng cuäüc hoüp nhàòm muûc âêch xaïc minh mäüt saín pháøm. Pháön låïn caïc phæång phaïp saín xuáút pháön mãöm âãöu áún âënh træåïc nhæîng cuäüc hoüp nhæ váûy. Tuìy theo baín cháút cuía saín pháøm cáön khaío saït, ngæåìi ta noïi vãö khaío saït thiãút kãú toaìn thãø (global design), khaío saït thiãút kãú chi tiãút (detailed design), vaì khaío saït maî nguäön. Mäüt këch baín máùu (typical scenario) cho mäüt khaío saït maî nguäön nhæ sau : 1. Cáön âãún 4 ngæåìi gäöm mäüt chuí tëch, mäüt ngæåìi láûp trçnh, mäüt ngæåìi thiãút kãú vaì mäüt khaío saït (âãöu laì nhuîng chuyãn gia vãö Tin hoüc, riãng khaío saït phaíi coï kiãnú thæïc chuyãn män vãö lénh væûc æïng duûng cuía saín pháøm). 2. Caïc thaình viãn nháûn chæång trçnh nguäön vaì caïc âàûc taí træåïc cuäüc hoüp êt ngaìy âãø âoüc vaì chuáøn bë. 3. Cuäüc hoüp keïo daìi khoaíng 1 giåì 30 âãún khoaíng 2 giåì. 4. Trong quaï trçnh hoüp khaío saït : − Ngæåìi láûp trçnh âoüc vaì giaíi thêch chæång trçnh cuía mçnh, coï thãø âoüc tæìng doìng lãûnh mäüt vaì traí låìi caïc cáu hoíi âæåüc âàût ra. − Chæång trçnh âæåüc phán têch càn cæï trãn mäüt danh saïch caïc läùi sai (errors) thäng duûng do khaío saït cung cáúp. 5. Cuäüc hoüp khäng sæía läùi tçm tháúy maì chè ghi nháûn qua biãn baín maì thäi. Chênh ngæåìi láûp trçnh seî tæû sæía läùi sau khi hoüp xong. 6. Nãúu khi khaío saït tçm tháúy trong chæång trçnh, nhiãöu khiãúm khuyãút (failures), hoàûc nhiãöu läùi tráöm troüng thç phaíi tiãúp tuûc khaío saït láön sau, sau khi sæía läùi. TS. PHAN HUY KHAÏNH biãn soaûn 90
Thæí nghiãûm chæång trçnh 91 Mäüt säú këch baín coi troüng viãûc tçm läùi sai vaì khuyãún khêch viãûc chaûy demo træûc tiãúp maî chæång trçnh (hand made) nguäön : khaío saït mang âãún cuäüc hoüp caïch tiãún haình vaì caïc dæî liãûu liãn quan âãø moüi ngæåìi tiãún haình thæí nghiãûm. Ngæåìi ta coìn goüi caïch thæí nghiãûm nhæ váûy laì walk throughs (chaûy suäút). Mäüt säú këch baín laûi coi troüng viãûc chæïng minh khäng hçnh thæïc : khaío saït âãö nghë xaïc minh caïc tênh cháút cho pheïp thæí nghiãûm tênh âuïng âàõn cuía saín pháøm. Ngæåìi ta noïi âáy laì viãûc khaío saït càn cæï trãn viãûc xaïc minh. Viãûc kiãøm laûi (review) khaïc våïi khaío saït vç ràòng viãûc kiãøm laûi khäng âoìi hoíi phaíi hoüp : Saní pháøm âæåüc giao cho nhæîng ngæåìi khäng tham gia vaìo viãûc láûp trçnh, hoü coï nhæîng khuynh hæåïng âaïnh giaï âäüc láûp. Coï thãø noïi phæång phaïp khaío saït coï hiãûu quaí âaïng kãø : nhæîng säú liãûu tçm tháúy trong caïc vàn baín ghi nháûn khoaíng 50% sai soït âæåüc phaït hiãûn khi khaío saït. Nhæîng con säú dæåïi âáy (láúy tæì taûp chê IEEE3 nàm 1992 cuía Dyer M. tæì baìi baïo “Verification Based Inspection") cho tháúy caïc sai säú tçm tháúy khi phaït triãøn dæû aïn 5 pháön mãöm cuía haîng IBM : Khaío saït Khaío saït Khaío saït maî Thæí nghiãûm Thæí nghiãûm Dæû aïn thiãút kãú toaìn bäü thiãút kãú chi tiãút âån vë hãû thäúng 1 50 25 25 2 4 13 49 17 17 3 20 27 10 20 23 4 20 26 22 18 36 5 10 18 24 24 24 Mäüt phæång phaïp khaïc, goüi laì phæång phaïp phoìng saûch (Clean-room Methodology), thay vç thæí nghiãûm (testing), khuyãún khêch viãûc khaío saït (inspection) bàòng caïch xaïc minh (verification) trong quaï trçnh saín xuáút pháön mãöm. Sæû phaït triãøn pháön laì liãn tiãúp laìm mën (raffinement) saín pháøm. Mäùi giai âoaûn, ngæåìi ta tiãún haình chæïng minh tênh âuïng âàõn (prouving) mäüt caïch chàût cheî, âäöng thåìi våïi caïc cuäüc khaío saït, sao cho saín pháøm pháön mãöm khäng chæïa sai soït. Viãûc thæí nghiãûm chè âæåüc tiãún haình khi xaïc minh háûu nghiãûm (a posteriori) nhåì caïc phæång phaïp thäúng kã, nhàòm âaût âæåüc muûc âêch âàût ra luïc âáöu. Phæång phaïp phoìng saûch do H.Mills xáy dæûng taûi IBM, âaî âæåüc aïp duûng âãø saín xuáút caïc pháön mãöm cåî låïn. 3 IEEE, âoüc laì eye-triple-ee, tãn viãút tàõt cuía Institute of Elechtrric and Engineers. TS. PHAN HUY KHAÏNH biãn soaûn 91
92 Cäng nghãû Pháön mãöm II. Caïc phæång phaïp thæí nghiãûm Phæång phaïp thæí nghiãûm laì cho chaûy chæång trçnh tæì mäüt säú dæî liãûu thæí âæåüc choün træåïc. Pheïp thæí nghiãûm duìng cho caí hai quaï trçnh xaïc minh vaì håüp thæïc hoïa V&V, våïi âiãöu kiãûn ràòng chæång trçnh laì chaûy âæåüc. Viãûc thæí nghiãûm phán biãût : 1. Caïc pheïp chæïng minh tênh âuïng âàõn hay khaío saït maî nguäön maì khäng chaûy chæång trçnh, våïi quy trçnh “walkthroughs” bàòng caïch chaûy demo (hand-made). 2. Chaûy chæång trçnh debugger âãø tçm sæía läùi. Caïc thæí nghiãûm vaì chaûy debugger thæåìng do caïc nhoïm cäng taïc khaïc nhau âaím nhiãûm. Âãø náng cao hiãûu quaí, ngæåìi ta thæåìng phán cäng nhæ sau : nhoïm thæí nghiãûm laì nhoïm khäng láûp trçnh, coìn nhoïm chaûy debugger laì nhoïm tham gia láûp trçnh ra saín pháøm. Quaï trçnh debugger gäöm nhiãöu giai âoaûn : 1. Tçm tháúy läùi sai (Locate error) 2. Tçm caïch khàõc phuûc läùi sai (Design error repair) 3. Khàõc phuûc läùi sai (Error repair) 4. Thæí nghiãûm laûi chæång trçnh (Re-teat program) Tçm tháúy Tçm caïch Khàõc phuûc Thæí nghiãûm läùi sai khàõc phuûc läùi sai läùi sai laûi chæång trçnh Hçnh 4.1. Quaï trçnh debugger Våïi nhæîng phæång phaïp láûp trçnh truyãön thäúng, quaï trçnh V & V laì khaío saït vaì thæí nghiãûm chæång trçnh. Thæûc tãú, viãûc thæí nghiãûm chiãúm mäüt pháön âaïng kãø trong quaï trçnh saín xuáút pháön mãöm, chiãúm khoaíng tæì 30% âãún 50%, tuìy theo baín cháút cuía dæû aïn Tin hoüc. II.1. Âënh nghéa vaì muûc âêch thæí nghiãûm Ngæåìi ta âæa ra nhuîng âënh nghéa sau âáy : Mäüt thæí nghiãûm laì cho chaûy (run) hay thæûc hiãûn (execution) mäüt chæång trçnh tæì nhuîng dæî liãûu âæåüc læûa choün âàûc biãût, nhàòm âãø xaïc minh kãút quaí nháûn âæåüc sau khi chaûy laì âuïng âàõn. Mäüt táûp dæî liãûu thæí laì táûp håüp hæîu haûn caïc dæî liãûu trong âoï mäùi dæî liãûu phuûc vuû cho mäüt thæí nghiãûm.
Thæí nghiãûm chæång trçnh 93 Mäùi pheïp thæí nghiãûm chè ra hoaût âäüng tæì viãûc thiãút kãú caïc táûp dæî liãûu thæí, tiãún haình thæí nghiãûm vaì âaïnh giaï kãút quaí âãún caïc giai âoaûn khaïc nhau trong chu kyì säúng cuía pháön mãöm. Ngæåìi thæí nghiãûm (hay nhoïm thæí nghiãûm) coï kiãún thæïc chuyãn män Tin hoüc coï nhiãûm vuû tiãún haình pheïp thæí nghiãûm. Mäüt khiãúm khuyãút (failure) xaíy ra khi chæång trçnh thæûc hiãûn cho ra kãút quaí khäng tæång håüp våïi âàûc taí cuía chæång trçnh. Mäüt läùi sai (error) laì mäüt pháön chæång trçnh (lãûnh) âaî gáy ra khiãúm khuyãút. Ngæåìi thæí nghiãûm coï nhiãûm vuû : 1. Taoû ra táûp dæî liãûu thæí. 2. Triãøn khai caïc pheïp thæí. 3. Láûp baïo caïo vãö kãút quaí thæí nghiãûm vaì læu giæî. Muûc âêch thæí nghiãûm laì âãø : 1. Chæïng minh ràòng chæång trçnh laì âuïng âàõn Âãø khàóng âënh tênh âuïng âàõn cuía chæång trçnh, cáön tiãún haình caïc thæí nghiãûm toaìn bäü (exhaustive testing), âoìi hoíi táûp dæî liãûu thæí phaíi hæîu haûn vaì coï kêch thæåïc væìa phaíi sao cho âuí sæïc thuyãút phuûc. Âiãöu naìy trãn thæûc tãú ráút khoï thæûc hiãûn. Sau âáy laì mäüt tiãu chuáøn näøi tiãúng cuía Dijkstra : “Caïc thæí nghiãûm cho pheïp chæïng minh mäüt chæång trçnh laì khäng âuïng, bàòng caïch chè ra mäüt phaín vê duû, tuy nhiãn, khäng bao giåì coï thãø chæïng minh âæåüc chæång trçnh âoï laì âuïng âàõn“. 2. Gáy ra nhæîng khiãúm khuyãút cuía chæång trçnh Myers G. J. trong baìi baïo “The Art of Software Testing“, Wiley 1979, âaî âënh nghéa thæí nghiãûm nhæ sau : “Pheïp thæí nghiãûm laì cho chaûy chæång trçnh nhàòm tçm ra nhæîng sai soït”. Tæì âoï, thæåìng ngæåìi ta noïi vãö “thæí nghiãûm phaï huíy“ (destructive testings). Muûc âêch cuía nhuîng pheïp thæí nhæ váûy laì táûp trung tçm ra caïc läùi sai tæì nhuîng khiãúm khuyãút do ngæåìi láûp trçnh phaûm phaíi. Ngæåìi thæí nghiãûm tiãún haình våïi muûc âêch nghëch (negative) : pheïp thæí laì thaình cäng nãúu tçm ra âæåüc khiãúm khuyãút, laì tháút baûi trong træåìng håüp ngæåüc laûi. Viãûc thæí nghiãûm kiãøu naìy thæåìng âæåüc aïp duûng trong quaï trçnh viãút chæång trçnh. 3. Âæa ra âaïnh giaï ténh (static evaluation - static benchmark) vãö cháút læåüng cuía chæång trçnh. Ngæåìi ta sæí duûng phæång phaïp “thæí nghiãûm ténh“ (static testing) cho muûc âêch naìy. Trong phæång phaïp phoìng tràõng, ngæåìi ta chè tiãún haình nhuîng pheïp thæí ténh, TS. PHAN HUY KHAÏNH biãn soaûn 93
94 Cäng nghãû Pháön mãöm nhàòm muûc âêch væìa âaím baío cäng viãûc cuía ngæåìi láûp trçnh væìa âaïnh giaï sæû tin cáûy cuía saín pháøm váûn haình. II.2. Thæí nghiãûm trong chu kyì säúng cuía pháön mãöm Ngæåìi ta phán biãût nhiãöu phæång phaïp thæí nghiãûm, tæång æïng våïi caïc giai âoaûn saín xuáút pháön mãöm khaïc nhau. Thæí Thæí nghiãûm Thæí nghiãûm Thæí Thæí nghiãûm Thæí nghiãûm “big bang” trãn xuäúng nghiãûm hãû thäúng nghiãûm Thæí nghiãûm têch håüp Hçnh 4.2. Nhiãöu phæång phaïp thæí nghiãûm II.2.1. Thæí nghiãûm âån thãø Thæí nghiãûm âån thã ø (Module testing), hay thæí nghiãûm âån vë (Unit testing) do ngæåìi láûp trçnh tæû tiãún haình. Phæång phaïp naìy hay âæåüc sæí duûng trong láûp trçnh cáúu truïc (top-down programing). Caïc phæång phaïp thæí nghiãûm khaïc do ngæåìi thæí nghiãûm tiãún haình. Giaí sæí goüi M laì mäüt âån thãø cáön thæí nghiãûm riãng biãût. Khi âoï, xaíy ra hai træåìng håüp nhæ sau : Træåìng håüp 1 : nhæîng âån thãø do M goüi tåïi khäng coï màût luïc thæí nghiãûm. Khi âoï, nhæîng âån thãø do M goüi tåïi vàõng màût phaíi âæåüc thay thãú båíi caïc chæång trçnh cuìng mäüt giao diãûn våïi M. Caïc chæång trçnh naìy thæûc hiãûn âuïng chæïc nàng maì chuïng âaûi diãûn cho âån thãø vàõng màût vaì chuïng âæåüc goüi laì caïc trçnh stubs (“cuäúng“). Âån thãø M Hçnh 4.3. Caïc âån thãø vàõng màût âæåüc thay båíi caïc trçnh stubs Vê duû, nãúu âån thãø âang âæåüc thæí nghiãûm goüi mäüt thuí tuûc sàõp xãúp åí âáöu : Procedure Sort (T: Array ; n: Integer); ngæåìi ta coï thãø sæí duûng trçnh Stub : Procedure Sort (T: Array ; n: Integer) ; Writeln (‘Daîy cáön sàõp xãúp laì : ‘) ; for i:= 1 to n do writeln (T[i]) ;
Thæí nghiãûm chæång trçnh 95 for i:= 1 to n do readln (T [i]) ; Tiãúp theo, ngæåìi thæí nghiãûm seî tiãún haình sàõp xãúp daîy âaî nháûp bàòng tay âãø thay thãú cho thuí tuûc sàõp xãúp vàõng màût. Træåìng håüp 2 : nhæîng âån thãø goüi tåïi M khäng coï màût luïc thæí nghiãûm. Khi âoï, âån thãø goüi tåïi M nhæng vàõng màût phaíi âæåüc thay thãú båíi mäüt chæång trçnh, âæåüc goüi laì trçnh driver. Trçnh driver goüi M âãø M thæûc hiãûn trãn caïc dæî liãûu thuäüc táûp dæî liãûu thæí, sau âoï ghi nháûn caïc kãút quaí tênh âæåüc båíi M âãø so saïnh våïi caïc kãút quaí chåì âåüi. Âån thãø M Hçnh 4.4. Duìng trçnh driver âãø goüi thæûc hiãûn M Säú læåüng caïc trçnh stubs vaì caïc trçnh drivers cáön thiãút âãø tiãún haình thæí nghiãûm caïc âån thãø phuû thuäüc vaìo thæï tæû caïc âån thãø âæåüc thæí nghiãûm. II.2.2. Thæí nghiãûm têch håüp Thæí nghiãûm têch håüp væìa nhàòm taûo mäúi liãn kãút giæîa caïc âån thãø, væìa âæåüc tiãún haình âäúi våïi nhæîng âån thãø låïn hçnh thaình hãû thäúng chæång trçnh hoaìn chènh. Coï nhiãöu phæång phaïp thæí nghiãûm têch håüp. 1. Phæång phaïp “big bang“ Ngæåìi ta xáy dæûng mäúi liãn hãû giæîa caïc âån thãø âãø taûo thaình mäüt phiãn baín hãû thäúng hoaìn chènh, sau âoï thæí nghiãûm phiãn baín naìy. Nhæ váûy ngæåìi ta cáön âãún nhiãöu trçnh drivers, mäùi trçnh driver cho mäüt âån thãø, mäüt trçnh stubs cho táút caí caïc âån thãø cuía hãû thäúng, træì âån thãø chênh phaíi âæåüc thæí nghiãûm bàòng phæång phaïp thæí nghiãûm âån vë. Phæång phaïp “big bang” nguy hiãøm : táút caí caïc sai soït coï thãø âäöng thåìi xuáút hiãûn, viãûc xaïc âënh tæìng läùi sai seî gàûp khoï khàn. Hån næîa phæång phaïp naìy âoìi hoíi mäüt læåüng täúi âa caïc trçnh drivers vaì caïc trçnh stubs. Vç váûy thæåìng ngæåìi ta sæí duûng caïc phæång phaïp têch håüp tæì trãn xuäúng, hay tæì dæåïi lãn. 2. Phæång phaïp thæí nghiãûm tæì trãn xuäúng (Descendant hay Top-down Testing Method) Bàõt âáöu thæí nghiãûm âån thãø chênh, sau âoï thæí nghiãûm chæång trçnh nháûn âæåüc tæì sæû liãn kãút giæîa âån thãø chênh vaì caïc âån thãø âæåüc goüi træûc tiãúp tæì âån thãø chênh, v.v TS. PHAN HUY KHAÏNH biãn soaûn 95
96 Cäng nghãû Pháön mãöm Phæång phaïp naìy chè cáön duìng mäüt trçnh driver duy nháút cho âån thãø chênh, nhæng cáön mäüt trçnh stub cho mäùi âån thãø coìn laûi. Level 1 Daîy caïc Level 1 thæí nghiãûm Level 2 stubs Level 2 Level 2 Level 2 Level 2 Level 3 stubs Hçnh 4.5. Phæång phaïp thæí nghiãûm tæì trãn xuäúng 3. Phæång phaïp thæí nghiãûm tæì dæåïi lãn (Ascendant hay Bottom-Up Testing Method) Bàõt âáöu thæí nghiãûm caïc âån thãø khäng goüi âãún caïc âån thãø khaïc, sau âoï caïc chæång trçnh nháûn âæåüc båíi sæû liãn kãút giæîa mäüt âån thãø chè goüi âãún caïc âån thãø âaî âæåüc thæí nghiãûm våïi caïc âån thãø naìy, v.v . . Phæång phaïp naìy âoìi hoíi mäùi âån thãø mäüt trçnh driver, nhæng khäng cáön trçnh stub. Mæïc N Mæïc N Mæïc N MæïcN Mæïc N Mæïc N-1 Mæïc N-1 Mæïc N-1 Hçnh 4.6. Thæí nghiãûm tæì dæåïi lãn Phæång phaïp tiãún toí ra æu âiãøm hån phæång phaïp luìi, do caïc trçnh driversæí duûng dãù viãút hån caïc trçnh stubs vaì coï caïc cäng cuû âãø taûo sinh tæû âäüng caïc trçnh drivers. Màût khaïc, thæï tæû têch håüp thæåìng bë raìng buäüc båíi thæï tæû coï màût cuía caïc âån thãø. II.2.3. Thæí nghiãûm hãû thäúng Váún âãö laì thæí nghiãûm pháön mãöm hoaìn chènh vaì pháön cæïng âãø âaïnh giaï hiãûu nàng, âäü an toaìn, tênh tæång håüp våïi caïc âàûc taí, v.v . . . Nhæîng thæí nghiãûm naìy âoìi hoíi nhiãöu thåìi gian. Ngæåìi ta noïi âãún thæí nghiãûm cháúp nháûn (Acceptance testing), laì nhæîng thæí nghiãûm phuì håüp våïi saín pháøm cuäúi cuìng qua håüp âäöng âaî kyï våïi khaïch haìng (nhiãöu khi viãûc thæí nghiãûm naìy do khaïch haìng tiãún haình), coìn âæåüc goüi laì thæí nghiãûm alpha vaì cuäúi cuìng laì thæí nghiãûm caìi âàût (Setup Testing), laì thæí nghiãûm âäúi våïi saín pháøm cuäúi cuìng, tiãún haình taûi vë trê
Thæí nghiãûm chæång trçnh 97 cuía khaïch haìng (våïi caïc maïy tênh vaì hãû âiãöu haình hoü âang sæí duûng). Ngæåìi ta goüi caïc thæí nghiãûm cho phiãn baín âáöu tiãn cuía pháön mãöm do khaïch haìng âæåüc læûa choün âàûc biãût tiãún haình laì thæí nghiãûm beta. II.2.4. Thæí nghiãûm häöi quy Ngæåìi ta coìn goüi caïc thæí nghiãûm tiãún haình sau khi sæía läùi laì thæí nghiãûm häöi quy, hay thoaïi lui (regresgion testing) nhàòm âãø xaïc minh nãúu caïc sai soït khaïc khäng âæåüc xæí lyï khi sæía chæîa. Kiãøn thæí nghiãûm naìy hay âæåüc duìng trong khi baío trç. Âãø tiãún haình hiãûu quaí caïc thæí nghiãûm naìy, cáön læu giæî laûi nhæîng thæí nghiãûm âaî laìm trong quaï trçnh saín xuáút pháön mãöm, âiãöu naìy giuïp cho viãûc xaïc minh tæû âäüng caïc kãút quaí thæí nghiãûm thoaïi lui. Khoï khàn gàûp phaíi laì trong säú nhæîng thæí nghiãûm âaî dàõt dáùn, cáön phaíi choün nhæîng thæí nghiãûm naìo chothæí nghiãûm thoaïi lui. Phæång caïch ngæåìi ta hay laìm laì kãút håüp mäùi lãûnh cuía chæång trçnh våïi táûp håüp caïc thæí nghiãûm laìm chaûy chæång trçnh. II.3. Dáùn dàõt caïc thæí nghiãûm Viãûc dáùn dàõt caïc thæí nghiãûm bao gäöm : - Xaïc âënh kêch thæåïc cuía táûp dæî liãûu thæí (váún âãö kãút thuïc caïc TN). - Læûa choün caïc dæî liãûu cáön thæí nghiãûm. - Xaïc âënh tênh âuïng âàõn hay khäng âuïng âàõn cuía caïc kãút quaí nháûn âæåüc sau khi thæûc hiãûn chæång trçnh âäúi våïi caïc dæî liãûu cuía táûp dæî liãûu thæí (Váún âãö låìi tiãn tri - oracle). Viãûc dáùn dàõt caïc thæí nghiãûm keìm theo viãûc viãút caïc chæång trçnh bäø tråü nhæ laì caïc stubs vaì caïc drivers. Váún âãö låìi tiãn tri Mäüt pheïp thæí nghiãûm (check program) Mäüt táûp håüp hæîu haûn caïc giaï trë âæa vaìo. Mäüt táûp håüp hæîu haûn caïc càûp (Giaï trë âæa vaìo, kãút quaí tæång æïng). Trong træåìng håüp 1, viãûc phaït hiãûn ra caïc khiãúm khuyãút phaíi âæåüc laìm bàòng tay (by hand), tæì âoï dáùn âãún mäüt cäng viãûc xem xeït kyî læåîng caïc kãút quaí máút thç giåì vaì mãût moíi (laìm haûn chãú kêch thæåïc caïc táûp dæî liãûu thæí). Coï hai kiãøu sai soït xaíy ra khi xem xeït : - Mäüt kãút quaí sai laûi âæåüc xem nhæ laì âuïng. - Mäüt kãút quaï âuïng coï thãø âæåüc hiãøu laì sai. Âãø traïnh xaïc minh bàòng tay, cáön phaíi coï nhæîng âàûc taí khaí thi, hay mäüt phiãn baín khaïc cuía chæång trçnh (âiãöu naìy coï nguy cå laìm lan truyãön sai soït tæì phiãn baín naìy sang phiãn baín khaïc). TS. PHAN HUY KHAÏNH biãn soaûn 97
98 Cäng nghãû Pháön mãöm Trong træåìng håüp thæï hai, chênh chæång trçnh âang chaûy tæû phaït hiãûn ra caïc khiãúm khuyãút, váún âãö laì tçm ra âæåüc caïc giaï trë âæa ra kãút quaí tæång æïng våïi giaï trë âæa vaìo. Âiãöu naìy coï thãø laìm “ bàòng tay “ våïi mäüt âàûc taí khaí thi, våïi mäüt phiãn baín cuía chæång trçnh, våïi cuìng nhæîng váún âãö âaî gàûp trong træåìng håüp âáöu. Ngæåìi ta cuîng coï thãø váûn duûng caïc pheïp thæí cuî âaî læu giæî. Chuï yï ràòng duìng chæång trçnh xaïc minh tênh âuïng âàõn cuía kãút quaí khäng luän luän âån giaín : nãúu xaíy ra coï nhiãöu caïi ra âuïng tæång æïng våïi moüt caïi vaìo thç phaíi âàût kãút quía do chæång trçnh tênh ra dæåïi daûng quy tàõc træåïc khi xaïc minh tênh nháút quaïn våïi kãút quaí dæû kiãún trong táûp dæî liãûu thæí. Âiãöu naìy khäng phaíi luän luän laìm âæåüc. Chàóng haûn laìm sao coï thãø xaïc minh âæåüc ràòng maî sinh ra båíi mäüt trçnh biãn dëch laì âuïng âàõn, nãúu chè thæí nghiãûm maî âoï maì thäi ? II.4. Thiãút kãú caïc pheïp thæí phaï huíy (Defect Testing) II.4.1. Caïc phæång phaïp dæûa trãn chæång trçnh Caïc phæång phaïp naìy coìn âæåüc goüi laì phæång phaïp coï cáúu truïc (Structural Testing) hay thæí nghiãûm häüp tràõng (white-box hay glass-box). Mäùi chæång trçnh tæång æïng våïi mäüt så âäö khäúi gäöm caïc cáúu truïc læûa choün vaì caïc cáúu truïc khäúi laì mäüt daîy täúi âa caïc lãûnh thæûc hiãûn (gäöm caïc lãûnh gaïn, lãûnh goüi chæång trçnh con, caïc lãûnh vaìo-ra ) maì khäng coï lãûnh reî nhaïnh. Ngæåìi ta goüi caïc khäúi lãûnh laì caïc âáöu vaìo så âäö khäúi vaì caïc quyãút âënh laì caïc cung âi ra tæì mäüt cáúu truïc læûa choün. a) Phuí caïc lãûnh (caïc âènh) Mäüt pheïp thæí laì phuí (truìm) hãút caïc lãûnh cuía mäüt chæång trçnh nãúu laìm cho mäùi lãûnh cuía noï âæåüc thæûc hiãûn. Âáy laì mäüt tiãu chuáøn täúi thiãøu : Ngæåìi ta khäng xeït nhæîng thæí nghiãûm maì mäùi lãûnh cuía chæång trçnh khäng âæåüc thæc hiãûn êt nháút mäüt láön. Chuï yï ràòng tiãu chuáøn naìy khäng phaíi luän luän thoía maîn bàòng mäüt chæång trçnh coï thãø chæïa caïc lãûnh maì khäng thãø âæåüc thæûc hiãûn. b) Phuí caïc quyãút âënh (caïc cung) Mäüt pheïp thæí phuí caïc quyãút âënh nãúu trong khi thæûc hiãûn, mäùi cung cuía så âäö täø chæïc cuía chæång trçnh âæåüc duyãût qua êt nháút mäüt láön : nghéa laì nãúu mäùi pheïp choün âæåüc thæûc hiãûn êt nháút mäüt láön cho mäùi giaï trë coï thãø (thuã hay fals e trong træåìng håüp gheïp reî nhaïnh logic). Nhæ váûy, tiãu chuáøn naìy khäng phaíi luän cáön phaíi thoía maîn. Vê duû : if A > 0 then if A ≥ 0 then . . . else . . .
Thæí nghiãûm chæång trçnh 99 c) Phuí caïc âiãöu kiãûn Ta xeït mäüt chæång trçnh chæïa cáúu truïc reî nhaïnh logic gäöm caïc lãûnh not, end vaì or. Mäüt pheïp thæí phuí caïc âiãöu kiãûn nãúu viãûc thæûc hiãûn chæång trçnh keïo theo sæû tênh giaï trë cuía biãøu thæïc naìy cho moüi giaï trë logic coï thã. Nhæ váûy mäüt biãøu thæïc coï hai toaïn haûng P, Q seî âæåüc tênh toaïn våïi : A B true true true false false true false false Pheïp phuí caïc âiãöu kiãûn cho pheïp cuíng cäú pheïp phuí caïc quyãút âënh. Vê duû coï thãø phuí caïc quyãút âënh bàòng caïch thæûc hiãûn pheïp læûa choün P vaì Q våïi : P = true, Q = true vaì P = false, Q = false, âiãöu naìy khäng cho pheïp phán biãût pheïp reî nhaïnh A or B. d) Phuí caïc läü trçnh thæûc hiãûn chæång trçnh (path testing) Mäüt pheïp thæí phuí caïc läü trçnh chaûy chæång trçnh nãúu gáy ra viãûc thæûc thi mäùi läü trçnh thæûc hiãûn chæång trçnh. Khäng täön taûi pheïp thæí nhæ váûy nãúu chæång trçnh coï vä haûn läü trçnh thæûc hiãûn trong træåìng håüp täøng quaït. Thäng thæåìng ngæåìi ta xáy dæûng pheïp thæí phuí caïc läü trçnh thæûc hiãûn coï säú læåüng ≤ mäüt hàòng âaî cho. e) Xaïc âënh dæî liãûu cho pheïp phuí läü trçnh thæûc hiãûn âàûc biãût Giaí thiãút ràòng våïi moüi lãûnh P cuía chæång trçnh vaì moüi quyãút âënh S, coï thãø tênh ptpre (P, S), âiãöu kiãûn âáöu yãúu nháút æïng våïi P vaì S. Ngæåìi ta coï thãø våïi moüi läü trçnh cuía chæång trçnh, tênh âæåüc mäüt cäng thæïc E sao cho caïc dæî liãûu cuía chæång trçnh thoía maîn E nãúu vaì chè nãúu viãûc thæûc hiãûn cuía chæång trçnh âi theo läü trçnh âaî choün. Âàûc biãût, E khäng laì sai nãúu vaì chè nãúu läü trçnh âaî choün laì läü trçnh thæûc thi. Nhæ váûy chè cáön tçm ra caïc dæî liãûu laìm thoía maîn E âãø coï pheïp thæí phuí läü trçnh âaî choün. Âiãöu naìy coï thãø thæûc hiãûn bàòng ta, hay chæïng minh mäüt caïch saïng taûo cäng thæïc xE. Phæång phaïp naìy âæåüc duìng âãø âënh nghéa pheïp thæí phuí caïc quyãút âënh cuía mäüt chæång trçnh : • Læûa choün mäüt táûp håüp caïc läü trçnh phuí caïc quyãút âënh. • Våïi mäùi läü trçnh, tênh âiãöu kiãûn âáöu yãúu nháút tæång æïng (hoàûc mäüt âiãöu kiãûn âáöu maûnh hån). • Tçm caïc dæî liãûu thoía maîn caïc âiãöu kiãûn âiãöu naìy. TS. PHAN HUY KHAÏNH biãn soaûn 99
100 Cäng nghãû Pháön mãöm f) Phuí caïc luäöng dæî liãûu Våïi mäùi biãún cuía chæång trçnh, ngæåìi ta goüi âënh nghéa laì mäüt træåìng håüp cuía biãún âoï, mäüt giaï trë âæåüc gaïn cho biãún (vê duû : x:=1, readln(x) ). Ngæåìi ta goüi sæí duûng laì mäüt træåìng håüp maì giaï trë cuía biãún âæåüc sæí duûng (vê duû : y:= x+y âäúi våïi biãún x). Trong caïc sæí duûng, ngæåìi ta phán biãût caïc sæí duûng trong caïc lãûnh khäng phaíi laì læûa choün, goüi laì C- sæí duûng, våïi C : calculus, caïc sæí duûng trong caïc lãûnh læûa choün, goüi laì P- sæí duûng, våïi P : Predicate. Mäüt pheïp thæí laì phuí caïc C-sæí duûng nãúu våïi mäùi biãún x, gáy ra viãûc thæûc thi måïi läü trçnh giæîa mäüt âënh nghéa x va ì mäüt C-sæí duûng âáöu tiãn cuîa x. Mäüt pheïp thæí laì phuí caïc P-sæí duûng nãúu, våïi mäùi biãún x gáy ra viãûc thæûc thi mäùi läü trçnh giæîa mäüt âënh nghéa x, vaì mäüt giaï trë læûa choün. II.4.2. Caïc phæång phaïp dæûa trãn âàûc taí Nhæîng phæång phaïp naìy coìn âæåüc goüi laì thæí nghiãûm chæïc nàng (funchæång trçnhional testing), ha thæí nghiãûm naìy, ngæåìi ta khäng chuï yï âãún chæång trçnh, maì chè laìm viãûc våïi âàûc taí chæïc nàng cuía chæång trçnh. Ngæåìi ta coï thãø thiãút kãú táûp dæî liãûu thæí træåïc khi viãút chæång trçnh. a) Caïc thæí nghiãûm toaìn thãø (Exhaustive Testing) Ngæåìi ta thæí nghiãûm chæång trçnh våïi táút caí dæî liãûu coï thãø vãö màût lyï thuyãút, âiãöu naìy chè laìm âæåüc nãúu táûp håüp dæî liãûu thæí laì hæîu haûn. Thæûc tãú, ngay caí khi táûp håüp dæî liãûu laì hæîu haûn thç thåìi gian thæûc hiãûn chæång trçnh cho caïc thæí nghiãûm toaìn thãø laì quaï låïn trong pháön låïn træåìng håüp. Vê duû : ⎯ 1. Tênh √ x , våïi x nguyãn giæîa 0 vaì 231 Våïi thåìi gian mäüt thæí nghiãûm laì 1s, khi âoï máút 231 = 2147483648 s. Mäüt nàm coï 365 x 24 x 3600s = 31536000s. Váûy thåìi gian mäüt thæûc nghiãûm toaìn thãø laì ≈ 68 nàm. 2. Thæí nghiãûm pheïp cäüng caïc soï nguyãn giæîa 0 vaì 231 Thåìi gian thæí nghiãûm mäüt pheïp cäüng laì 1 µs. Säú læåüng dæî liãûu laì : 231 x 231 = 262 ≈ 9.22 x 1018 Thåìi gian thæí nghiãûm toaìn thãø laì trãn 292 471 nàm. b) Caïc thæí nghiãûm båíi caïc låïp tæång âæång (Equivalence partioning) Nguyãn lyï : Phán hoaûch táûp håüp dæî liãûu thaình mäüt säú hæîu haûn låïp vaì læûa mäüt phán tæí (hay mäüt máùu phán tæí) trong mäùi låïp. Ngæåìi ta âàût trong cuìng mäüt låïp caïc
Thæí nghiãûm chæång trçnh 101 dæî liãûu âæåüc cho laì phuì håüp våïi chæång trçnh theo caïch âàûc taí. Nhæîng dæî liãûu naìy coï thãø cuìng gáy ra khiãúm khuyãút trong cuìng tçnh huäúng. Chuï yï cáön thæí nghiãûm caïc dæî liãûu nàòm åí phaûm vi giaïp ranh giæîa caïc låïp tæång âæång âãø phaït hiãûn caïc läùi sai kiãøu ≤ thæåìng láùn våïi <, v.v . . . c) Thæí nghiãûm âënh hæåïng båíi cuï phaïp (Syntax Controlled Testing) Khi dæî liãûu laì táûp håüp caïc chuäùi kyï tæû (caïc ngän ngæî láûp trçnh), chuïng âæåüc âàûc taí båíi caïc ätomat hæîu haûn, hoàûc båíi caïc vàn phaûm phi ngæî caính. Vê duû, nãúu pháön mãöm âæåüc thæí nghiãûm coï tênh tæång taïc qua laûi, nhæ caïc hãû âiãöu haình, thç táûp håüp daîy caïc haình âäüng coï thãø âæåüc âënh nghéa båíi mäüt ätämat hæîu haûn. Ngæåìi ta coï thãø âënh nghéa caïc táûp dæî liãûu thæí phuí caïc traûng thaïi âaût âæåüc, caïc cung, caïc läü trçnh coï âäü daìi bë chàûn, v.v . . . Khi táûp håüp dæî liãûu âæåüc âënh nghéa båíi mäüt vàn phaûm vi ngæî caính, ngæåìi ta coï thãø xáy dæûng pheïp thæí phuí caïc quy tàõc cuía vàn phaûm (mäùi quy tàõc âæåüc aïp duûng êt nháút mäüt láön âãø tiãún haình mäüt thæí nghiãûm). Chuï yï ràòng luïc naìy, ngæåìi ta chè coï thãø nháûn âæåüc dæî liãûu âuïng, viãûc nháûn âæåüc caïc dæî liãûu sai båíi cuìng phæång phaïp cáön thiãút phaíi viãút mäüt vàn phaûm saín sinh ra táûp håüp caïc dæî liãûu sai, âiãöu naìy laûi laì mäüt váún âãö hoïc buïa (vç ràòng buì cuía mäüt ngän ngæî PNC chæa chàõc âaî laì PNC). d) Caïc thæí nghiãûm ngáùu nhiãn (Random Testing) Âáy laì táûp dæî liãûu thæí sæí duûng caïc dæî liãûu láúy ngáùu nhiãn, tuán theo luáût xaïc suáút, chàóng haûn luáût âäöng âãöu, dãù tiãún haình nhæng thæåìng laì keïm hiãûu quaí. II.4.3. Kãút luáûn Hiãûn nay, ngæåìi ta thæåìng xáy dæûng pheïp thæí nghiãûm bàòng caïch phäúi håüp caïc thæí nghiãûm chæïc nàng vaì thæí nghiãûm cáúu truïc : ngæåìi ta bàõt âáöu thæí nghiãûm chæïc nàng træåïc (ngay khi âàûc taí yãu cáöu), sau âoï hoaìn thiãûn pheïp thæí nghiãûm båíi caïc tiãu chuáøn cáúu truïc (bao boüc caïc lãûnh, bao boüc caïc quyãút âënh ) khi coï âæåüc chæång trçnh. II.4.4. Caïc tiãu chuáøn kãút thuïc thæí nghiãûm Váún âãö âàût ra laì khi naìo thç kãút thuïc thæí nghiãûm ? hay cuû thãø hån laì xaïc âënh phaûm vi thæí nghiãûm nhæ thãú naìo ? Nãúu kãút thuïc thæí nghiãûm såïm thç coï thãø chæa tçm hãút läùi trong chæång trçnh. Coìn nãúu kãút thuïc muäün quaï thç laûi náng cao giaï thaình saín pháøm. Sau âáy laì mäüt säú tiãu chuáøn : TS. PHAN HUY KHAÏNH biãn soaûn 101
102 Cäng nghãû Pháön mãöm 1. Dæìng khi khäng coìn gáy ra âæåüc khiãúm khuyãút. Thæåìng thç mäüt chæång trçnh låïn bao giåì cuîng coï läùi, tiãu chuáøn naìy toí ra phi thæûc tãú, hån næîa máu thuáùn våïi muûc âêch cuía caïc thæí nghiãûm phaï huíy. 2. Dæìng khi thåìi gian (hay kinh phê) gia haûn cho thæí nghiãûm âaî hãút. Âãø tiãu chuáøn naìy coï hiãûu læûc thç phaíi âënh læåüng âæåüc táûp håüp caïc dæî liãûu thæí træåïc khi tiãún haình thæí nghiãûm. 3. Càn cæï vaìo kinh nghiãûm cuía caïc dæû aïn tæång tæû âaî hoaìn táút. Mäüt pheïp thæí nghiãûm bao boüc caïc quyãút âënh (hay 80% cuía caïc cung) khäng gáy ra khiãúm khuyãút. Váún âãö : Læa choün tuìy tiãûn cuía tiãu chuáøn. 4. Thæí nghiãûm chæìng 70 sai soït khäng âæåüc phaït hiãnû hay sau mäüt thåìi haûn 3 thaïng khäng xaíy ra. Váún âãö : Æåïc læåüng säú læåüng sai soït trong chæång trçnh, æåïc læåüng tyí lãû % caïc sai soït âæåüc phaït hiãûn båíi thæí nghiãûm, æåïc læåüng tyí lãû % sai soït phaûm phaíi trong caïc giai âoaûn phaït triãøn pháön mãöm vaì taûi giai âoaûn thæí nghiãûm maì nhæîng sai soït naìy âæåüc phaït hiãûn. 5. Thæí nghiãûm âãún khi säú læåüng sai soït tçm tháúy khäng coìn giaím theo mäüt caïch coï yï nghéa næîa. Váún âãö : Laìm sao æåïc læåüng âæåüc säú sai soït âaî giaím theo caïch coï yï nghéa ? 6. Phæång phaïp caïc âäüt biãún (Mutant method) Ngæåìi ta thay âäøi chæång trçnh bàòng caïch âæa vaìo caïc läùi. Caïc chæång trçnh bë thay âäøi âæåüc goüi laì caïc “âäüt biãún”. Mäüt pheïp thæí laì “täút” nãúu diãût âæåüc 100% (95%, v.v . . .) caïc “âäüt biãún” âoï. Váún âãö : Caïc sai soït âæa vaìo coï phaíi laì nhæîng sai soït thæûc tiãùn (coï thæûc)? II.5. Caïc pheïp thæí nghiãûm thäúng kã II.5.1. Måí âáöu Caïc pheïp thæí nghiãûm thäúng kã (Statistical Testing) nhàòm âãø âo âäü tin cáûy (reliability) cuía pháön mãöm, nghéa laì âo xaïc suáút chaûy äøn âënh vaì âuïng âàõn trong nhæïng âiãöu kiãûn sæí duûng cho træåïc. Caïc thæí nghiãûm phaï huíy khäng cho pheïp âaïnh giaï âæåüc tênh tin cáûy cuía mäüt chæång trçnh vç ràòng caïc thæí nghiãûm phaï huíy khäng tênh âãún caïc âiãöu kiãûn sæí duûng nhæ phæång phaïp naìy. Ngæåìi ta goüi khiãúm khuyãút (failure) laì nhæîng hiãûn tæåüng báút thæåìng xaíy ra laìm hãû thäúng âang thæûc thi dáùn âãún nhæîng hiãûu quaí khäng phuì håüp våïi âàûc taí ban âáöu. Mäüt khiãúm khuyãút coï thãø xaíy ra do pháön cæïng hoàûc do mäüt sai soït trong chæång trçnh. Sau âáy,û ngæåìi ta chè quan tám âãún nhæîng khiãúm khuyãút do läùi pháön mãöm gáy nãn.
Thæí nghiãûm chæång trçnh 103 Trong nhæîng âiãöu kiãûn sæí duûng âaî cho, sæû xuáút hiãûn thæåìng xuyãn caïc khiãúm khuyãút do caïc sai soït khaïc nhau gáy ra laì ráút biãún âäüng : mäüt säú sai soït gáy ra thæåìng xuyãn caïc khiãúm khuyãút, nhæîng sai soït khaïc thç ráút hiãúm, coï thãø khäng bao giåì xaíy ra trãn thæûc tãú. Viãûc thæûc thi mäüt pháön mãöm våïi mäüt dæî liãûu cäú âënh træåïc laì mäüt quaï trçnh coï tênh xaïc âënh gáy ra hoàûc laì mäüt kãút quaí âuïng, hoàûc laì mäüt khiãúm khuyãút. Nãúu ngæåìi ta åí trong nhæîng âiãöu kiãûn sæí duûng chæång trçnh, mäùi dæî liãûu coï thãø âæåüc cuía chæång trçnh seî cho mäüt xaïc suáút naìo âoï. Táûp håüp caïc dæî liãûu cungì xaïc suáút sæí duûng nhæ váûy âæåüc goüi laì mäüt máùu sæí duûng (use pattern) cuía chæång trçnh. Tæì mäüt màût càõt sæí duûng âaî cho, ngæåìi ta âënh nghéa xaïc suáút mäüt láön chaûy cho mäüt kãút quaí âuïng vaì xaïc suáút mäüt khiãúm khuyãút, coìn âæåüc goüi laì tyí suáút khiãúm khuyãút. Våïi mäüt mä hçnh âäüc láûp våïi thåìi gian, ngæåìi ta âënh nghéa âäü tin cáûy (reliability) cuía mäüt chæång trçnh nhæ laì xaïc suáút cuía sæû kiãûn “ láön chaûy sau cuía chæång trçnh laì âuïng “, nghéa laì 1,xaïc suáút cuía mäüt khiãúm khuyãút. Våïi mäüt mä hçnh phuû thuäüc thåìi gian, ngæåìi ta âënh nghéa âäü tin cáûy nhæ laì mäüt xaïc suáút cuía sæû kiãûn “chæång trçnh chaûy âuïng âàõn trong thåiì gian t”. Luïc naìy âäü tin cáûy laì mäüt haìm cuía thåìi gian. Caïc mä hçnh phuû thuäüc vaìo thåìi gian thæåìng âæåüc sæí duûng cho caïc pháön mãöm tæång häù (nhæ laì caïc hãû âiãöu haình). Tiãúp theo âáy, ngæåìi ta seî chè khai triãøn caïc mä hçnh âäüc láûp våïi thåìi gian. Khi xuáút hiãûn mäüt khiãúm khuyãút, nãúu laì mäüt khiãúm khuyãút vãö pháön cæïng, thç phaíi sæía chæîa, nãúu laì mäüt khiãúm khuyãút vãö pháön mãöm thç phaíi chaûy trçnh sæía läüi debugger. Sæía chæîa caïc hæ hoíng thuäüc vãö pháön cæïng laì âãø thay thãú nhæîng chi tiãút hæ hoíng, thiãút láûp laûi sæû váûn haình äøn âënh cuía thiãút bë nhæ træåïc. Coìn chaûy trçnh debugger laì âãø sæía caïc läùi vãö thiãút kãú, tàng âäü tin cáûy cuía pháön mãöm. Thæåìng ngæåìi ta sæí duûng âaûi læåüng liãn quan âãún âäü tin cáûy laì säú láön sæí duûng trung bçnh cho âãún khi xaíy ra khiãúm khuyãút (âäúi våïi mä hçnh âäüc láûp våïi thåìi gian), hoàûc sæí duûng sau mäüt thåìi gian trung bçnh naìo âoï âãún khi xaíy ra khiãúm khuyãút (âäúi våïi mä hçnh phuû thuäüc vaìo thåìi gian). Âaûi læåüng liãn quan âãún âäü tin cáûy MTTF (Mean Time To Failure : thåìi gian trung bçnh âãø xaíy ra khiãúm khuyãút) âæåüc tênh nhæ sau : Trong mä hçnh âäüc láûp våïi thåìi gian : Âäü äøn âënh = xaïc suáút mäüt láön chaûy âuïng. = 1 - xaïc suáút mäüt khiãúm khuyãút. TS. PHAN HUY KHAÏNH biãn soaûn 103
104 Cäng nghãû Pháön mãöm MTTF = säú láön sæí duûng trung bçnh cho âãún khi xaíy ra khiãúm khuyãút. = 1 / xaïc suáút mäüt khiãúm khuyãút. = 1/ (1 - Âäü äøn âënh). Tyí suáút khiãúm khuyãút laì nghëch âaío cuía MTTF. II.5.2. Æåïc læåüng âäü äøn âënh cuía mäüt pháön mãöm Âãø æåïc læåüng âäü äøn âënh hay khaí nàng váûn haình thäng suäút (reliability) cuía mäüt pháön mãöm, ngæåìi ta càn cæï vaìo kãút quaí cuía caïc pheïp thæí nghiãûm thäúng kã, nghéa laì caïc thæí nghiãûm ngáùu nhiãn thuìy theo máùu sæí duûng âaî choün. a) Phæång phaïp træûc tiãúp Giaí thiãút ràòng trong khi tiãún haình n pheïp thæí, ngæåìi ta gàûp d khiãúm khuyãút. Ta coï thãø æåïc læåüng âäü äøn âënh cuía pháön mãöm âang xeït båíi biãøu thæïc : 1 − d / n Phæång phaïp naìy chè coï thãø âæa ra mäüt æåïc læåüng täút vãö âäü äøn âënh nãúu säú caïc khiãúm khuyãút d laì coï nghéa (chàóng haûn âäü tin cáûy laì 1 nãúu khi thæí nghiãûm khäng xaíy ra khiãúm khuyãút naìo, âiãöu naìy khäng coï nghéa). Hån næîa, nãúu sau khi thæí nghiãûm, maì chaûy trçnh debugger, thç chæång trçnh seî bë thay âäøi vaì viãûc æåïc læåüng seî chè coìn håüp thæïc mäüt caïch coï âiãöu kiãûn khi giaí thiãút vãö cháút læåüng cuía quaï trçnh debugger. b) Phæång phaïp thæí nghiãûm giaí thuyãút (Hypothesis Testing) Váún âãö laì xáy dæûng mäüt táûp håüp caïc pheïp thæí nghiãûm maì kãút quaí âæåüc áún âënh træåïc cho pheïp khàóng âënh hay baïc boí âäü äøn âënh cuía pháön mãöm âang xeït coï mäüt giaï trë R våïi mäüt âäü tin cáûy x%. R vaì x thoaí maîn : 0 < R < 1 vaì 0 < x < 100 Caïc tham säú R vaì x cuîng nhæ quy caïch vãö kãút quaí âæåüc cäú âënh træåïc. Ngæåìi ta noïi chæång trçnh laì âæåüc kiãøm nghiãûm nãúu coï âäü äøn âënh R. Cho c = x/100, ta coï : 1 − c = xaïc suáút cho mäüt saín pháøm coï âäü äøn âënh tháúp hån âäü äøn âënh R.
CHÆÅNG 5 Âàûc taí pháön mãöm I. Måí âáöu âàûc taí pháön mãöm I.1. Khaïi niãûm vãö âàûc taí pháön mãöm I.1.1. Âàûc taí pháön mãöm laì gç ? Âàûc taí (specification) âæåüc âënh nghéa trong tæì âiãøn tiãúng Viãût (1997) : “Mä taí tháût chi tiãút mäüt bäü pháûn âàûc biãût tiãu biãøu âãø laìm näøi báût baín cháút cuía toaìn thãø”. Theo Computer Dictionary cuía Microsoft Press® (1994), âàûc taí laì sæû mä taí chi tiãút : Vãö màût pháön cæïng, âàûc taí cung cáúp thäng tin vãö caïc thaình pháön, khaí nàng vaì yãúu täú kyî thuáût cuía maïy tênh. Vãö màût pháön mãöm, âàûc taí mä taí mäi træåìng hoaût âäüng vaì chæïc nàng cuía chæång trçnh. Theo IBM Dictionary of Computing (1994), âàûc taí laì (1) mäüt daûng thæïc vàn baín chi tiãút cung cáúp caïc mä taí xaïc âënh vãö mäüt hãû thäúng nhàòm âãø phaït triãøn hay håüp thæïc hoaï. (2) Trong lénh væûc phaït triãøn hãû thäúng, âàûc taí laì mä taí caïch thiãút kãú, caïch bäú trê thiãút bë vaì caïch xáy dæûng chæång trçnh cho hãû thäúng. Nhæ váûy, âàûc taí laì sæû mä taí caïc âàcû træng nhàòm diãùn âaût caïc yãu cáöu vaì caïc chæïc nàng cuía mäüt saín pháøm pháön mãöm cáön thiãút kãú. Âàûc taí liãn quan âãún caïc âäúi tæåüng, caïc khaïi niãûm vaì caïc thuí tuûc naìo âoï cáön âãún khi phaït triãøn chæång trçnh. Âàûc taí coï caïc âàûc træng : • Tênh chênh xaïc (Correctness) • Tênh træìu tæåüng (Abstraction) • Tênh chàût cheî vãö màût Toaïn hoüc (Rigorousness) I.1.2. Caïc phæång phaïp âàûc taí Ngæåìi ta thæåìng sæí duûng 3 phæång phaïp âàûc taí : âàûc taí phi (khäng) hçnh thæïc, âàûc taí hçnh thæïc vaì âàûc taí häùn håüp. Âàûc taí phi hçnh thæïc (informal specification) âæåüc diãùn âaût bàòng ngän ngæî tæû nhiãn vaì toaïn hoüc. Tuy phæång phaïp âàûc taí naìy khäng chàût cheî nhæng dãù hiãùu vaì dãù diãùn âaût. Ta thæåìng sæí duûng khi cáön phaït biãøu caïc baìi toaïn, caïc yãu cáöu ban âáöu. TS. PHAN HUY KHAÏNH biãn soaûn 105
106 Cäng nghãû Pháön mãöm Vê duû û 1 : 1. Tçm nghiãûm cuía phæång trçnh f(x) = 0 våïi f(x) laì mäüt âa thæïc coï báûc cho træåïc sao cho våïi giaï trë thæûc x thç f(x) coï giaï trë bàòng 0. 2. Biãún âäøi mo mäüt ma tráûn vuäng A cáúp n × n vãö daûng tam giaïc trãn, nghéa laì ma tráûn A coï caïc pháön tæí nàòm phêa trãn âæåìng cheïo chênh thç bàòng 0. Âàûc taí hçnh thæïc (formal specification) âæåüc diãùn âaût bàòng ngän ngæî âaûi säú vaì logic toaïn, ráút chàût cheî, chênh xaïc vaì khäng nháúp nhàòng (non-ambiguous). Vê duû û 2 1. Tçm nghiãûm cuía phæång trçnh f(x) = 0 våïi f(x) laì mäüt âa thæïc coï báûc cho træåïc sao cho våïi giaï trë thæûc x thç f(x) coï giaï trë bàòng 0. 2. Biãún âäøi mo mäüt ma tráûn vuäng A cáúp n × n vãö daûng tam giaïc trãn, nghéa laì ma tráûn A coï caïc pháön tæí nàòm phêa trãn âæåìng cheïo chênh thç bàòng 0. Caïc tênh cháút cuía âàûc taí hçnh thæïc • âàûc taí mä taí nhæîng caïi phaíi laìm nhæng khäng phaíi mä taí laìm nhæ thãú naìo. • Láûp trçnh thãø hiãûn tæåìng minh viãûc læûa choün caïch khai triãøn : nghiãn cæïu thuáût giaíi, caïch viãút cäng thæïc • Âàûc taí cho pheïp diãùn taí âáöy âuí mäüt váún âãö, giaím täúi thiãøu tênh phæïc taûp cuía hãû thäúng âang xeït. • Âàûc taí phaíi cho pheïp kiãøm tra âæåüc quaï trçnh phaït triãøn pháön mãöm (cháút læåüng vaì tênh tin cáûy) Âàûc taí hçnh thæïc liãn quan âãún : - Cáúu truïc dæî liãûu vaì caïc haìm (kiãøu dæî liãûu) - Thåìi gian - Thao taïc - Âån thãø hay âäúi tæåüng. Tênh âaûi säú càn cæï trãn viãûc âënh nghéa caïc kiãøu dæî liãûu, tênh hiãûu quaí âaûi säú âæåüc xaïc âënh båíi caïc cäng cuû toaïn hoüc, âaûi säú vaì logic. Âàûc taí häùn håüp (Mixing Specification) phäúi håüp giæîa hai phæång phaïp : hçnh thæïc vaì phi hçnh thæïc. Thæåìng mä taí phi hçnh thæïc nhàòm laìm giaíi thêch roî hån, dãù hiãøu hån mäüt khi mä taí hçnh thæïc quaï phæïc taûp. I.1.3. Caïc thê duû minh hoüa Mä taí caïc cáúu truïc dæî liãûu : Cho ma tráûn vuäng A cáúp n × n, n ≥ 1 :
Âàûc taí 107 A = {ai j | i = 1 n, j = 1 n} gäöm caïc pháön tæí ai j åí haìng i, cäüt j Bäún âènh (goïc) cuía ma tráûn A laì a11, a1n, ann vaì an1 Âæåìng cheïo chênh laì vector d1 = {aii | i = 1 n} Âæåìng cheïo phuû laì vector d2 = {ai, n - i + 1 | i = 1, n} Pháön tæí ai j âäúi xæïng våïi aj i qua âæåìng cheïo chênh d1 Pháön tæí ai j âäúi xæïng våïi an - j + 1 qua âæåìng cheïo phuû d2 Ma tráûn tam giaïc trãn : A0 = { ai j | ai j ≠ 0, ∀ i = 1 n, j = i n ∧ ai j = 0, ∀ i = 2 n, j = 1 i - 1 } Ma tráûn tam giaïc dæåïi : 0 A = { ai j | ai j ≠ 0, ∀ i = 1 n, j = 1 i ∧ ai j = 0, ∀ i = j n - 1, j = 2 n } I.2. Âàûc taí vaì láûp trçnh Trong nhæîng træåìng håüp coï thãø, ngæåìi ta hæåïng âàûc taí vãö mäüt ngän ngæî láûp trçnh naìo âoï. Vê duû vãö âàûc taí âãû qui cho baìi toaïn thaïp Haì näüi (Tower of Hanoi). Cho chäöng n âéa n = 64 xãúp thaình hçnh thaïp åí cäüt A (låïn nháút dæåïi cuìng vaì nhoí dáön lãn trãn). Haîy chuyãøn chäöng n âéa naìy qua cäüt B theo nguyãn tàõc sau : 1. Mäùi láön chè di chuyãøn mäüt âéa tæì cäüt naìy qua cäüt kia 2. Khäng âàût âéa to lãn âéa nhoí 3. Láúy vë trê cäüt C âãø âàût taûm caïc âéa trung gian Sau âáy laì baìi toaïn Thaïp Haì näüi våïi n = 3 âéa. Hçnh 5.1. Chäöng âéa træåïc khi chuyãøn Hçnh 5.2. Chäöng âéa sau khi chuyãøn (våïi7 láön xãúp) TS. PHAN HUY KHAÏNH biãn soaûn 107
108 Cäng nghãû Pháön mãöm a) Caïch giaíi phi hçnh thæïc Chuyãøn n - 1 âéa tæì A qua C láúy B laìm cäüt trung gian, sau âoï chuyãøn âéa dæåïi cuìng tæì A sang B. Tiãúp tuûc chuyãøn n - 1 âéa tæì C qua B láúy A laìm cäüt trung gian theo caïch trãn. b) Caïch giaíi hçnh thæïc bàòng âàûc taí Goüi thuí tuûc chuyãøn n âéa tæì A qua B láúy C laìm trung gian (n > 0) laì : Haì_näüi (n, A, B, C) vaì thuí tuûc chuyãøn mäüt âéa tæì A qua B laì : Chuyãøn_mäüt_âéa(A, B). Khi âoï, ta coï âàûc taí : Haì_näüi (n, A, B, C) = if n > 0 then begin Haì_näüi (n - 1, A, C, B); Chuyãøn_mäüt_âéa (A, B); Haì_näüi (n - 1, C, B, A) End ta dãù daìng viãút caïc thao taïc trãn thaình thuí tuûc nhæ sau : Procedure ChuyãønCäüt(n, A, B, C: TãnCäüt); Begin if n>0 then begin ChuyãønCäüt(n-1, A, C, B); Chuyãøn_mäüt_âéa_tæì_A_sang_C; ChuyãønCäüt(n-1, B, A, C); End End; Thao taïc Chuyãøn_mäüt_âéa_tæì_A_sang_C; âæåüc viãút thaình lãûnh : Writeln(‘Chuyãøn mäüt âéa tæì ‘, A:1, ‘ -> ‘, C:1); Thãm biãún âãúm i âãø tênh säú bæåïc chuyãøn âéa, chæång trçnh âáöy âuí nhæ sau : Program HanoiTower; Type TãnCäüt = 1 3; Var i, N: Integer; Procedure ChuyãønCäüt(n, A, B, C: TãnCäüt); Begin if n>0 then begin ChuyãønCäüt(n-1, A, C, B); i:=i+1; Writeln(i:3,‘Chuyãøn mäüt âéa tæì ‘,A:1,‘ -> ‘,C:1); ChuyãønCäüt(n-1, B, A, C); End End; Begin Write(‘Säú âéa cáön chuyãøn : ‘);
Âàûc taí 109 Readln(N); i:=0; ChuyãønCäüt; Readln End. Chaûy chæång trçnh trãn seî cho kãút quaí nhæ sau : Säú âéa cáön chuyãøn : 4 1.Chuyãøn mäüt âéa tæì 1 -> 2 2.Chuyãøn mäüt âéa tæì 1 -> 3 3.Chuyãøn mäüt âéa tæì 2 -> 3 4.Chuyãøn mäüt âéa tæì 1 -> 2 5.Chuyãøn mäüt âéa tæì 3 -> 1 6.Chuyãøn mäüt âéa tæì 3 -> 2 7.Chuyãøn mäüt âéa tæì 1 -> 2 8.Chuyãøn mäüt âéa tæì 1 -> 3 9.Chuyãøn mäüt âéa tæì 2 -> 3 10.Chuyãøn mäüt âéa tæì 2 -> 1 11.Chuyãøn mäüt âéa tæì 3 -> 1 12.Chuyãøn mäüt âéa tæì 2 -> 3 13.Chuyãøn mäüt âéa tæì 1 -> 2 14.Chuyãøn mäüt âéa tæì 1 -> 3 15.Chuyãøn mäüt âéa tæì 2 -> 3 Trong træåìng håüp täøng quaït n âéa, säú bæåïc chuyãøn âéa seî laì : 20 + 21 + . . . + 2n = 2n - 1 láön. Våïi n=64, giaí sæí thåìi gian âãø chuyãøn mäüt âéa laì t giáy, thç thåìi gian âãø chuyãøn hãút 64 âéa cuía baìi toaïn Thaïp Haì näüi seî laì : (264 - 1) × t = 1.8446744074E+19 × t giáy. Mäüt nàm coï 365 × 24 × 60 × 60 = 31 536 000 giáy, giaí sæí t = 10-2 giáy thç säú nàm cáön âãø chuyãøn 64 âéa laì : (1.8446744074E+19 / 31536000) × 10-2 = 5.8494241735E+11 ≈ 5.8 tyí nàm ! Baìi táûp : 1, 2, 3, 4, 5 trang 140-141 (Nguyãùn Xuán Huy). II. Âàûc taí cáúu truïc dæî liãûu II.1. Cáúu truïc dæî liãûu cå såí vectå II.1.1. Dáùn nháûp Cho mäüt cuäún tæì âiãøn. Cáön tra cæïu mäüt tæì åí mäüt trang naìo âoï báút kyì : Duyãût láön læåüt caïc tæì, tæì âáöu tæì âiãøn, cho âãún khi gàûp tæì cáön tra cæïu, goüi laì tçm tuáön tæû (giäúng tãûp tuáön tæû) TS. PHAN HUY KHAÏNH biãn soaûn 109
110 Cäng nghãû Pháön mãöm Nãúu tæì âiãøm âaî âæåüc sàõp xãúp ABC, coï thãø tçm ngáùu nhiãn mäüt tæì, sau âoï tuìy theo tæì âaî gàûp maì tçm phêa træåïc hay phêa sau tæì âoï tæì cáön tra cæïu. Coï thãø xem tæì âiãøn laì mäüt vectå cho pheïp tçm kiãúm ngáùu nhiãn mäüt tæì. Trong tin hoüc, bäü nhåï maïy tênh cuîng xem laì mäüt vectå gäöm caïc ä nhåï læu træî dæî liãûu II.1.2. Âàûc taí hçnh thæïc Cho mäüt táûp giaï trë E vaì mäüt säú nguyãn n ∈ N. Mäüt vectå laì mäüt aïnh xaû V tæì khoaíng I ⊂ N vaìo E. V : I → E, I = [1 n], n laì säú pháön tæí cuía V, hay kêch thæåïc. V coï thãø räùng nãúu n = 0 Kyï hiãûu vectå båíi (V[1 n], E) hoàûc E : V[1 n], hoàûc V nãúu khäng coï sæû hiãøu nháöm. Mäüt pháön tæí cuía vectå laì càûp (i, V[i]) våïi i ∈ [1 n], âãø âån giaín ta viãút V[i]. Mäüt vectå coï thãø âæåüc biãøu diãùn båíi táûp caïc pháön tæí cuía noï : (V[1], V[2], , V[n]) hay (x1, x2, , xn) nãúu xi = V[i], laì caïc giaï trë (træûc kiãûn) Vectå con : Ta goüi thu heûp cuía V trãn mäüt khoaíng liãn tiãúp cuía [1 n] laì vectå con cuía V[1 n] : V[ i j], j > i, räùng nãúu i > j Vê duû : V[1 5] = (7, 21, -33, 6, 8) Caïc vectå con : V[2 4] = (21, -33, 6) V[1 3] = (7, 21, -33) v.v II.2. Truy nháûp mäüt pháön tæí cuía vectå Cho V[1 n]. Våïi ∀ i ∈ [1 n], pheïp truy nháûp V[i] seî cho giaï trë pháön tæí coï chè säú i cuía V. Kãút quaí khäng xaïc âënh nãúu i ∉ [1 n] Vê duû : V[1 5] = (7, 21, -33, 6, 8) V[2] = 21, V[4] = 6 nhæng V[0], V[7] khäng xaïc âënh. Vectå âæåüc sàõp xãúp thæï tæû (SXTT) Ta noïi : - Vectå räùng (n = 0) laì vectå âæåüc SXTT. - Vectå chè gäöm 1 pháön tæí (n = 1) laì vectå âæåüc SXTT. - Vectå V[1 n], n > 1 laì vectå âæåüc SXTT nãúu ∀ i ∈ [1 n - 1], ∀ [i] ≤ ∀ [i + 1] Coï thãø âënh nghéa âãû qui 3 :
Âàûc taí 111 V[1 i] âæåüc SXTT, V[i] ≤ V[i + 1] ⇒ V[i i + 1] âæåüc SXTT, våïi i ∈ [1 n - 1] Mäüt säú kyï hiãûu khaïc : a ∈ V[1 n] ⇔ ∃ j ∈ [1 n], a = V[j] a ∉ V[1 n] ⇔ ∀ j ∈ [1 n], a ≠ V[j] a , ≥ , = vaì ≠ . Âãø xeït caïc thuáût toaïn xæí lyï vectå, ta sæí duûng mä taí dæî liãûu : Const n = 100 ; Type Vectå = anay [1 n] of T ; {T laì kiãøu cuía caïc pháön tæí cuía vectå} II.3. Caïc thuáût toaïn xæí lyï vectå Duyãût vectå Cho V[1 n], thuáût toaïn duyãût vectå âæåüc viãút âãû quy nhæ sau : Procedure scan (V: vectå; i, n: integer); Begin if i 0) ⇒ (check, pháöntæí ∉ V)} ∨ (not check, pháöntæí ∉ V)} Var i: integer; TS. PHAN HUY KHAÏNH biãn soaûn 111
112 Cäng nghãû Pháön mãöm begin i:= 1; {pháöntæí ∉ V[1 i - 1], i ≤ n} while (V[i] n then check := false else if V[i] = phántæí then check := true else check := check (V, i + 1, n, phántæí) end; Khi goüi haìm, i coï thãø nháûn giaï trë báút kyì, tæì 1 n, âàûc biãût i = 1 Træåìng håüp duyãût vectå tæì phaíi qua traïi, ta khäng cáön duìng biãún i næîa : function check (V:Vectå; n: integer; phántæí: T): Boolean; {n ≥ 0 ⇒ (check, phántæí ∈ V) V (Not check, phántæí ∉ V)} begin if n = 0 then check := false else if V[n] = phántæí then check := true else check := check (V, n - 1, phántæí) end; b) Vectå âæåüc sàõp xãúp thæï tæû Ta cáön tçm chè säú i ∈ [1 n] sao cho thoía maîn : V[1 i - 1] < pháöntæí ≤ V[i n] 1 i n V[1 i - 1] < pháöntæí pháöntæí ≤ V[i n] Hçnh 5.3. Vectå âæåüc sàõp xãúp thæï tæû Váún âãö laì kiãøm tra âàóng thæïc pháöntæí = V[i] khäng trong V âaî âæåüc sàõp xãúp ? Láûp luáûn :
Âàûc taí 113 Giaí sæí âaî xæí lyï i - 1 (1 ≤ i ≤ n + 1) phán tæí âáöu cuía V vaì V[1 i - 1] 0 ⇒ (checknum, phán tæí ∈ V) ∨ (Not checknum, pháöntæ í ∉ V)} Var i: integer ; begin if phán tæí > V[n] then checknum := false { not checknum, phántæí ∉ V)} else begin {phántæí ≤ V[n]} i := 1 ; {V[1 i - 1] 1) âaî âæåüc sàõp xãúp thæï tæû : ∀ i ∈ [1 n - 1], V[i] ≤ V[i +1] Ta chia V thaình 3 vectå con V[1 m - 1], V[m m] vaì V[m + 1 n] âæåüc sàõp xãúp thæï tæû sao cho : V[1 m - 1] ≤ V[m] ≤ V[m + 1 n] Xaíy ra 3 træåìng håüp : ∈ V[1 m - 1] nãúu phán tæí V[m] TS. PHAN HUY KHAÏNH biãn soaûn 113
114 Cäng nghãû Pháön mãöm luïc naìy ta tråí laûi baìi toaïn âaî xeït : tçm phán tæí trong vectå V[1 m - 1] hoàûc V[m +1 n]. Kãút thuïc nãúu phán tæí = V[m] Mäüt caïch täøng quaït, láön læåüt xaïc âënh daîy caïc vectå coï V1, V2, , Vk sao cho mäùi Vi coï kêch thæåïc nhoí hån kêch thæåïc cuía vectå con træåïc âoï Vi - 1 Âãø yï ràòng nãúu choün V1 = V[1 n], V2 = V[2 n], , Vk = V[k n], ta âi âãún pheïp tçm kiãúm tuáön tæû âaî xeït åí trãn. Ta seî choün m laì vë trê giæîa (nãúu n leí) âãø cho V[1 m - 1] vaì V[m + 1 n] coï kêch thæåïc bàòng nhau, hoàûc choün m sao cho chuïng hån keïm nhau mäüt phán tæí. Khi âoï kêch thæåïc cuía caïc vectå thuäüc daîy V1, V2, , Vk seî láön læåüt âæåüc chia âäi taûi mäùi bæåïc : n, n/2, , n/2k - 1. Nhæ váûy, seî coï täúi âa [ log2n] vectå con khaïc räùng. Vê duû : nãúu n = 9000, säú vectå con khaïc räùng täúi âa seî laì 13, vç 213 = 8192 Xáy dæûng thuáût toaïn : Sau mäüt säú bæåïc, ta coï vectå con V[inf sup] sao cho : V[1 inf - 1] sup (inf = sup + 1) (V[1 inf-1] V[m] : tiãúp tuûc tçm kiãúm trong V[m + 1 sup] láúy inf := m + 1 âãø coï laûi khàóng âënh V[1 inf - 1] < pháön tæí Nhæ váûy caí hai træåìng håüp : V[1 inf - 1] < pháön tæí < V[sup + 1 n] Khåíi âáöu, láúu inf := 1 vaì sup := n Ta coï thuáût toaïn nhæ sau : function binary (V:vectå; n:integer; phántæí:T): Boolean; {V âæåüc SXTT ⇒ (binary, phántæ∈í V)∨(not binary, phántæ∉í V)} Var inf, sup, m : integer ; OK : Boolean ; begin OK : false ; {not OK, phán tæí ∉ V}
Âàûc taí 115 inf := 1 ; sup := n ; {V[1 inf - 1] phántæí} {(V[1 inf - 1] sup then NhëPhán:= false else begin m := (inf + sup) div 2 ; if V[m] = phántæí then NhëPhán:= true else if V[m] < phántæí then NhëPhán:= NhëPhán(V, m+1, sup, phántæí) else NhëPhán:= NhëPhán(V, inf, m - 1, phántæí) end end ; Haìm naìy coï thãø âæåüc goüi våïi caïc giaï trë inf, sup báút kyì, thäng thæåìng âæåüc goüi båíi doìng lãûnh : NhëPhán (V, 1, n, pháöntæí) b) Phæång aïn 2 Coï thãø tçm ra nhæîng phæång aïn khaïc cho thuáût toaïn tçm kiãúm nhë phán. Chàóng haûn, thay vç kiãøm tra âàóng thæïc V[m] = pháöntæí, ta kiãøm tra khàóng âënh : V[1 inf - 1] < pháöntæí ≤ V[inf n] Ssau âoï kiãøm tra pháöntæí = V[inf] âãø coï cáu traí låìi. TS. PHAN HUY KHAÏNH biãn soaûn 115
116 Cäng nghãû Pháön mãöm Màût khaïc, coï thãø thay âäøi giaï trë traí vãö cuía haìm tçm kiãúm nhë phán båíi vë trê cuía phán tæí trong vectå, bàòng 0 nãúu phán tæí ∉ V. Nãúu inf = 1, khàóng âënh coï daûng V[1 0] 0) ⇒ (m ∈ [1 n] NhëPhán = m, V[m] = phántæí) V (NhëPhán = 0, phán tæí ∉ V)} Var m, inf, sup : integer ; begin if phán tæí > V[n] then nhë phán := 0 else begin inf := 1 ; sup := n ; {V[1 inf - 1] < phántæí ≤ V[sup n]} while inf < sup do begin m := (inf + sup) div 2 ; if pháöntæî ≤ V[m] do sup := m {phátæí ≤ V[sup n]} else inf := m + 1 {V[1 inf - 1] < phán tæí} {V[1 inf - 1] < phán tæí ≤ V[sup n]} end ; {(inf = sup, V[1 inf - 1] < phán tæí ≤ V[inf n] ⇒ (V[1 inf - 1] < phántæí ≤ V[inf n]} if phántæí = V[inf] then NhëPhán:= inf else NhëPhán:= 0 end end ;
Âàûc taí 117 III. Âàûc taí âaûi säú : mä hçnh hoïa phaït triãøn pháön mãöm (Pháön naìy chè phuûc vuû tham khaío) III.1. Måí âáöu Âàûc taí âaûi säú khäng mä taí caïc yãúu täú liãn quan âãún thåìi gian thæûc thi cuîng nhæ traûng thaïi. Ngän ngæî âàûc taí traûng thaïi liãn quan âãún : - Ngæî nghéa (Semantic) - Cuï phaïp (syntax) - Caïc thuäüc tênh (Properties) Hçnh veî Ngæî nghéa cuía caïc âàûc taí âaûi säú liãn quan âãún : - Dáúu kê (signature) cuía mäüt kiãøu âaûi säú træìu tæåüng - Haûng (term) våïi caïc biãún - Phæång trçnh vaì caïc tiãn âãö - Caïc mä hçnh âàûc biãût Cuï phaïp cuía âàûc taí âaûi säú Vê duû : Xáy dæûng kiãøu string cho caïc xáu kyï tæû cuìng caïc pheïp toaïn thäng duûng trãn xáu nhæ sau : - Taûo xáu räùng måïi (pheïp toaïn new) - Gheïp xáu (append) - Thãm mäüt kyï tæû vaìo xáu (add to) - Láyú âäü daìi xáu - Kiãøm tra xáu räùng (is empty) - Kiãøm tra hai xáu bàòng nhau khäng (=) - Trêch kyï tæû âáöu tiãn cuía xáu (frist) Âãø âënh nghéa kiãøu string, ngæåìi ta coìn sæí duûng caïc kiãøu sau : - char : kiãøu cuía kyï tæû - nat : kiãøu cuía säú nguyãn - bool : kiãøu giaï trë logic TS. PHAN HUY KHAÏNH biãn soaûn 117
118 Cäng nghãû Pháön mãöm Tãn caïc táûp håüp vaì caïc pheïp toaïn trãn táûp håüp xaïc âënh mäüt kyï dáúu (signature). Nhæ váûy mäüt dáúu kê âæåüc xáy dæûng tæì : - Tãn caïc kiãøu âàûc taí - Tãn caïc pheïp toaïn våïi viãûc chè roî miãön xaïc âënh (domain) vaì miãön trë (range) nhæ sau : tãn pheïp toaïn : miãön xaïc âënh → miãön trë Ta xáy dæûng dáúu kê tæì kiãøu string nhæ sau Adt String ; Use char, Not, Bool ; Sorts string ; Operations new : → string ; append _ _ : String, string → string ; add _ to _ : char, string → string ; # _ : String → not ; is empty ? _ string → bool ; _ = _ : string, string → bool ; frist _ : string → char ; Tãn xuáút hiãûn trong mäüt dáúu kê gäöm hai loaûi laì coï êch (internest) vaì bäø tråü (auxiliary) tuìy theo vai troì cuía chuïng. Vê duû : - String laì coï êch - Char, not vaì bool laì bäø trå ü Cuï phaïp (cp) Cp âàûc taí âaûi säú sæí duûng trong vê duû trãn âæåüc chia ra thaình caïc khäúi : âáöu, giao tiãúp vaì thán cuía âàûc taí. Mäùi khäúi gäöm mäüt säú khai baïo ngàn caïch nhau båíi caïc tæì khoïa (coï gaûch chán) Âäúi våïi khäúi giao tiãúp (interface), ngæåìi ta sæí duûng caïc khaïi niãûm tiãön täú (prefix), trung täú (infix) vaì háûu täú (postfix) nhæ sau : Tiãön täú : tãn cuía pheïp toaïn âæåüc âàût træåïc daîy caïc tham biãún Vê duû : appenend _ _ : string, string → string ; Tæì âoï ngæåìi ta coï thãø viãút caïc haûng dæåïi daûng : append x y hay append (x y) hay (append x y) Trung täú : cho pheïp âënh nghéa toaïn tæí hay vë tæì Vê duû _ = _ : string, string → bool ; tæì âoï coï thãø viãút cacï haûng dæåïi daûng :
Âàûc taí 119 x = y hay (x = y) Häùn håüp : cho pheïp viãút caïc biãøu thæïc báút kyì mäüt caïch mãöm deío nhæ add_to_ : char, string → string tæì âoï coï thãø viãút caïc haûng dæåïi daûng : add c to append (x y) Trong nhiãöu træåìng håüp trãn âáy, caïc càûp dáúu ngoàûc dáúu âæåüc duìng âãø phán caïch caïc haûng våïi nhau III.2. Phán loaûi caïc pheïp toaïn Caïc pheïp toaïn âæåüc chia ra thaình 2 loaûi : Loaûi quan saït âæåüc (oprations) Loaûi phaït sinh (generator operations) Loaûi quan saït âæåüc coï caïc daûng sau : Kiãøu coï êch [vaì kiãøu bäø tråü] → Kiãøu bäø tråü Vê duû : _ = _ : string, string → bool; # _ : string → not ; is empty ? : string → bool ; first _ : string → char ; Loaûi phaït sinh coï daûng : Kiãøu coï êch [vaì kiãøu bäø tråü] → Kiãøu coï êch Vê duû : new : _ → string ; add_ to _ : char, string → string ; ÅÍ âáy, pheïp toaïn new taûo ra mäüt xáu räùng, coìn pheïp toaïn add _ to _ thãm mäüt kyï tæû vaìo xáu. Caïc tiãn âãö âæåüc xáy dæûng tæì caïc pheïp toaïn duìng cho caïc kiãøu bäø tråü giaí sæ í âæåüc âënh nghéa nhæ sau : true : → bool ; false : → bool ; not _ : bool → bool ; _ and _ : bool, bool → bool ; _ or _ : bool ; bool → bool ; 0 : → not ; TS. PHAN HUY KHAÏNH biãn soaûn 119
120 Cäng nghãû Pháön mãöm 1 : → not ; succ : not → not ; _ + _ : not, not → not : _ - _ : not, not → not : _ * _ : not, not → not : _ / _ : not, not → not : _ = _ : not, not → bool; a : → char ; b : → char ; _ = _ : char, char → bool ; III.3. Haûng vaì biãún Trong âàûc taí âaûi säú, caïc biãún âæåüc âënh kiãøu vaì coï thãø nháûn giaï trë tuìy yï tuìy theo kiãøu âaî âënh nghéa. Vê duû : khai baïo kiãøu x : string ; y : string ; c : char ; âënh nghéa caïc biãún x, y, c âãø sæí duûng trong caïc haûng sau âáy : add c to x = append (x y) append (is empty ? (new), add x to x) Haûng laì mäüt biãøu thæïc nháûn âæåüc tæì viãûc täø håüp liãn tiãúp caïc pheïp toaïn cuía singnature (dáúu kê). Mäüt haûng laì håüp thæïc nãúu haûng âoï thoía maîn caïc pheïp toaïn âaî sæí duûng (kiãøu vaì vë trê). Qui tàõc quy naûp âæåüc duìng âãø xáy dæûng táûp håüp caïc haûng + coï kiãøu s âæåüc viãút t : s âæåüc âënh nghéa nhæ sau : + : s1, s2, , sn → s ∧ t1 : s1, t2 : s2, , tn : sn (f t1 t2 tn) : s trong âoï sæí duûng quy tàõc khai baïo kiãøu biãún x : s Tæì âoï, haûng håüp thæïc trong hai haûng tæì vê duû væìa xeït laì add c to x = append (x y) III.4. Pheïp thãú caïc haûng Pheïp thãú (substitutions) laì mäüt pheïp toaïn trãn caïc haûng cho pheïp thay thãú caïc biãún (coï màût) trong caïc haûng båíi caïc haûng khaïc. Táûp håüp caïc biãún FV xuáút hiãûn trong mäüt haûng âæåüc âënh nghéa mäüt caïch âãû quy nhæ sau : FV (ft1t2 tn) = FV (t1) ∪ FV (t2) ∪ FV (t2) ∪ ∪ FV (tn)
Âàûc taí 121 FV (x) = {x} Vê duû : FV (append (is empty ? (new), add c to x)) = {x, c} Pheïp thãú trong mäüt haûng t cho caïc thaình pháön chæïa biãún x båíi haûng u, kyï hiãûu t [u /x], âæåüc âënh nghéa nhæ sau : Våïi x ∈ FV (t) thç (f t1 t2 tn) [u/ x ] = (f t1 [u/ x] t2 [u/ x] tn [u/ x]) y [u/ x] = u y = x = y y ≠ x Vê duû : append ( is empty ? (new), (add c to x)) [(add c to y) / x] = append (is empty ? (new), (new), ( add c to ( add c’ to y))) Mä taí caïc thuäüc tênh qua caïc phæång trçnh Caïc tiãn âãö sæí duûng trong âàûc taí âæåüc xáy dæûng theo logic vë trê báûc 1 daûng phæång trçnh (pt) Mäüt phæång trçnh håüp thæïc coï vãú traïi vaì vãú phaíi cuìng kiãøu haûng : AX spec = {t = t’ | t : s ∧ t’ : s} Trong vê duû vãö âa kiãøu string, pheïp toaïn is empty ? âæåüc âënh nghéa theo phæång trçnh : is empty ? (new) = true ; Coï nghéa mäüt xáu væìa måïi taûo ra laì räùng - sau âoï, viãûc thãm mäüt kyï tæû måïi vaìo xáu seî cho kãút quaí laì false : is empty ? (add c to x) = false ; Tênh âãû quy cuía phæång trçnh : append (x, add c to y) = add c to (append (x, y)) ; chè ra ràòng viãûc gheïp mäüt xáu våïi xáu âæåüc taûo ra bàòng caïch thãm mäüt kyï tæû vaìo xáu naìy thç cuîng coï giaï trë nhæ gheïp hai xáu træåïc räöi sau âoï thãm mäüt kyï tæû vaìo xáu kãút quaí. Âiãöu âoï håüp lyï vç ta coï tênh cháút cuía phæång trçnh : append (x, new) = x ; nghéa laì gheïp mäüt xáu naìo âoï våïi xáu räùng cuîng cho ra kãút quaí chênh xáu âoï Ta coï caïc tiãn âãö vãö xáu kyï tæû nhæ sau : Axioms is empty ? (new) = true ; is empty ? (add c to x) = false ; # new = 0 ; # (add c to x) = x (x) = + 1; TS. PHAN HUY KHAÏNH biãn soaûn 121
122 Cäng nghãû Pháön mãöm append (x, new) = x ; append (x, add c to y) = add c to append (x y) ; (new = new) = true ; add c to x = true ; (add c to x = new) = false ; (new = add c to x) = false ; (add c to = add d to y) = (c = d) and (x = y) ; where where x, y : string ; c, d : char ; end string ; Caïc tiãn âãö âiãöu kiãûn Caïc tiãn âãö âiãöu kiãûn têch cæûc (positive conditional axions) laì måí räüng cuía caïc phæång trçnh, chuïng laì caïc mãûnh âãö Horm vãö tênh bàòng nhau, coï daûng : t1 = t1’ ∧ t2 = t2’ ∧ ∧ tn = t’n ⇒ t = t’ Vê duû : is empty ? (x) = flase ⇒ first (add c to x) = first (x) ; is empty ? (x) = true ⇒ first (add c to x) = c ; III.5. Caïc thuäüc tênh cuía âàûc taí Âàûc taí âàût ra hai váún âãö sau âáy : - Håüp thæïc hoïa - Læåîng nàng chæïng baïc (completude) cuía âàûc taí III.5.1. Mä hçnh láûp trçnh (triãøn khai) Caïc mä hçnh láûp trçnh mä taí caïch thæïc triãøn khai cuía âàûc taí. Coï nghéa caïc chæång trçnh træìu tæåüng seî kiãøm chæïng caïc thuäüc tênh âaî trçnh baìy trong âàûc taí (thiãút láûp). Táûp håüp caïc mä hçnh âàûc taí våïi caïc pheïp toaïn keìm theo âæåüc kyï hiãûu Mod (spec). Khaïi niãûm láûp trçnh dáùn âãún quan hãû thoía maîn kyï hiãûu Æ xaïc âënh tênh triãøn khai âuïng âàõn cuía âàûc taí. Ta coï : M ∈ Mod (spec) ⇔ (∀t, t’ : s vaì t = t’ ∈ Ax spec ta coï M Æ t = t’) Våïi moüi tiãn âãö : t = t’ cuía Ax spec Mod (spec) Æ t = t’ ⇔ ∀M ∈ Mod (spec),
Âàûc taí 123 M Æ t = t’ III.5.2. Mä hçnh âàûc biãût Nhæîng mä hçnh cháúp nháûn âæåüc båíi mäüt âàûc taí ráút phong phuï. Sau âáy laì mäüt vê duû vãö mä hçnh cho âàûc taí kiãøu Bool : Hçnh veî trong hai mä hçnh A vaì B åí trãn, âàûc taí kiãøu Bool thoîa maîn våïi caïc quy æåïc coï giaï trë laì caïc dáúu x, caïc pheïp toaïn biãøu diãùn båíi caïc quan hãû giæîa miãön xaïc âënh vaì miãön trë. Chuï yï ràòng A chæïa caïc giaï trë vä êch tæång tæû nhæ viãûc sæí duûng 1 byte cho kiãøu Bool, coìn B chæïa væìa âuí (täúi thiãøu) giaï trë cáön thiãút tæång tæû nhæ sæí duûng 1 bit cho kiãøu Bool. III.5.3. Mä hçnh âäöng dæ Mä hçnh naìy laì mäüt thæång âaûi säú caïc haûng âäöng dæ âënh nghéa båíi caïc quy tàõc sau âáy : - t = t’ laì tiãn âãö khi âoï t ~ t’ - Phaín xaû : t ~ t - Âäúi xæïng : t ~ t’ ⇒ t’ ~ t - Bàõc cáöu : t = t’ ∧ t’ ~ t’’ ⇒ t ~ t’’ - Khaí thãú : (cáúu thaình - substitutivite) t1 ~ t1’ ∧ t2 ~ t2’ ∧ ∧ tn ~ tn’ ⇒ (ft1t2 tn) ~ (ft1’t2’ tn’) - Thay thãú : cho x laì biãún, u laì haûng t ~ t’ ⇒ t [u/ x] ~ t’ [u/ x] Quaï trçnh khai triãøn mäüt âàûc taí Khai triãøn mäüt âàûc taí laì váún âãö khoï khàn. Nhæîng âënh nghéa vãö cuï phaïp caïc chæïc nàng mong âåüi khäng laì khoï khàn nhæng tênh âuïng âàõn cuía chuïng laûi khäng kiãøm chæïng âæåüc dãù daìng. III.6. Pheïp chæïng minh trong âàûc taí âaûi säú Muûc âêch pháön naìy laì chè ra caïch chæïng minh (chæïng minh) caïc thuäüc tênh trong caïc âàûc taí âaûi säú. Mäüt thuäüc tênh cáön chæïng minh coï daûng mäüt âënh lyï, chàóng haûn daûng mäüt phæång trçnh. Giaí sæí ta cáön chæïng minh thuäüc tênh sau âáy trong âàûc taí caïc säú nguyãn tæû nhiãn dæång Not : succ (0) = succ (succ (0)) = succ (succ (0))) ? succ (0) + succ (0)) = succ (succ (succ (0))) TS. PHAN HUY KHAÏNH biãn soaûn 123
124 Cäng nghãû Pháön mãöm Tiãn âãö : succ (x) + y = succ (x + y) Quy tàõc thay thãú våïi s = {x = 0, y = succ (succ(0))} succ (0) + succ (succ (0)) = succ (0 + succ(succ (0))) Tiãn âãö : 0 + x = x vaì quy tàõc thay thãú våïi s = { x = succ (succ (0)))} 0 + succ (succ (0)) = succ (succ (0)) Quy tàõc thay thãú våïi pheïp succ trãn (2) succ (0 + succ (succ (0))) = succ (succ (0))) Quy tàõc bàõc cáöu cho (1) vaì (3) 5. Âënh lyï âaî âæåüc chæïng minh. Cáön chuï yï ràòng thuäüc tênh naìy laì håüp thæïc cho moüi quaï trçnh âàûc taí säú tæû nhiãn Not. III.6.1. Lyï thuyãúttæång âæång Lyï thuyãút tæång âæång (cuía mäüt âàûc taí) âæåüc xáy dæûng tæì caïc tiãn âãö cuía âàûc taí, laì táûp håüp caïc âënh lyï håüp thæïc qua caïc quy tàõc sau âáy : - Phaín xaû : t = t - Âäúi xæïng : t = t’ ⇒ t’ = t - Bàõc cáöu : t = t’ ∧ t’ = t’’ ⇒ t’ = t’’ - Khaí thãú : t = t’ ∧ t2 = t2’ ∧ ∧ tn = tn’ ⇒ (ft1, t2, , tn) = (ft1’, t2’, , tn’) - Pheïp thãú : cho x laì biãún vaì u laì haûng t1 = t1’ ∧ t2 = t2’ ∧ ∧ tn = tn’ ⇒ t = t’ khi âoï t1 [u/ x] = t1’ [u/ x] ∧ ∧ tn [u/ x] = tn’ [u/ x] ⇒ t [u/ x] = t’ [u/ x] - Pheïp càõt : Cond1 ∧ (u = u’) ∧ cond2 ⇒ t = t’ vaì cond ⇒ x = x’, khi âoï : cond1 ∧ cond ∧ cond2 ⇒ t = t’ Caïc qui tàõc cuía lyï thuyãút tæång âæång thãø hiãûn caïc thuäüc tênh bàòng nhau (phaín xaû, âäúi xæïng vaì bàõc cáöu), thuäüc tênh haìm (khaí thãú), caïc biãún (pheïp thãú) vaì thay thãú caïc vãú bàòng nhau (pheïp càõt). Caïc quy tàõc naìy xaïc âënh pheïp suy diãùn Ã EQ, âënh lyï sau âáy minh hoüa kêch chàõc chàõn vaì tênh roî cuía pheïp suy diãùn Âënh lyï : lyï thuyãút tæång âæång våïi mäüt âàûc taí spec, ∀t = t’, Ax spec Ã EQ t = t’ ⇔ Mod (Ax spec) Æ t = t’
Âàûc taí 125 Cäng thæïc Mod (Ax spec) Æ t = t’ chè ra ràòng phæång trçnh laì håüp thæïc trong moüi caïch láûp tyíçnh coï thãø. Tuy nhiãn coï thãø xaíy ra mäüt säú træåìng håüp âàûc biãût khi mä hçnh khäng håüp lyï, luïc âoï coï thãø true = false. Ta coï thãø chæïng minh ràòng thuäüc tênh succ (succ (0)) - succ (succ (0)) = 0 laì håüp thæïc (valid), nhæîng thuäüc tênh succ (succ (succ (0))) - succ (succ (0)) = 0 Khäng laì håüp thæïc trong âàûc taí âang xeït, vç ràòng sau khi suy diãùn, ta nháûn âæåüc succ (0) = 0 laì khäng håüp thæïc. Ta coï thãø tháúy ràòng x - x = 0 khäng chæïng minh âæåüc trong ngæî caính âang xeït màûc dáöu âënh lyï naìy toí ra hiãøn nhiãn trong âàûc taí. Tæì âoï, ta coï thãø bäø sung thãm mäüt säú giaí thiãút cho mä hçnh âãø tàng khaí nàng chæïng minh coï thãø. III.6.2. Khaïi niãûm vãö lyï thuyãút quy naûp Nhæ âaî chè ra, ta cáön thãm caïc âënh lyï täøng quan hån âãø coï khaí nàng suy diãùn tæì caïc tiãn âãö cuía âàûc taí, chàóng haûn nhæ x + y = y + x laì khäng coï tênh suy dáön trong lyï thuyãút tæång âæång. Ta seî thãm vaìo caïc qui tàõc sæí duûng trong lyï thuyãút tæång âæång mäüt quy tàõc måïi nhæ sau : - Qui naûp : giaí sæí G laì cäng thæïc sao cho x laì mäüt biãún tæû do, nãúu våïi moüi t, G [t/ x] laì suy diãùn âæåüc thç G cuîng suy diãùn âæåüc cho t. Quy tàõc naìy chè roî ràòng coï thãø kãút luáûn ràòngnãúu viãûc chæïng minh mäüt âënh lyï laì håüp thæïc cho moüi træåìng håüp, âënh nghéa båíi mäüt haûng, båíi mäüt biãún thç âënh lyï cuîng håüp thæïc cho cäng thæïc âæåüc læåüng hoïa mäüt caïch phäø duûng trãn biãún nay.ì Tæång tæû âäúi våïi âënh lyï tæång âæång, âënh lyï sau âáy cho kãút quaí thuyãút phuûc cho viãûc suy diãùn quy naûp âäúi våïi âàûc taí hæîu haûn. Âënh lyï 3.2 : Lyï thuyãút quy naûp Våïi mäüt âàûc taí âaûi säú spec ∀t = t’, Ax spec Ã Ind t = t’ ⇔ ModGen (Ax spec) Æ t = t’ Ta seî minh hoüa nguyãn lyï naìy båíi mäüt vê duû trãn caïc giaï trë logic xáy dæûng tæì caïc pheïp toaïn true, false vaì not. Ta muäún chæïng minh ràòng : not (not (b)) = b - træåìng håüp cå såí : ? not (not (true)) =not (false) = true ; 2. Not (not (false)) = not (true) = false ; TS. PHAN HUY KHAÏNH biãn soaûn 125
126 Cäng nghãû Pháön mãöm - Khäng quy naûp : not (not (b)) = b suy ra not (not (not (b))) = not (b) quy tàõc khaí thãú våïi not cho not (not (b)) = b not (not (not (b))) = not (b) Nhåì quy tàõc quy naûp maì thuäüc tênh mong muäún âæåüc chæïng minh. Nhæ váûy lyï thuyãút quy naûp cho pheïp chæïng minh tênh giao hoaïn cuía pheïp cäüng trong Not qua x + y = y+ x viãûc chæïng minh cáön quy naûp hai láön trãn x vaì y. III.6.3. Chæïng minh tæû âäüng båíi viãút laûi Viãûc chæïng minh båíi viãút laûi (demonstration by rewriding) laì mäüt kyî thuáût cho pheïp chæïng minh tæû âäüng. Âoï laì quaï trçnh æåïc læåüng caïc haûng bàòng caïch viãút laûi mäüt caïch hãû thäúng caïc haûng thaình caïc daûng chuáøn (daûng khäng thãø æåïc læåüc âæåüc næîa) vaì pheïp chæïng minh caïc thuäüc tênh. Nguyãn lyï sæí duûng laì hæåïng âãún caïc phæång trçnh âàûc taí theo quy tàõc viãút laûi vaì aïp duûng liãn tiãúp caïc quy tàõc naìy trãn caïc haûng âaî æåïc læåüc. Vê duû : tæì tiãn âãö not true = false ta seî dáùn âãún quy tàõc not true ??? false. Quy tàõc naìy âæåüc duìng âãø chæïng minh tênh bàòng nhau cuía daûng t = t’. Sæû bàòng nhau laì håüp thæïc nãúu hai vã ú cuía chuïng âæåüc viãút laûi thaình duy nháút mäüt haûng khäng thãø æåïc læåüc âæåüc næîa. Âënh lyï 3.3 Chæïng minh båíi viãút laûi Våïi mäüt âàûc taí spect, t, t’’ laì caïc haûng nãúu t ??? ??? to vaì t’ ??? to thç : Ax spec Ã EQ t = t’ ÅÍ âáy ta sæí duûng kyï hiãûu t ???* t’ cho daîy t ??? ??? t hay t laì mäüt daûng chuáøn cuía haûng, nghéa laì mäüt haûng khäng thãø thu goün. Cáön chuï yï ràòng âàóng thæïc taûo ra båíi viãút laûi khäng bàõt buäüc âäöng nháút våïi âàóng thæïc nháûn âuåüc tæì hãû thäúng suy diãùn Ã EQ (khäng hoìan toaìn). Âãø coï thãø thæûc hiãûn caïc pheïp chæïng minh theo lyï thuyãút træåïc âáy, ta cáön nháûn âæåüc mäüt hãû thäúng viãút laûi häüi tuû tæång âæång våïi hãû thäúng sinh båíi caïc tiãu âãö. Giaíi phaïp âáìu tiãn laì hæåïng tåïi caïc phæång trçnh, Nãúu hãû thäúng nháûn âæåüc laì âi âãún âêch (moüi hæåïng suy dáøn khaïc nhau coï thãø âãöu dáøn vãö cuìng kãút quaí) vaì kãút thuïc (sau mäüt säú hæîu haûn bæåïc viãút laûi træåïc khi nhán âæåüc daûng chuáøn). Tæì âoï caïc thuäüc tênh chæïng minh âæåüc tæång âæång våïi caïc phæång trçnh xuáút phaït. Chàóng haûn âãø âàûc taí Bool, ta cáön nháûn âæåüc bàòng caïch hæåïng caïc tiãn âãö tæì traïi qua phaíi : not (true) ??? false
Âàûc taí 127 not (false) ??? true true and b ??? b false and b ??? false true or b ??? true false or b ??? b false xor b ??? not (b) Vê duû : sæí duûng caïc quy tàõc trãn âãø viãút laûi haûng sau âáy : not (false or (true and false)) not (true and false) not (false or false) not (false) true Tuy nhiãn, nguyãn lyï hæåïng vãö viãút laûi khäng âuí âãø chæïng minh moüi thuäüc tênh tæång âæång. Ta coï thãø minh hoüa âiãúu âoï trong âàûc taí caïc säú tæû nhiãn mäüt caïch âån giaín nhæ sau : Interface Sort not ; Operations 0 : → not ; _ _ : not → not ; _ + _ : not not → not ; Body Axions a x 1 0 + x = x ; a x 2 : x + (- x) = 0 ; Tæì âàûc taí trãn, ta coï thãø xáy dæûng caïc quy tàõc : 0 + x ??? x x + (- x) ??? 0 - 0 ??? 0 TS. PHAN HUY KHAÏNH biãn soaûn 127
128 Cäng nghãû Pháön mãöm Cáön chuï yï ràòng trong træåìng håüp naìy, viãûc hæåïng caïc quy tàõc tæì traïi qua phaíi chæa âuí, vç nãúu muäún chæïng minh - 0 = 0 thç phaíi cáön aïp duûng tiãn âãö 1 tæì phaíi qua traïi, sau âoï aïp duûng tiãn âãö 2 tæì traïi qua phaíi, nhæ váûy seî khäng tæång æïng våïi viãûc læûa choün âënh håïng ???. Roî raìng viãûc âënh hæåïng laì mäüt cå chãú chæïng minh chæa âáöy âuí, âàûc biãût âäúi våïi caïc tiãn âãö vãö caïc pheïp tênh sinh. Cå chãú naìy coï thãø âáöy âuí trong nhiãöu tçnh huäúng thæûc tãú. Trong træåìng håüp caïc tiãn âãö khäng âënh hæåïng nhæ pheïp giao hoaïn, caïc kyï thuáût âàûc taí âæåüc phaït triãøn âãø thæûc hiãûn viãút laûi (hãû viãút laûi kiãøu modun kãút håüp - giao hoaïn) Caïc pheïp toaïn phaït sinh (xáy dæûng) Theo âënh nghéa, mäüt mä hçnh âæåüc phaït sinh båíi mäüt táûp håüp con w caïc pheïp toaïn nãúu moüi giaï trë cuía mä hçnh naìy nhán âæåüc båíi mäüt haûng âæåüc xáy dæûng tæì caïc bäü sinh w. Âënh nghéa naìy cho pheïp, theo dënh lyï quy naûp, chè xem xeït caïc bäü sinh trong caïc chæïng minh bàòng caïch chè chæïng minh quy naûpchuïng (båíi vç moüi haûng âaût âæåüc båíi caïc viãûc täø håüp caïc bäü sinh) III.6.4. Phán cáúp trong âàûc taí âaûi säú Caïc mä hçnh phán thãø laìm thoía maîn caïc tiãn âãö vaì caïc haûn chãú do caïc raìng buäüc âån thãø chuí yãúu dæûa trãn khaí nàng buäüc âån thãø. Caïc raìng buäüc âån thãø chuí yãúu dæûa trãn khaí nàngkhäng bë xaïo träün giæîa caïc mä hçnh åí mæïc phán cáúp tháúp hån khi sæí duûng mäüt âàûc taí. Nguyãn lyï naìy cho pheïp sæí duûng viãûc phán cáúp caïc âàûc taí trong caïc giai âoaûn khai triãøn, âàûc biãût khi laìm mën (refinement). Coï nghéa laì caïc mä hçnh phaíi âæåüc láûp trçnh âäüc láûp våïi nhau. Caïc kiãøu xaïo träün coï thãø xuáút hiãûn trong mäüt âàûc taí âaûi säú laì : - “junk” (maíng) : caïc giaï trë âæåüc thãm vaìo båíi viãûc duìng caïc âån thãø, raìng buäcü vãö tênh âáöy âuí haûn chãú kiãøu xaïo träün naìy. - “cofusion” (träün láùn) : caïc giaï trë bë thay âäøi (collapse), do raìng buäüc vãö sæû hiãûn hæîu phán cáúp laìm aính hæåíng âãún âàûc taí. Låïp caïc mä hçnh phán cáúp âæåüc kyï hiãûu båíi Hitol (spec) âoï laì nhæîng mä hçnh thoía maîn quy tàõc vãö sæû haûn chãú caïc mä hçnh trãn caïc mä hçnh con baío toaìn âæåüc âæåüc ngæî nghéa cuía chuïng. Tênh roî raìng (Completude suffisance) Ta seî minh hoüa tçnh huäúng “junk” bàòng mäüt vê duû Adl Khäng_hoaìn_toaìn ; In terface Use Not, Bool ;
Âàûc taí 129 Operation f : not → bool ; Body Axioms f (succ (x)) = false ; where x : not ; End ; Vê duû trãn khäng roî raìng khi thãm âënh nghéa haìm f trãn caïc âån thãø vãö not vaì bool. Caïc tiãn âãö vãö âån thãø cuía haìm f seî laìm xaïo träün caïc kiãøu âaî âënh nghéa. Ta tháúy mäüt giaï trë måïi f (0) kiãøu seî khäng âæåüc xaïc âënh vç khäng coï tiãn âãö naìo chè ra f (0) laì true hay false. IV. Âàûc taí hay caïch cuû thãø hoïa sæû træìu tæåüng (Specification or How to Make Abstrations Real) IV.1. Âàûc taí pheïp thay âäøi bäü nhåï Giaí sæí ta cáön âàûc taí pheïp thay âäø näüi dung mäüt bäü nhåï. Âãø âån giaín hoïa maì khäng laìm máút tênh âæåüc biãøu diãùn båíi så âäö sau : 10 20 30 bäü nhåï chè gäöm 3 âëa chè nhåï chæïa 3 giaï trë luïc âáöu âãöu laì 0 giaí lãûnh, laìm thay âäøi näüi dung cuía bäü nhåï âæåüc kyï hiãûu båíi chg (x, y) Vê duû lãûnh chg (2, 5) laìm thay âäøi âëa chè thæï 2 tæì giaï trë 0 thaình 5 : 1 0 1 0 2 0 chg (2, 5) 2 5 3 0 3 0 Nhæ váûy, lãûnh chg (x, y) âaî thay âäøi näüi dung cuía âëa chè x thaình giaï trë y vaì giæî nguyãn näüi dung cuía caïc âëa chè coìn laûi. Goüi q laì bäü nhåï luïc âáöu vaì q’ laì bäü nhåï nháûn âæåüc sau khi thæûc hiãûn lãûnh chg (x, y), ta coï thãø chuyãøn så âäö trãn thaình daûng âiãöu kiãûn nhæ sau : q chg (x, y) q’ (1.1) TS. PHAN HUY KHAÏNH biãn soaûn 129
130 Cäng nghãû Pháön mãöm Ta noïi lãûnh chg (x, y) âaî chuyãøn bäü nhåï q thaình q’. Âënh nghéa ngæî nghéa cuía lãûnh chg chênh laì âàûc taí, nhåì viãút âiãöu kiãûn tæång âæång våïi âiãöu kiãûn (1.1) Vê duû sæû kãút håüp caïc âiãöu kiãûn sau âáy âãø âàûc taí pheïp toaïn thay âäøi chg : q’ (x) = y q’ (a) = q (a) nãúu a ≠ x (1.2) Nhæ váûy ta âaî ngáöm áøn thæìa nháûn ràòng q vaì q’ chè âënh caïc haìm. Trong vê duû naìy, våïi bäü nhåï 3 âëa chè, miãön xaïc âënh cuía haìm laì táûp håüp {1, 2, 3} täøng quaït caïc âëa chè vaì miãön giaï trë laì caïc giaï trë coï thãø læu træî âæåüc trong bäü nhåï âang xeït, chàóng haûn laì táûp håüp caïc säú nguyãn {-231, , 231} (1.3) Mäüt caïch täøng quaït, goüi A laì táûp håüp caïc âëa chè, V laì táûp håüp caïc giaï trë, ta coï: q ∈ A → V (1.4) Nhæ váûy mäüt biãøu thæïc daûng q (a) chè coï nghéa nãúu a ∈ A, tæì âoï q (a) chè coï nghéa nãúu a ∈ A, tæì âoï q (a) ∈ V. Do bäü nhåï q’ nháûn âæåüc tæì q sau khi thæûc hiãûn lãûnh chg, q’ cuîng thoía maîn âiãöu kiãûn (1.4) q’ ∈ A → V Tuy nhiãn âiãöu kiãûn (1.2) khäng phaíi luän luän coï nghéa vç ràòng biãøu thæïc q’ (x) âoìi hoíi x ∈ A. Ta tháúy âiãöu kiãûn (1.1) dáùn âãún (1.2) nhæng ngæåüc laûi khäng hoaìn taìon âuïng. Ta coï thãø haûn chãú caïc âiãöu kiãûn (1.2) âãø coï âæåüc âiãöu kiãûn tæång âæång nhæ sau x ∈ A y ∈ V q’ (x) = y (1.5) q’ (a) = q (a) våïi x ≠ a vaì x ∈ A Trong (1.5), hai âiãöu kiãûn âáöu âæåüc goüi laì âiãöu kiãûn âáöu (preconditions), hai âiãöu kiãûn sau âæåüc goüi laì caïc âiãöu kiãûn sau (postconditions) Ta cáön kiãøm tra (1.5) laì cháúp nháûn âæåüc, nghéa laì coï âiãöu kiãûn (1.4) laì báút hiãún (invariant). Muäún váûy ta cáön chæïng minh âënh lyï sau âáy : ((1.4) vaì (1.5)) keïo theo (1.4)’ (1.6) Âënh lyï vãö tênh cháúp nháûn âæåüc (plausibility) Ta coï thãø näúi hai âiãöu kiãûn tæång âæång (1.1) vaì (1.5) q chg (x, y) q’ x ∈ A y ∈ V (1.7)
Âàûc taí 131 q’ (x) = y q’ (a) = q (a) våïi x ≠ a vaì a ∈ A Ngæåìi ta noïi q xaïc âënh traûng thaïi (state) cuía hãû thäúng, mäüt âiãöu kiãûn nhæ (1.4) laì mäüt báút biãún cuía hãû thäúng, (1.7) laì âàûc taí lãûnh laìm chuyãøn (tiãún triãøn) traûng thaïi cuía hãû thäúng. ÅÍ âáy ta sæí duûng caïc biãún coï âaïnh dáúu nhaïy âãø chè traûng thaïi cuía hãû thäúng sau khi chuyãøn âäøi. Ta cuîng noïi mäüt âàûc taí laì cháúp nháûn âæåüc (plausible) nãúu âàûc taí âoï baío toaìn báút biãún cuía hãû thäúng. Nháûn xeït Dãù daìng chæïng minh âënh lyï (1.6) nhæng cuîng dãù daìng bæåïc laûi âënh lyï bàòng caïch xeït phaín vê duû sau : 1 0 1 0 2 0 chg (2, 5) 2 5 3 0 3 0 9 4 0 Roî raìng vê duû trãn thoía maîn caïc âiãöu kiãûn (1.4) vaì (1.5) nhæng khäng thoía maîn (1.4)’ Thæûc ra, lãûnh chg (2, 5) thay âäøi näüi dung âëa chè x (cho giaï trë y) nhæng váùn giæî nguyãn caïc âëa chè khaïc, nghéa laì kêch thæåïc bäü nhåï khäng thay âäøi. IV.2. Haìm Trãn âáy, ta âaî váûn duûng quan âiãøm toaïn hoüc vãö haìm, sau âáy ta tiãúp tuûc laìm roî mäüt säú khaïi niãûm vaì tênh cháút cuía quan âiãøm naìy. Cho hai táûp håüp X vaì Y, biãøu thæïc X → X biãøu diãùn táûp håüp caïc haìm toaìn pháön (total) våïi miãön xaïc âënh (nguäön) laì X vaì miãön trë (âêch) laì Y. Tæång tæû, biãøu thæïc X → Y biãøu diãùn táûp håüp caïc haìm bäü pháûn (partical) tæì nguäön X vaìo âêch Y. Sæû khaïc nhau giæîa chuïng laì åí chäù, mäüt haìm bäü pháûn khäng hoaìn toaìn xaïc âënh cho moüi giaï trë cuía nguäön X. Nãúu f laì mäüt haìm bäü pháûn thç kyï hiãûu dom (f) (domain) laì táûp håüp con cuía X maì f xaïc âënh. Trong træåìng håüp haìm toaìn pháön, miãöm xaïc âënh vaì nguäön laì âäöng nháút. Vê duû haìm q åí muûc trãn laì haìm toaìn pháön våïi nguäön X = {1, 2, 3} vaì âêch Y = {-231, , 231}, ta coï thãø viãút : q ∈ {1, 2, 3} → {-231, , 231} Tuy nhiãn âáy laì mäüt haìm bäü pháûn tæì táûp säú nguyãn Z vaìo chênh noï vç caïc táûp håüp nguäön vaì âêch cuía q âãöu laì táûp håüp con cuía Z. q ∈ Z → Z luïc naìy dom (q) = {1, 2, 3} TS. PHAN HUY KHAÏNH biãn soaûn 131
132 Cäng nghãû Pháön mãöm Ta cuîng coï thãø xáy dæûng táûp håüp con cuía âêch chæïa caïc giaï trë xaïc âënh tæì táûp håüp con cuía nguäön, goüi laì ran (f) (range) Khi mäüt haìm âæåüc âënh nghéa, ta coï thãø liãût kã caïc thaình pháön cuía haìm. Vê duû, ta coï : 1 0 0 2 0 chg (2, 5) 5 3 0 0 tæång æïng våïi hai haìm : q = { 1→ 0, 2 → 0, 3 → 0 } q’ = { 1 → 0, 2 → 5, 3 → 0 } Âãø nhán âæåüc caïc dom vaì caïc ran tæì caïc haìm, ngæåìi ta táûp håüp caïc pháön tæí âàût åí bãn traïi vaì bãn phaíi cuía muîi tãn tæång æïng : dom (q) = {1, 2, 3} dom (q’) = 1, 2, 3} ran (q) = { 0 } ran (q’) = { 0, 5 } Mäüt caïch täøng quan, ta coï kãút quaí sau : dom ({ x → y }) = { x } ran ({ x → y }) = { y } (2.1) f ∈ X → Y keïo theo dom (f) = X Cho haìm f ∈ X → Y vaì mäüt táûp håüp con S ⊆ X, ngæåìi ta kyï hiãûu f \ S laì haìm nhán âæåüc bàòng caïch loaûi khoíi dom (f) caïc pháön tæí cuía S. Âáy laì pheïp haûn chãú tæång æïng våïi âënh nghéa sau : dom (f \ S) = dom (f) - S (f \ S) (x) = f (x) våïi x ∈ dom (f) - S HÇNH VEÎ Ta coï : { 1 → 5, 2 → 8, 3 → 6 } \ { 1, 2} = { 3 → 6 } \ { 1, 2 } = { 3 → 6 } Cho hai haìm coï cuìng nguäön vaì cuìng âêch nhæng coï caïc dom råìi nhau. Kyï hiãûu f ∪ g laì håüp cuía hai haìm theo âënh nghéa sau : dom (f ∪ g) = dom (f) ∪ dom (g) f (x) nãúu x ∈ dom (f) (f ∪ g) (x) = g (x) nãúu x ∈ dom (g) (2.4) Bàòng caïch duìng hai pheïp toaïn trãn âáy, ta coï thãø âënh nghéa sæû chäöng lãn (overload) cuía mätü haìm båíi mäüt haìm khaïc. Ta kyï hiãûu f + g taïc âäüng lãn hai haìm f vaì g coï cuìng nguäön vaì cuìng âêch maì láön naìy, caïc dom khäng nháút thiãút råìi nhau :
Âàûc taí 133 Ta coï : f + g = (f \ dom (g)) ∪ g (2.5) Tæì (2.3) ta coï : (f \ dom (g)) (x) nãúu x ∈ dom (f \ dom (g) (f + g) (x) = g (x) nãúu x ∈ dom (g) (2.6) hay (f + g) (x) = f (x) nãúu x ∈ dom (f) - dom (g) g (x) nãúu x ∈ dom (g) HÇNH VEÎ Vê duû : { 1 → 0, 2 → 0, 3 → 0 } + { 2 → 5 } = ({ 1 → 0, 2 → 0, 3 → 0 } \ { 2 } ∪ { 2 → 0 } = { 1 → 0, 3 → 0 } ∪ { 2 → 5 } = { 1 → 0, 2 → 5, 3 → 0 } Lyï do cå baín âãø âæa vaìo caïc pheïp toaïn \, ∪ vaì + thay vç sæí duûng mäüt caïch hãû thäúng nhæîng âënh nghéa cuía chuïng (2.3), (2.4) vaì (2.7) trong viãûc hçnh thæïc hoïa laì åí chäù tá coï thãø chæïng minh dãù daìng daîy caïc tênh cháút âaûi säú seî sæí duûng vãö sau. Sau âáy laì mäüt säú tênh cháút : (f ∪ g) \ S = (f \ G) ∪ (g \ S) (f + g) \ S = (f \ S) + (g \ S) (f \ S) \ T = f \ (S ∪ T) f ∪ g = g ∪ f (f ∪ g) ∪ h = f ∪ (g ∪ h) dom (f ∪ g) = dom (f) ∪ dom (g) (2.8) ran (f ∪ g) = ran (f) ∪ ran (g) (f + g) + h = f + (g + h) dom (f + g = dom (f) ∪ dom (g) Báy giåì ta coï thãø sæía chæîa âàûc taí âaî nháûn âæåüc åí cuäún muûc træåïc (1.7). Âàûc taí naìy roî raìng âån giaín hån : q chg (x, y) q’ x ∈ A y ∈ V q’ = q + { x → y } Âënh lyï vãö tênh cháúp nháûn âæåüc (plausilility) báy giåì dãù daìng âæåüc chæïng minh båíi pheïp tênh hçnh thæïc âån giaín (simple formal calculus). TS. PHAN HUY KHAÏNH biãn soaûn 133
134 Cäng nghãû Pháön mãöm Theo (2.1) vaì (2.8), ta coï : dom (q’) = dom (q) ∪ { x } ran (q’) ⊂ ran (q) ∪ { y } Nhæng ta coï giaí thiãút (1.4) vf giaí thiãút (2.8) vaì theo (2.2) dom (q) = A vaì { x } ⊂ A ran (q) ⊂ V vaì { y } V Nhæ váûy : dom (q’) = A ran (q’) ⊂ V Tæì âoï theo (2.2) thç q’ ∈ A → V IV.3. Håüp thæïc hoïa vaì phuûc häöi Trong muûc 1, ta âaî âàûc taí caïch hoaût âäüng cuía mäüt bäü nhåï trong âoï, ta coï thãø thay âäøi näüi dung cuía noï. Báy giåì, ta seî tiãúp tuûc phaït triãøn vê duû naìy bàòng caïch âàût ra hai yãu cáöu bäø sung ta muäún ràòng nhæîng thay âäøi trãn bäü nhåï coï âàûc tênh taûm thåìi, nghéa laì ta coï thãø thay âäøi tråí laûi nhåì mäüt pheïp toaïn thêch håüp, màût khaïc ta coï håüp thæïc hoïa (validation) bàòng caïch traí laûi nhæîng thay âäøi træåïc âoï. Ta goüi not (restart) vaì vld (validate) laì nhæîng thao taïc måïi. Nhæîng yãu cáöu bäø sung væìa nãu coï thãø biãøu diãùn hçnh thæïc bàòng caïch kãút håüp caïc âiãöu kiãûn sau âáy : q vld q1 q1 op q2 qn - 1 op qn qn rst q’ Trong âoï op (operations) laì mäüt thao taïc daûng chung (x, y) hay rdm, dáùn âãún âiãöu kiãûn : q’ = q våïi q vaì n báút kyì. Vaí laûi, yãu cáöu vãö tênh “trong suäút” cuía pheïp toaïn håüp thæïc hoïa dáùn âãún âiãöu kiãûn : q’ = q Caïch giaíi quyãút hiãn nhiãn nháút mang tênh yï niãûm laì laìm tàng gáúp âäi bäü nhåï. Nhæ váûy traûng thaïi cuía hãû thäúng báy giåì âæåüc âàûc træng båíi hai biãún p vaì q nhæ sau : p ∈ A → V
Âàûc taí 135 q ∈ A → V (3.1) Bäü nhåï q âoïngvai troì bäü nhåï træåïc âoï, coìn bäü nhåï p duìng âãø khäi phuûc traûng thaïi cuî khi cáön khåíi âäüng laûi. Sau âáy laì âàûc taí cuía 3 thao taïc cho hãû thäúng våïi mod thay thãú chg : (p, q) mod (x, y) ((p’, q’) p’ = p (3.2) q chg (x, y) q’ Ta tháúy thao taïc thay âäøi bäü nhåï xuáút hiãûn nhæ mäüt sæû måí räüng, åí mæïc âàûc taí, cuía pheïp toaïn chg : (p, q) rst (p’, q’) q’ = p q’ = q (3.3) (p, q) vld (p’, q’) p’ = q q’ = q (3.4) Dãù daìng chæïng minh ràòng caí ba pheïp toaïn naìy âãöu cháúp nháûn âæåüc, nghéa laì sau khi thæûc hiãûn chuïng, ta coï (3.1)’. Noïi caïch khaïc, p vaì q âæåüc thay thãú båíi p’ vaì q’ trong (3.1), våïi giaí thiãút ràòng (3.1) âaî âæåüc kiãøm chæïng træåïc khi thæûc hiãûn chuïng. Räút cuäüc, ta phaíi chæïng minh ràòng viãûc kãút håüp caïc âiãöu kiãûn sau âáy : (p, q) vld (p1, q1) (p1, q1) op (p2, q2) (pn - 1, qn - 1) op (pn, qn) (pn, qn) rst (p’, q’) dáùn âãún q’ = q Tháût váûy, theo (3.4), ta coï : p1 = q vaì theo (3.2) vaì (3.4) do op laì mäüt trong hai pheïp toaïn mod (x, y) hoàûc rst, ta coï : pn = p1 Cuäúi cuìng, theo (3.3) :q’ = pn Roî raìng pheïp håüp thæïc hoïa laì trong suäút vç dáùn âãún q’ = q theo (3.4) Sau âáy laì mäüt vê duû vãö caïc pheïp toaïn trãn : TS. PHAN HUY KHAÏNH biãn soaûn 135
136 Cäng nghãû Pháön mãöm q p 1 0 0 2 0 0 3 0 0 mod (1, 1) 1 1 0 2 0 0 3 0 0 mod (2, 2) 1 1 0 2 2 0 3 0 0 mod (1, 3) 1 3 0 2 2 0 3 0 0 vld 1 3 3 2 2 2 3 0 0 mod (3, 1) q q 1 3 3 2 2 2 2 1 0 not 1 3 3 2 2 2 3 0 0 Pháön tiãúp theo seî laìm mën mä hçnh naìy, nghéa laì âæa vaìo caïc biãún traûng thaïi måïi âãø thãø hiãûn caïc raìng buäüc vãö pháön cæïng vaì pháön mãöm.
Âàûc taí 137 IV.4. Bàõt âáöu triãøn khai thæûc tiãùn Vãö màût thæûc tiãùn, coï nhiãöu caïch âãø triãøn khai hãû thäúng âaî âæåüc âàûc taí trong muûc træåïc. Tháût váûy, coï nhiãöu yãúu täú kyî thuáût coï thãø aính hæåíng âãún caïch triãøn khai ; chàóng haûn kêch thæåïc khäng gian V caïc giaï trë âoïng vai troì quan troüng : giaí sæí ràòng caïc pháön tæí cuía táûp håüp A tæång æïng våïi caïc âëa chè cuía caïc trang trong mäüt hãû thäúng coï bäü nhåï phán trang (paging). Trong træåünghåp naìy, mäùi “giaï trë” seî tæång æïng våïi näi dung cuía mäüt traûng thaïi coï kêch thæåïc diãøn hçnh laì 1 bytes. Nãúu nhæîng trang naìy duìng âãø thãø hiãûn mäüt bäü nhåï aío 4 Mbytes, thç ta seî tháúy ràòng coï 4096 trang vaì båíi váyû thåìi gian duìng âãø thæûc hiãûn caïc sao cheïp cáön thiãút cho caïc thao taïc khåíi âäüng vaì håüp thæïc hoïa coï thãø toí ra nàûng nãö. Trong træåìng håüp væìa nãu (ta seî triãøn khai thæûc tiãùn trong muûc naìy), caïch giaíi quyãút laì sæí duûng caïch giaïn tiãúp : hai laìbäü nhåï p vaì q taûo thaình traûng thaïi cuía hãû thäúng âaî xeït trong muûc træåïc, seî âæåüc thay thãú båíi hai baíng (hai haìm) a vaì n (a: ancient, n : new) chæïa caïc con troí tåïi bäü nhåï m. Hãû thäúng måïi seî âæåüc âàûc træng båíi caïc thaình pháön sau : a ∈ A → D n ∈ A → D m ∈ D → V (4.1) Trong âoï D laì táûp håüp caïc âëa chè cuía bäü nhåï m. Sau âáy laì så âäö minh hoüa hãû thäúng måïi naìy : n a m 1 2 2 1 2 2 4 6 2 5 3 5 5 3 5 4 8 5 1 6 4 Trong vê duû trãn, cuîng trong caïc vê duû trãn vãö sau, ta tiãúp tuûc sæí duûng caïc giaï trë V nhæ træåïc. Bàòng caïch kãút håüp caïc baíng a vaì n våïi m, ta nháûn âæåüc caïc baíng p vaì q cuía hãû thäúng cuî : q p 1 5 5 2 8 4 3 1 1 Nhæ váûy, ta coï thãø tháúy ràòng hai hãû thäúng khäng âäüc láûp våïinhau : hai hãû thäúng måïi hiãûn thæûc hoïa hãû thäúng cuî vaì hãû thäúng cuî thãø hiãûn sæû thay âäøi biãún nhæ sau TS. PHAN HUY KHAÏNH biãn soaûn 137
138 Cäng nghãû Pháön mãöm p (x) = m (a (x)) q (x) = m (n (x)) våïi x ∈ A (4.2) Ta coï thãø kiãøm chæïng ngay âæåüc ràòng nhæîng thay âäøi cuía biãún laì coï yï nghéa (roî raìng vç caïc haìm a, n vaì m laì toaìn pháön) vaì chàût cheî våïi báút biãún (3.1) chè roî ràòng p vaì q dãöu thuäüc táûp håüp A → V Pheïp biãún âäøi mod dàûc taí båíi caïc âiãöu kiãûn (3.2) seî âæåüc triãøn khai båíi mäüt pheïp toaïn måïi mod1. Pheïp mod1 seî ghi mäüt giaï trë måïi, mäüt âëa chèmaì khäng thuäüc vaìo miãön trë (range) cuía n cuîng nhæ miãön trë cuía a, noïi caïch khaïc, âëa chè naìy chè phuû thuäüc vaìo táûp håüp : ran (n) ∪ ran (a) hay roî hån, thuäüc táûp håüp D - (ran (n) ∪ ran (0)), táûp håüp âæåüc âàût tãn laì L (Liberty). Nãúu L ≠ ∅, mäüt âiãöu kiãûn træåïc dæåüc âàût ra, thç ta coï thãø choün mäüt âëa chè báút kyì u, våïi âàûc taí sau : (a, n, m) mod1 (x, y) (a’, n’, m’) x ∈ A y ∈ V L ≠ ∅ a’ = a n’ = n + { x → u } m’ = m + { u → y } (4.3) trong âoï L = ran (n) ∪ ran (a) u ∈ L Ta cáön chæïng minh ràòng âàûc taí (4.3) laì cháúp nháûn âæåüc, nghéa laì : ((4.1) vaì (4.3)) keïo theo (4.1)’ (4.4) Mãûnh âãö (4.4) trãn âáy laì hiãøn nhiãn. Tiãúp theo ta cáön chæïng minh pheïp mod1 phuì håüp (âuïng) våïi pheïp mod âaî âàûc taí åí (3.2) nhæ sau : ((4.2), (4.2)’ vaì (4.3)) keïo theo (3.2) (4.5) Mãûnh âãö naìy khäng hiãøn nhiãn, tæång æïng våïi så âäö giao hoaïn dæåïi âáy : HÇNH VEÎ Noïi caïch khaïc, nãúu caïc giaï trë cuía caïc biãún (a, n, m) vaì (a’, n’, m’) thoía maîn âàûc taí (4.3), thç khi tråí vãö caïc biãún cuî (p, q) vaì (p’, q’) (caïc biãún âaî bë thay âäøi tråí thaình caïc biãún (a, n, m) vaì (a’, n’, m’) båíi caïc pheïp biãún âäøi (4.2) vaì 4.2)’) caïc giaï trë cuía caïc biãún (p, q) vaì (p’, q’) thoía maîn âàûc taí (3.2).
Âàûc taí 139 Noïi goün laûi, (4.3) hiãûn thæûc (3.2) Caïc pheïp toaïn måïi khåíi taûo laûi caïc håüp thæïc hoïa mä taí trong caïc âàûc taí sau âáy roî raìng cháúp nháûn âæåüc vaì phuì håüp : (a, n, m) rst1 (a’, n’, m’) a’ = a n’ = n (4.6) m’ = m (a, n, m) vld1 (a’, n’, m’) a’ = n n’ = n (4.7) m’ = m Nhçn vaìo caïc cäng thæïc, ta tháúy âaî khäng cheïp laûi caïc giaï trë nhæng chè coï caïc âëa chè coï thãø coï theo mäüt sæû tiãút kiãûm âaïng kãø vãö thåìi gian nhæng khäng låïn làõm vãö khäng gian nhåï. Giaí thiãút våïi 4096 trang vaì âëa chè cuía D laì 2 bytes, mäùi baíng a vaì n seî chiãún 8 Kbytes. Hãû thäúng måïi hoaût âäüng qua vê duû sau : n a m 1 1 1 1 0 2 2 2 2 0 3 3 3 3 0 4 0 5 0 6 0 mod1 (1, 1) 1 4 1 1 0 L = { 4, 5, 6 } 2 2 2 2 0 u = 4 ∈ L 3 3 3 3 0 (choün u = min (L)) 4 1 5 0 6 0 TS. PHAN HUY KHAÏNH biãn soaûn 139
140 Cäng nghãû Pháön mãöm IV.5. Pheïp håüp thaình (cáúu taûo) ÅÍ muûc træåïc, ta âaî sæí duûng mäüt caïch phi hçnh thæïc pheïp håüp thaình (composition opertion) cuía p vaì q theo a, m vaì n. Trong muûc naìy, ta tiãúp tuûc âënh nghéa pheïp håüp thaình mäüt caïch chàût cheî hån. Pheïp håüp thaình, kyï hiãûu laì 0, taïc âäüng lãn hai toaïn haûng laì hai haìm, chàóng f vaì g, thuäüc vãö caïc táûp håüp X → Y vaì Y → Z tæång æïng, sao cho haìm fog thuäüc vãö táûp X → Z Pheïp håüp thaình coï thãø âæåüc âënh nghéanhæ sau : dom (fog) = { x ∈ dom (g) / g (x) ∈ dom (f) } (fog) (x) = f (g (x)) våïi x ∈ dom (fog) (5.1) Vê duû : { 2 → 6, 5 → 8 }o { 1 → 2, 4 → 3, 7 → 5 } = { 1 → 6, 7 → 8 } Tæì âënh nghéa trãn coï thãø suy ra ngay ràòng nãúu caïc haìm f vaì g âãöu toaìn pháön (noïi caïch khaïc, nãúu dom (g) = X vaì dom (f) = Y), thç haìm fog cuîng laì toaìn pháön. Mäüt caïch täøng quan hån, nãúu miãön trë cuía g nàòm trong miãön xaïc âënh.cuía f thç hai haìm g vaì fog coï cuìng miãön xaïc âënh. Ta coï thãø dãù daìng xáy dæûng mäüt säú luáût kiãøu âaûi säú âãø näúi liãön pheïp håüp thaình våïi caïc pheïp häüi vaì haûn chãú âaî xeït åí muûc 2. Sau âáy laì mäüt säú luáût nhæ váûy : (f ∪ g) o h= (f o h) ∪ (g o h) f o (g ∪ h) = (fog) ∪ (f o h) (5.2) S ∩ rang (g) = ∅ keïo theo (f \ s) og = fog (5.3) dom (f) ∩ ran (g) = ∅ keïo theo fog = { } (5.4) Biãøu thæïc { } chè âënh haìm räùng f o (g \ S) = (fog) \ S (5.5) { x → y } o { x → u } = { x → y } (5.6) Tæì caïc luáût trãn, ta coï thãø âån giaín hoïa pheïp thay âäøi biãún âaî âënh nghéa åí (4.2) nhæ sau : p = m o a q = m o n (5.7) Vaì ta coï thãø chæïng minh dãù daìng âënh lyï phuì håüp (4.5) bàòng caïch sæí duûng caïc tênh cháút trãn. Tháût váûy, ta cáön chæïng minh hai âàóng thæïc sau âáy : m’ o n’ = (m o n) + { x → y } m’ o o’ = m o a Nghéa laì : (m + { u → y }) o (n + { x → u }) = (m o n) + { x → y }
Âàûc taí 141 (m + { u → y }) o a = m o a våïi caïc giaí thiãút : u ∉ ran (n) nghéa laì { u } ∩ ran (n) = ∅ (5.8) u ∉ ran (a) nghéa laì { u } ∩ ran (a) = ∅ (5.9) Ta coï kãút quaí phuû nhæ sau : (m \ { u }) o (n \ { x }) = (( m \ { u }) o n) \ { x } theo (5.5) = (m o n) \ { x } theo (5.3) vaì (5.8). Nhæng : { x → y } o (n \ { x }} = { } theo (5.4), (2.2) vaì (5.8). Vaì ta cuîng coï : (m \ { u }) o { x → u } = { } theo (5.4) vaì (2.2) { u → y } o { x → u } = { x → y } theo (5.6) Nhæ váûy theo (5.2) vaì (2.5) : (m + { u → y }) o (m + { x → u}) = (m o n) \ { x } ∪ { x → y } = (m o n) + { x → y } Màût khaïc ta coï : m \ { u } o a = m o a theo (5.3) { u → y } o a = { } theo (5.4) Nhæ váûy : (m + { u → y }) o a = m o a theo (2.4) vaì (5.3) IV.6. Triãøn khai thæï hai Muûc naìy seî täúi æu caïch triãøn khai âáöu tiãn âaî trçnh baìy trong muûc 4 bàòng caïch xáy dæûng táûp håüp L caïc âëa chè tæû do cuía D, táûp håüp maì ta âaî choün tuìy yï mäüt pháön tæí u trong âàûc taí pheïp toaïn mod1 åí (4.3). YÏ tæåíng thiãút kãú caïch triãøn khai thæï hai naìy nàòm åí chäø giæî laûi traûng thaïi cuía mäùi âëa chè cuía D maì âëa chè naìy coï thãø thuäüc vãö mäüt (vaì chè mäüt maì thäi) trong 4 táûp håüp råìi nhau nhæ sau : RN _ RN RA ∩ RN RN _ RA RA ∪ RN = L trong âoï RA = ran (a), RN = ran (n) TS. PHAN HUY KHAÏNH biãn soaûn 141
142 Cäng nghãû Pháön mãöm Tuìy theo mäüt âëa chè d cuía D thuäüc vãö mäüt trong bäún táûp håüp trãn, ta noïi traûng thaïi tæång æïng seî laì : old (cuî) d ∈ ran (a) common (chung) d ∈ ran (a) vaì d ∈ ran (n) new (måïi) d ∈ ran (a) free (tæû do) d ∉ ran (a) vaì d ∉ ran (n) Khi mäüt âëa chè tæû do âæåüc choün, khi mäüt thay âäøi xaíy ra, âëa chè âoï chuyãøn qua traûng thaïi måïi ; vãö âëa chè quaï taíi trong baíng n, nãúu âëa chè âoï khäng phán chia bãn trong baíng n (nghéa laì nãúu haìm nlaì âån aïnh vaì âiãöu naìy âæåüc giaí thiãút laì luän âuïng), khi âoï, âëa chè seî tråí nãn tæû do nãúu âaûng åí traûng thaïi måïi hoàûc chuyãøn sang traûng thaïi cuî nãúu âang åí traûng thaïi chung. Khi mäüt pheïp håüp thæïc hoïa hay khåíi âäüng laûi caïc âëa chè tæû do hay chung váùn nhæ cuî. Caïc âëa chè måïi chuyãøn thaình tæû do khi mäüt sæû khåíi âäüng laûi vaì laì træåìng håüp chung khi håüp thæïc hoïa. Cuäúi cuìng, caïc âëa chè cuî chuyãøn thaình tæû do khi håüp thæïc hoïa vaì tråí thaình chung khi khåíi âäüng laûi.Chuï yï ràòng caïc âëa chè cuî khäng liãn quan âãún sæû thay âäøi. Så âäö dæåïi âáy toïm tàõt mäüt caïch phi hçnh thæïc nhæîng chuyãøn âäøi khaïc nhau naìy. Muûc âêch âãø hçnh thæïc hoïa phæång phaïp naìy, ta âæa vaìo mäüt biãún måïi s âënh nghéa traûng thaïi cuía mäùi âëa chè cuía D. s ∈ D → {fr, nw, cm, ol} (6.1) Ta coï báút biãún sau âáy : RA - RN = adr (ol) RA ∩ RN = adr (cm) (6.2) RN - RA = adr (nw) RA ∪ RN = adr (fr) HÇNH VEÎ Trong âoï : RA = ran (a) RN = ran (n) adr (z) = {x ∈ D / s (x) = Z} våïi Z ∈ {fr, nw, cm, ol} Cuäúi cuìng báút biãún thæï ba chè roî ràòng caí hai haìm n vaì a âãöu âån aïnh, nghéa laì hai âëa chè cuía A phán biãût seî luän luän tæång æïng våïi caïc âëa chè cuía D phán biãût qua caïc haìm naìy. Táûp håüp caïc haìm tæì A vaìo D nhæ váûy âæåüc kyï hiãûu båíi A ⌡ D nhæ váûy
Âàûc taí 143 n ∈ A ⌡ D a ∈ A ⌡ D Báy giåì seî laì âënh nghéa ba haìm chuyãøn tiãúp láön læåüt laì f, g vaì h sæí duûng khi thay âäøi (cho caïc âëa chè cuía D liãn quan), khåíi âäüng laûi thay cho håüp thæïc hoïa (cho moüi âëa chè cuía D) : f = {fr → nw, nw → fr, thay âäøi cm → ol} g = {fr → fr, nw → fr, cm → cm, khåíi âäüng laûi ol → cm} h = {fr → fr, nw → cm, cm → cm, håüp thæïc hoïa ol → fr} Ta coï âàûc taí cuía 3 pheïp toaïn måïi mod2, rst2, vaì vld2 xuáút hiãûn nhæ laì caïc måí räüng tæång æïng tæì muûc 4 : (a, n, m, s) mod2 (x, y) (a’, n’, m’, s’) (a, n, m) mod1 (x, y) (a’, n’, m’) (6.5) s’ = s + {u → f (s (u)), v → f (s) (v))} xem (4.3) trong âoï : L = { Z ∈ D |s (z) = fr } u ∈ L v = n (x) (a, n, m, s) rst2 (a’, n’, m’, s’) (6.6) s’ = gos xem (4.6) (a, n, m, s) vld2 (a’, n’, m’, s’) (6.7) (a, n, m) vld1 (a’, n’, m’) xem (4.7) s’ = hos Sau âáy laì mäüt quaï trçnh chuyãøn âäøi cuía hãû thäúng CHÆÌA Chæïng minh TS. PHAN HUY KHAÏNH biãn soaûn 143
144 Cäng nghãû Pháön mãöm Màûc duì trong muûc træåïc ta âaî kiãøm chæïng kyî læåîng âàûc taí hãû thäúng vaì nháûn âæåüc kãút quaí thoîa maîn, nhæng chæa âaím baío âæåüc tênh âuïng âàõn cuía âàûc taí trong moüi træåìng håüp. Âãø âi âãún mäüt kãút quaí täøng quaït, ta cáön phaíi chæïng minh khäng phaíi cho mäüt træåìng håüp âàûc biãût naìo âoï maì phaíi cho caïc dæî liãûu tæåüng træng thoía maîn nhæîng giaí thiãút naìo âoï, caïc pheïp toaïn âaî âàûc taí laì phuì håüp vaì cháúp nháûn âæåüc. Viãûc chæïng minh tênh phuì håüp cuía caïc pheïp toaïn âàûc taí åí (6.5), (6.6) vaì (6.7) so våïi caïc pheïp toaïn âàûc taí åí (4.3), (4.6) vaì (4.7) laì hiãøn nhiãn vç ràòng trong caïch láûp caïc cäng thæïc thç caïc pheïp toaïn (4.3), (4.6) vaì (4.7) mäüt caïch tæång æïng. Traïi laûi, viãûc chæïng minh tênh cháúp nháûn âæåüc phæïc taûp hån. Træåïc hãút ta cáön chæïng minh ba nhoïm âënh lyï báút biãún sau âáy : ((6.1) vaì (6.5)) keïo theo (6.1)’ (7.1) ((6.2) vaì (6.5)) keïo theo (6.2)’ (7.2) ((6.3) vaì (6.5)) keïo theo (6.3)’ (7.3) ((6.1) vaì (6.6)) keïo theo (6.1)’ (7.4) ((6.2) vaì (6.6)) keïo theo (6.2)’ (7.5) ((6.3) vaì (6.6)) keïo theo (6.3)’ (7.6) ((6.1) vaì (6.7)) keïo theo (6.1)’ (7.7) ((6.2) vaì (6.7)) keïo theo (6.2)’ (7.8) ((6.3) vaì (6.7)) keïo theo (6.3)’ (7.9) Âäúi våïi 3 âënh lyï åí nhoïm 1, ta coï thãø dáùn âãún caïc giaí thiãút cho caïc âiãöu kiãûn sau âáy : a ∈ A ⌡ D n ∈ A ⌡ D u ∉ RN (7.10) u ∉ RA v ∈ RN Trong âoï u vaì âæåüc âënh nghéa åí (6.5) vaì RA, RN âæåüc âënh nghéa åí (6.2) chæïng minh (7.1)
Âàûc taí 145 Mäüt khoï khàn nhoí laì haìm chuyãøn tiãúp f âæåüc âënh nghéa åí (6.4) laì haìm bäü pháûn. Cáön chæïng minh ràòng s’ âæåüc âënh nghéa âuïng, nghéa laì caïc biãøu thæïc f (s (u)) vaì f (s (v)) trong (6.5) coï nghéa, noïi caïch khaïc ta coï : s (u) ∈ dom (f) s (v) ∈ dom (f) âiãöu naìy hiãøn nhiãn vç ràòng theo (7.10), ta coï : s (u) = fr s (v) = { nw, cm} vaì theo (6.4) ta coï dom (f) = {fr, nw, cm} Âãø chæïng minh (7.2) vaì (7.3) ta cáön kãút quaí sau âáy liãn quan âãún sæû quaï taíi cuía mäüt haìm âån aïnh thæìa nháûn maì khäng chæïng minh : f ∈ X ⌡ Y keïo theo f’ ∈ X ⌡ Y x ∈ dom (f) ran (f’) = r’ y ∉ Y - ran (f) y ≠ f (x) Trong âoï : f’ = f + {x → y} r’ = (ran (f) - {f (x)}) ∪ {y} chæïng minh (7.2) : Theo (7.10), (7.11) vaì (6.5) ta coï RA’ = RA (vç ràòng a’ = a theo (4.3)) RN’ = (RN {V}) ∪ {u} theo 7.11 u ≠ v theo 7.10 HÇNH VEÎ Xaíy ra hai træåìng håüp : 1/ v ∈ RA, nghéa laì s (v) = cm Khi âoï : RA’ - RN’ = (RA - RN) ∪ {v} RA’ ∩ RN’ = (RA ∩ RN) - {v} RN’ - RA’ = (RN - RA) ∪ {u} RA’ ∪ RN’ = (RA ∪ RN) - {u} HÇNH VEÎ 2/ v ∉ RA, nghéa laì s (v) = nw Khi âoï : RA’ - RN’ = RA - RN TS. PHAN HUY KHAÏNH biãn soaûn 145
146 Cäng nghãû Pháön mãöm RA’ ∩ RN’ = RA ∩ RN RN’ - RA’ = ((RN - RA) - {v}) ∪ {v} RN’ ∪ RA’ = ((RN ∪ RA) - {u} ∪ {v} HÇNH VEÎ Nhæ váûy caïc chuyãøn tiãúp tæì s (u) vaì s (v) nhæ sau fr → nw våïi u cm → ol våïi v trong træåìng håüp 1/ nw → fr våïi v trong træåìng håüp 2/ Caïc chuyãøn tiãúp naìy tæång æïng våïi caïc chuyãøn tiãúp âaî chè ra båíi haìm g âënh nghéa åí (6.4) IV.7. Triãøn khai thæûc hiãûn láön thæï ba Láön naìy, ta giaí thiãút ràòng xaíy ra caïc sai soït cáön phaíi dæû phoìng nhåì hãû thäúng håüp thæïc hoïa vaì khåíi âäüng laûi. Giaí sæí caïc baíng a, n, m vaì s âæåüc caìi âàût trãn caïc thiãút bë nhåï khaïc nhæ sau : HÇNH VEÎ Tæì caïch täø chæïc naìy, ta muäún dæû phoìng caïc sai soït taïc âäüng lãn bäü nhåï trong bàòng caïch khåíi âäüng laûi tæì âéa. ÅÍ âáy, ta âaî caìi âàût caïc baíng s vaì s trong bäü nhåï trong våïi muûc âêch tàng tênh hiãûu quaí cuía pheïp thay âäøi bäü nhåï laì nhanh nháút coï thãø. Våïi muûc âêch trãn, viãûc khåíi âäüng laûi laìm thay âäøi baíng s tæì chênh noï (thæûc tãú laì s’ = gos theo (6.6)) khäng coìn coï taïc duûng næîa vç ràòng ta giaí thiãút ràòng bäü nhoï trung tám laì s seî khäng coìn næîa. Mäüt giaíi phaïp laì gáúp âäi baíng s lãn âéa cho mäùi láön håüp thæïc hoïa. Xáy dæûng baíng måïi t âæåüc tæång æïng våïi báút biãún nhæ sau : t ∈ D → {fr, cm} (8.1) Chuï yï ràòng ta khäng cáön moüi giaï trë caïc traûng thaïi âëa chè âéa vç ràòng t chè duìng âãø taïi sinh laûi baíng s khi khåíi âäüng laûi, tæì âoï ta coï báút biãún bäø sung nhæ sau : {x ∈ D | t (x) = cm} = ran (a) (8.2) Ta coï caïc âàûc taí måïi nhæ sau : (a, n, m, s, t) mod3 (x, y) (a’, n’, m’, s’, t’) (a, n, m, s) mod2 (x, y) (a’, n’, m’, s’) (8.3) t’ = t xem (6.5) (a, n, m, s, t) rst3 (a’, n’, m’, s’, t’) (a, n, m) rst1 (a’, n’, m’) (8.4) s’ = t xem (4.6)
Âàûc taí 147 t’ = t (a, n, m, s, t) vld3 (a’, n’, m’, s’, t’) (8.5) (a, n, m, s) vld2 (a’, n’, m’, s’) xem (6.7) t’ = s’ Dãù daìng chæïng minh ràòng caí ba âàûc taí trãn laì phuì håüp vaì cháúp nháûn âæåüc. Màût khaïc ta tháúy ràòng pheïp khåíi âäüng laûi taïi sinh bäü nhåï trong tæì âéa vaì chè tæì âéa maì thäi. Triãøn khai láön thæï tæ vaì láön thæï nàm Ta seî maî hoïa caïc giaï trë fr, nw, cm vaì ol nhæ haìm âån aïnh k nhæ sau : k = {(0, 0) → fr, (0, 1) → ol, (1, 0) → cm, (9.1) (1, 1) → nw} Sau âoï ta biãøu diãùn caïc haìm s vaì t nhåì ba chuäùi bit nhæ sau : b ∈ D → {0, 1} âãø biãøu diãùn s c ∈ D → {0, 1} d → {0, 1}âãø biãøu diãùn t (9.2) Cuäúi cuìng, thay âäøi caïc biãún tæång æïng våïi caïc âiãöu kiãnû sau : s (x) = k (b (x), c (x)) t (x) = k (d (x), 0) våïi x ∈ D (9.3) Giaí sæí laì pheïp buì (âaío ngæåüc bêt) nhæ sau 0 = 1,1 = 0 (9.4) Ta tháúy coï thãø maî hoïa haìm f âaî âënh nghéa åí (6.4) nhåì hai pheïp buì vaì haìm h cuîng âaî dënh nghéa åí (6.4) nhåì pheïp sao cheïp vaì âàût lãö 0 tæång æïng våïi haìm : Z ∈ D → {0} (9.5) Ta coï 3 âàûc taí måïi nhæ sau : (a, n, m, b, c, d) mod4 (x, y) (a’, n’, m’, b’, c’, d’) (a, n, m) vld1 (a’, n’,m’) b’ = b (9.8) c’ = z xem (4.7) d’ = b Báy giåì ta chè cáön toïm tàõt laûi nhæîng gç âaî laìm cho âãún luïc naìy, nghéa laì mäüt màût, sao cheïp laûi caïc âàûc taí (4.3), (4.6) vaì (4.7) vaìo bãn trong cuía (9.6), (9.7) vaì (9.8), màût khaïc, nhoïm caïc báút biãún (4.1), (6.1), (6.2), (6.3), (8.1), (8.2) vaì (9.2) Âiãöu naìy laìm âæåüc bàòng caïch khæí caïc biãún tråí thaình dæ thæìa (chæïa s vaì t) båíi caïc pheïp thay âäøi biãún (9.3). TS. PHAN HUY KHAÏNH biãn soaûn 147