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

1、沈陽工業(yè)大學碩士學位論文Z規(guī)格說明中集合論算子的自動求精研究及實現(xiàn)姓名：李巍巍申請學位級別：碩士專業(yè)：計算機軟件與理論指導(dǎo)教師：王宏生20050312沈陽工業(yè)大學碩士學位論文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