JAVA字節(jié)碼的部分計值技術(shù)及正確性研究.pdf

1、本文主要包括四部分內(nèi)容。第一部分介紹了部分計值技術(shù)的理論基礎(chǔ)和研究現(xiàn)狀以及應用。第二部分介紹了Java虛擬機的體系結(jié)構(gòu)和Java語言部分計值研究的發(fā)展現(xiàn)狀。第三部分是本文的重點，選擇Java字節(jié)碼程序作為部分計值研究的對象，首先按照Java語言的特性把Java分為了五個層次，命名為JavaI、JavaC、JavaO、JavaE和JavaT，然后分析了由JavaI程序編譯得到的JVMLI字節(jié)碼程序的指令序列結(jié)構(gòu)，定義了JVMLI字節(jié)碼程序

2、的指稱語義，并在此基礎(chǔ)上形式化的提出了JVMLI程序的部分計值規(guī)則，然后定義了部分計值正確性的含義并使用歸納法證明了這些計值規(guī)則的正確性。本文的最后一部分簡單討論了JVMLC 、JVMLO 、JVMLE 和JVMLT 的部分計值，由于引入了面向?qū)ο蠛彤惓Ｌ幚?，特別是線程機制的思想，研究語言語義的難度就迅速增大，該部分的研究工作還在繼續(xù)進行，主要是使用抽象狀態(tài)機（ASM,Abstract State Machine）[25]來刻劃Java