基于C++STL技術(shù)實(shí)現(xiàn)Z形式規(guī)格說(shuō)明求精變換的研究.pdf

1、軟件開(kāi)發(fā)的形式化方法被當(dāng)今軟件工程領(lǐng)域譽(yù)為克服“軟件危機(jī)”，提高軟件可靠性和生產(chǎn)效率的革命性途徑。為了克服自然語(yǔ)言和程序設(shè)計(jì)語(yǔ)言描述規(guī)格說(shuō)明的模糊性和歧義性缺陷，人們提出了形式化開(kāi)發(fā)范型，即通過(guò)形式化、規(guī)范化的數(shù)學(xué)理論，用描述“做什么”來(lái)取代“怎么做”。Z語(yǔ)言就是形式化方法中具有代表性的一種形式規(guī)格說(shuō)明，它語(yǔ)言精確、無(wú)二義性，可以用于推理和對(duì)需求規(guī)格說(shuō)明求精。求精是規(guī)格說(shuō)明實(shí)現(xiàn)可執(zhí)行化的重要過(guò)程，實(shí)現(xiàn)規(guī)格說(shuō)明求精，可以為Z語(yǔ)言應(yīng)用于更廣

2、泛的領(lǐng)域奠定基礎(chǔ)。本文重點(diǎn)研究Z形式規(guī)格說(shuō)明的求精方法，以Z的數(shù)據(jù)型求精為基礎(chǔ)，對(duì)Z形式規(guī)格說(shuō)明進(jìn)行自頂向下，逐步求精，結(jié)合C++語(yǔ)言、數(shù)據(jù)結(jié)構(gòu)以及C++標(biāo)準(zhǔn)模板庫(kù)技術(shù)，探討Z規(guī)格說(shuō)明的求精方法。Z是一個(gè)類(lèi)型化的語(yǔ)言，有豐富的數(shù)據(jù)類(lèi)型，其數(shù)據(jù)類(lèi)型分為簡(jiǎn)單類(lèi)型與復(fù)合類(lèi)型。由于Z語(yǔ)言的數(shù)據(jù)類(lèi)型相當(dāng)復(fù)雜，現(xiàn)有的高級(jí)語(yǔ)言不支持Z語(yǔ)言數(shù)據(jù)類(lèi)型的直接轉(zhuǎn)換。但是，C++語(yǔ)言的標(biāo)準(zhǔn)模板庫(kù)中定義的容器類(lèi)型卻為Z語(yǔ)言數(shù)據(jù)類(lèi)型的轉(zhuǎn)換提供了良好的支持，本文先對(duì)