Java語(yǔ)言的類(lèi)和多態(tài)性的公理語(yǔ)義.pdf

1、大連理工大學(xué)碩士學(xué)位論文摘要本文以Java語(yǔ)言為背景，重點(diǎn)詞論了類(lèi)的繼承和多態(tài)性的公理語(yǔ)義，同時(shí)也給出了必、要的及相關(guān)的語(yǔ)言成分的公理語(yǔ)義。主要工作包括:(1)給出了類(lèi)的公理語(yǔ)義，包括類(lèi)的聲明、類(lèi)的靜態(tài)方法、構(gòu)造函數(shù)的公理語(yǔ)義以及類(lèi)的數(shù)據(jù)成員訪問(wèn)表tA的公理語(yǔ)義。(2)給出了與對(duì)象相關(guān)的公理語(yǔ)義，包括對(duì)象的創(chuàng)建，實(shí)例方法調(diào)用的公理語(yǔ)義。(3)數(shù)組也是對(duì)象，我們給出了與數(shù)組相關(guān)的公理語(yǔ)義，包括數(shù)組實(shí)例創(chuàng)建表達(dá)式和數(shù)組訪問(wèn)表達(dá)式的公理語(yǔ)義。

2、(4)因?yàn)轭?lèi)的繼承和多態(tài)性是面向?qū)ο蟪绦蛟O(shè)計(jì)語(yǔ)言的一種機(jī)制，而非一種語(yǔ)言成分，故以不同于L述三類(lèi)語(yǔ)言成分的方式描述它們的公理語(yǔ)義。隨著程序設(shè)計(jì)的研究與發(fā)展，程序的正確性、可靠性、可維護(hù)性等問(wèn)題受到川門(mén)的普遍關(guān)注。許多程序規(guī)范與驗(yàn)證的形式化方法涌現(xiàn)出來(lái)，對(duì)程序tki十方法學(xué)的發(fā)展起了flft的推動(dòng)作用。但是盡管面向?qū)ο蟮姆椒ㄔ诮裉斓能浖_(kāi)發(fā)中得到廣泛應(yīng)用并取得顯著的成就，這個(gè)領(lǐng)域的形式化正確證明方法仍然是一個(gè)難以解決的問(wèn)題。在正確性證明中

3、最廣泛應(yīng)用的方法是Hoare方法，它利用推導(dǎo)公式來(lái)描述程序或程序片斷的輸人輸出關(guān)系。對(duì)象不變式描述了面向?qū)ο髷?shù)據(jù)結(jié)構(gòu)中元素間的關(guān)系，在對(duì)象創(chuàng)建后以及方法引用前后它總為真。對(duì)象不變式在面向?qū)ο蟪绦虻淖C明中具有重要作用。利用對(duì)象不變式，類(lèi)不變式，靜態(tài)澎熊成員的狀態(tài)和實(shí)例數(shù)據(jù)成員的狀態(tài)，并結(jié)合Hoare公理系統(tǒng)，我們明確給出了類(lèi)的公理語(yǔ)義。多態(tài)性是面向?qū)ο蟪绦蛟O(shè)計(jì)的一一個(gè)重要特點(diǎn)，也勻佳點(diǎn)，在使用時(shí)最容易發(fā)生錯(cuò)誤和誤解。在用公理語(yǔ)義描述多態(tài)性

4、的時(shí)候，由于我們使用的描述方法是靜態(tài)的，而被描述對(duì)象是動(dòng)態(tài)的，所以在描述多態(tài)性的時(shí)候需要做大量工作。本文通過(guò)引人新的謂詞和函數(shù)確定了用公理語(yǔ)義描述多態(tài)性的前置條件和后置條件，從而描述了多態(tài)性的公理語(yǔ)義。利用我們給出的公理語(yǔ)義可以用于編譯、解釋Java程序的生成驗(yàn)證用Java語(yǔ)言編寫(xiě)的程序的正確性。關(guān)鍵詞:對(duì)象不變式公理語(yǔ)義程序驗(yàn)證獨(dú)創(chuàng)性說(shuō)明作者鄭重聲明:本碩士學(xué)位論文是我個(gè)人在導(dǎo)師指導(dǎo)下進(jìn)行的研究工作及取得研究成果。盡我所知，除了文中特