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

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

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

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

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