Z規(guī)格說(shuō)明中集合論算子的自動(dòng)求精研究及實(shí)現(xiàn).pdf

1、沈陽(yáng)工業(yè)大學(xué)碩士學(xué)位論文Z規(guī)格說(shuō)明中集合論算子的自動(dòng)求精研究及實(shí)現(xiàn)姓名：李巍巍申請(qǐng)學(xué)位級(jí)別：碩士專業(yè)：計(jì)算機(jī)軟件與理論指導(dǎo)教師：王宏生20050312沈陽(yáng)工業(yè)大學(xué)碩士學(xué)位論文SetTheoryOperatorAutomaticRefinementResearchandImplementationinZSpecificationAbstractItisfrequentlydi韶d、碰I哮ollstotheimprovementofsoft

2、warequalityandproductivitythatinformalspecificationdiscribedbym咖relanguagef北quenUyisobscureanddivergentFormalmethodwaspreferredinordertooverridedefieiencyofspecificationdiscribedby02tRlrelanguageZispresentlythemostfashio

3、nableformalspecificationButaSawholethetheoryandtechnologyofZspecificationisn’textensivelyappliedinindustryfieldSo，thetheoryofautomaticrefinementfromZspecificationtohighlanguageispreferredHoweveritsrealizationmakesslowpro

4、gressTherefore，thissubjectstudiesautomaticrefinementofsettheoryoperatorinordertOdevelopaentirecompilerwhichcanmakeaconvertofZspecificationtocompiledhighlevelprogrammelanguageAtfirstthesubjectmainlydiscussesfollowingaspec

5、ts：firststudyZspecificationdatatypesandrelationshipamongdatatypes；SecondpreferthethoughtthatusingcontainersinSTLexpressZspecifi鈕fiondatatypesinordertostudyautomaticrefinement；Thirddesigntherefinementruleofsetreferencebag

6、sequenceetcdatatypesinZusingCandSTLtechnology；Fourthofferfunctiontemplateforautomaticrefinementfromoperat。orsinsettheorytoC抖codeandmakesrefinementruleofoperatorinsettheorybytemplatetechnologyiIlClanguageandSTLtemplatelib

7、rarysupportingdataconstructionandgenemlalgorithmThenbasingOnabovestudy，designZTOCautomaticrefinerStudyincludes：Firstdesignthesymboltableinautomaticrefinementh鋤dlingprocess；SecondpmcccdlexicalanalysisofZspecification；Thir

8、ddesigngrammarrule婦SmartZmodifiedandproceedgrammaranalysisbytopdownparsingandgiveeliordealing；Fourthinstageofsemanticsanalysisproceedstatics跚lailticscheckingandrefreshtheinformationinsymboltable；FiRkgeneratetargetIrrogra

9、rnme(c=code)inaccordingtOtheinformationinanalysisofsemanticsandsymboltable，aswellastherefinementruleofsettheoryoperatoringeneratingtargetcodestageItisimportantfortheapplicationofformalapproachandformalspecificationinalls