資源描述：
《關(guān)系代數(shù)→關(guān)系演算轉(zhuǎn)換系統(tǒng)的研制》由會(huì)員上傳分享，免費(fèi)在線閱讀，更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫。
1、‘’；}；27j·逸／聲明本人聲明所呈交的學(xué)位論文是本人在導(dǎo)師指導(dǎo)下進(jìn)行的研究工作及取得的研究成果。據(jù)我所知，除了文中特別加以標(biāo)注和致謝的地方外，論文中不包含其他人已經(jīng)發(fā)表或撰寫過的研究成果，也不包含為獲得或其他教育機(jī)構(gòu)的學(xué)位或證書而使用過的材料。與我一同工作的同志對(duì)本研究所做的任何貢獻(xiàn)均已在論文中作了明確的說明并表示謝意。學(xué)位論文作者簽名：蘇月擘簽字日期：弘產(chǎn)年彭月／，乙日學(xué)位論文版權(quán)使用授權(quán)書本學(xué)位論文作者完全了解江西師范大學(xué)研究生院有關(guān)保留、使用學(xué)位論文的規(guī)定，有權(quán)保留并向國家有關(guān)部門或機(jī)構(gòu)送交論文的復(fù)印件和電子稿，允許論文被查閱和借閱。本人授權(quán)江西師范大學(xué)研究生院可以將學(xué)位論文
2、的全部或部分內(nèi)容編入有關(guān)數(shù)據(jù)庫進(jìn)行檢索，可以采用影印、縮印或掃描等復(fù)制手段保存、匯編學(xué)位論文o(保密的學(xué)位論文在解密后適用本授權(quán)書)學(xué)位論文作者簽名：芳戽盈簽字日期：矽／o年6月／，1眉蠢名：1銻主簽字日期：。知如年6月f擁．囊鼙瀑，；；菱氣吐鼉≯羈0要，藩．．1∥0；●。?；卜；。。．．。喜毒oq毒0蠆嚳罐薯鼉q飛墨遵_a京毒；?！?■o_●■■一◆●摘要㈣蝴．
3、1i
4、lnull幽．IIIII㈣IIIIIIIIIIII舢IIY18380。1”1。在程序驗(yàn)證領(lǐng)域，Hoare公理方法與Dijkstra最弱前置謂詞方法是最為杰出的，這兩個(gè)方法系統(tǒng)的基點(diǎn)是各自定義的語言系統(tǒng)，然后根據(jù)各自
5、的方法尋求語言系統(tǒng)的語義。在研究軟件形式化時(shí)，我們發(fā)現(xiàn)這樣的問題：怎么探尋數(shù)據(jù)庫程序中關(guān)系代數(shù)語句的語義，這里數(shù)據(jù)庫程序即是用具備關(guān)系操作的程序設(shè)計(jì)語言編寫的包含關(guān)系操作的程序。無論是Hoare公理方法或是Dijkstra最弱前置謂詞方法，各自定義的語言系統(tǒng)都沒有觸及數(shù)據(jù)庫領(lǐng)域。PAR方法中的Apla語言的特色之一是把關(guān)系代數(shù)操作納入程序設(shè)計(jì)語言中，這使得Apla可以直接用于數(shù)據(jù)庫程序的開發(fā)。當(dāng)今現(xiàn)實(shí)是，程序不可避免地要與數(shù)據(jù)庫打交道，所以，對(duì)這部分程序的驗(yàn)證急需理論上的擴(kuò)展、突破。經(jīng)過長久深入的研究，本文發(fā)現(xiàn)驗(yàn)證數(shù)據(jù)庫程序的核心就是找到數(shù)據(jù)庫中關(guān)系代數(shù)的語義，進(jìn)一步，也就是把關(guān)系代數(shù)
6、轉(zhuǎn)換成等價(jià)的關(guān)系演算。本文主要研究了關(guān)系代數(shù)到關(guān)系演算的轉(zhuǎn)換規(guī)則，并對(duì)傳統(tǒng)轉(zhuǎn)換規(guī)則進(jìn)行了簡化、擴(kuò)展。針對(duì)關(guān)系代數(shù)到關(guān)系演算的轉(zhuǎn)換規(guī)則，本文主要解決兩重運(yùn)算的轉(zhuǎn)換，我們發(fā)現(xiàn)更多重的運(yùn)算轉(zhuǎn)換規(guī)則定義起來十分復(fù)雜，況且多重的運(yùn)算完全可以由單重的或兩重的運(yùn)算多步來實(shí)現(xiàn)。本文開發(fā)出轉(zhuǎn)換系統(tǒng)后臺(tái)算法模塊，并制作成DLL構(gòu)件形式。然后把DLL構(gòu)件與開發(fā)出的系統(tǒng)GUI組裝成完整的轉(zhuǎn)換系統(tǒng)。轉(zhuǎn)換系統(tǒng)能夠自動(dòng)生成與給定關(guān)系代數(shù)等價(jià)的關(guān)系演算結(jié)果，這樣就使得程序驗(yàn)證拓展到數(shù)據(jù)庫領(lǐng)域，提供一種可能。關(guān)鍵字：關(guān)系演算，關(guān)系代數(shù)，轉(zhuǎn)換規(guī)則，程序語義，PAR方法，核心算法，DLL構(gòu)件，構(gòu)件組裝■o，￡¨‰若爨rf。
7、群●；i，．i}拈#?{，p，“，r#．、4，謄，●■AbstractInthefieldofprogramverification，HoareaxiomaticmethodandtheDijkstraweakestpre—verbisthemostoutstandingofthesetwomethodsistheirpointsystem，thedefinitionofthelanguagesystem，andthenfindtheirwaytothesemanticsofthelanguagesystem．Formalresearchsoftware，wefoundthisprob
8、lem：howtoexplorethedatabaseprogram,thesemanticsofrelationalalgebrastatements，wherethedatabaseprogramthatisoperatedwitllrelationswriaeninprogramminglanguagesincludingrelationaloperationsprocedures．BothHoareaxiomaticmethodorDijkstraweakestpre—predicatemethod，eachdefinedlanguagesystemdidnottouchthe
9、databaseinthefield．PARmethodofAplaoneofthecharacteristicsoflanguageistorelationalalgebraoperationsintoprogramminglanguages，whichmakesApladatabaseprogramCanbedirectlyusedforthedevelopment．Todaytherealityis，theprogramwillinevi
