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

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

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

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

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