關(guān)系代數(shù)→關(guān)系演算轉(zhuǎn)換系統(tǒng)的研制.pdf

1、在程序驗(yàn)證領(lǐng)域，Hoare公理方法與Dijkstra最弱前置謂詞方法是最為杰出的，這兩個(gè)方法系統(tǒng)的基點(diǎn)是各自定義的語(yǔ)言系統(tǒng)，然后根據(jù)各自的方法尋求語(yǔ)言系統(tǒng)的語(yǔ)義。在研究軟件形式化時(shí)，我們發(fā)現(xiàn)這樣的問題：怎么探尋數(shù)據(jù)庫(kù)程序中關(guān)系代數(shù)語(yǔ)句的語(yǔ)義，這里數(shù)據(jù)庫(kù)程序即是用具備關(guān)系操作的程序設(shè)計(jì)語(yǔ)言編寫的包含關(guān)系操作的程序。
　　 無(wú)論是Hoare公理方法或是Dijkstra最弱前置謂詞方法，各自定義的語(yǔ)言系統(tǒng)都沒有觸及數(shù)據(jù)庫(kù)領(lǐng)域。PAR方

2、法中的Apla語(yǔ)言的特色之一是把關(guān)系代數(shù)操作納入程序設(shè)計(jì)語(yǔ)言中，這使得Apla可以直接用于數(shù)據(jù)庫(kù)程序的開發(fā)。當(dāng)今現(xiàn)實(shí)是，程序不可避免地要與數(shù)據(jù)庫(kù)打交道，所以，對(duì)這部分程序的驗(yàn)證急需理論上的擴(kuò)展、突破。
　　 經(jīng)過(guò)長(zhǎng)久深入的研究，本文發(fā)現(xiàn)驗(yàn)證數(shù)據(jù)庫(kù)程序的核心就是找到數(shù)據(jù)庫(kù)中關(guān)系代數(shù)的語(yǔ)義，進(jìn)一步，也就是把關(guān)系代數(shù)轉(zhuǎn)換成等價(jià)的關(guān)系演算。
　　 本文主要研究了關(guān)系代數(shù)到關(guān)系演算的轉(zhuǎn)換規(guī)則，并對(duì)傳統(tǒng)轉(zhuǎn)換規(guī)則進(jìn)行了簡(jiǎn)化、擴(kuò)展。針對(duì)