如果您无法下载资料，请参考说明：
1、部分资料下载需要金币，请确保您的账户上有足够的金币
2、已购买过的文档，再次下载不重复扣费
3、资料包下载后请先用软件解压，在使用对应软件打开
资料内容仅供您学习参考，如有不当或者侵权，请联系改正或者删除。StrategiesofModelingfromVDM-SLtoJMLJinDan,YangZong-Yuan(DepartmentofComputerScienceandTechnology,EastChinaNormalUniversity,Shanghai,41,China)E-mail:,AbstractVDM-SLisoneofthemostpopularformallanguageusedinsoftwaredevelopment,itsmathematicalapproachallowsunambiguousspecificationanddevelopmentofhighintegritysoftware.JMLisabehavioralinterfacespecificationlanguagetailoredtoJava(TM).AndtheexistingJML-basedtoolsofdebugging,verifyingandtestingaremature.ThispaperdiscussesthetwokindsofspecificationlanguageandprovidesanoveldesignmappingVDM-SLtoJMLofconstantvalues,variablesandconstraints.Thestrategiesofthedesignareillustratedwithanexample.specificationoflowabstractlevel.Andweillustrate1.Introductionthedesigninanexample.OurgoalistofacilitateuseofexistingJML-basedtoolstoverifyVDM-SLcode.Insoftwareengineering,usingnaturallanguage(NL)tospecifythesystemisapracticalchoice.Forexample,thetoolssupportUMLdiagramsarecommon.However,NLmayimportinconsistencyforsystemsbecauseofitspolymorphism,ambiguityandcontext-sensitiveness,especiallyforcomplicatedsystemsandhighintegritysoftware.Ontheopposite,formallanguagehasmanygreatfeatures.Formalmethodusestheformalspecificationlanguagetodescribesoftwarerequirements.Anditusespreciseandunambiguoussemanticstoensurethesystem’scorrectnessandmaintainability.Formalmethodcanbeclassifiedas5approaches[1],ofwhichonerepresentativemethodisVDM.VDM(theViennaDevelopmentMethod)[2]isafunction-basedshapemodelinglanguage.ItisbasedonADT(AbstractDataType),andusesabstractmodelingtoexpressthefunctionofADT.ThelanguagehasitsmathematicalsymbolsandproofrulesforcollectionsandusesHoare’spreandpostconditionstospecifyoperations.AcentralelementofVDMistheISOStandardspecificationlanguageVDM-SL[3].2.ThesyntaxofVDM-SLVDMisasoftwaredevelopmentmethodbasedonformalsemantics.Itprescribesthreestepsfordevelopinglargesoftware:proposerequirements,formaldefinitionsanddevelopment.Itisalsoatop-downmethodofrefinement.Formals
立即下载
