框架時(shí)序邏輯程序語言MSVL的形式語義.pdf

1、形式語義是對(duì)軟件系統(tǒng)進(jìn)行形式化驗(yàn)證和分析的重要理論基礎(chǔ)。程序語言的語義可以幫助人們更好的理解、執(zhí)行、分析軟件系統(tǒng)。操作語義有助于語言的實(shí)現(xiàn)，公理語義有利于程序的驗(yàn)證，指稱語義在強(qiáng)大的數(shù)學(xué)理論支持下為程序的含義提供了精確的數(shù)學(xué)描述。 時(shí)序邏輯程序設(shè)計(jì)是一種新型的程序設(shè)計(jì)范式，程序的具體執(zhí)行和性質(zhì)的描述可以在同一邏輯框架內(nèi)表示，適用于并發(fā)系統(tǒng)的建模、模擬和驗(yàn)證。盡管研究人員開發(fā)了相關(guān)的解釋器來執(zhí)行各類時(shí)序邏輯程序語言，時(shí)序邏輯及其可

2、執(zhí)行子集被廣泛地應(yīng)用于系統(tǒng)的規(guī)范和驗(yàn)證中，但是到目前為止，至少在區(qū)間時(shí)序邏輯程序語言中，還沒有一套系統(tǒng)而完整的形式語義。本文以區(qū)間時(shí)序邏輯程序語言MSVL為研究對(duì)象，分別從模型語義、操作語義、公理語義三條主線來研究區(qū)間時(shí)序邏輯程序的形式語義，并對(duì)三種語義之間的一致性、互補(bǔ)性進(jìn)行分析和證明。 本文研究了MSVL語言的極小模型語義。由于MSVL語言中的框架技術(shù)破壞了邏輯的單調(diào)性，傳統(tǒng)的規(guī)范模型已不再適用于捕獲該語言的模型語義。因此，

3、我們提出了極小模型理論并證明了極小模型的存在性定理。 為了正確理解程序語言的執(zhí)行過程，本文研究了MSVL語言的結(jié)構(gòu)化操作語義。首先定義了一種新的適用于描述區(qū)間時(shí)序邏輯程序語言語義的表達(dá)式格局和命令格局。其次給出了帶有時(shí)態(tài)操作符的算術(shù)表達(dá)式和布爾表達(dá)式的求值規(guī)則，以及程序的狀態(tài)遷移系統(tǒng)和區(qū)間遷移系統(tǒng)。狀態(tài)遷移系統(tǒng)包括將一個(gè)程序化簡為與其等價(jià)的正則形的語義等價(jià)規(guī)則和狀態(tài)上的遷移規(guī)則。區(qū)間遷移系統(tǒng)給出了將程序從一個(gè)狀態(tài)遷移到下一個(gè)狀態(tài)

4、的區(qū)間遷移規(guī)則。進(jìn)一步，我們研究了兩類遷移系統(tǒng)的性質(zhì)，并證明了操作語義和基于模型理論的極小模型語義之間的一致性。最后基于本文提出的操作語義，開發(fā)了具有對(duì)軟硬件系統(tǒng)進(jìn)行建模、模擬和驗(yàn)證功能的MSVL語言的解釋器。 為了實(shí)現(xiàn)在同一邏輯框架內(nèi)對(duì)并發(fā)系統(tǒng)進(jìn)行建模和驗(yàn)證的目的，本文研究了MSVL語言的公理語義。在該方法中，MSVL語言作為程序設(shè)計(jì)語言來描述系統(tǒng)行為（系統(tǒng)建模），命題投影時(shí)序邏輯作為斷言語言描述系統(tǒng)性質(zhì)。這樣，系統(tǒng)的模型和性