Software.Abstractions.Logic.Language.and.Analysis.Apr.2006

《Software.Abstractions.Logic.Language.and.Analysis.Apr.2006》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、49194Jackson1/31/069:30AMPage1SoftwareAbstractionscomputerscience/softwareengineeringSoftwareAbstractionsLogic,Language,andAnalysisDanielJacksonInSoftwareAbstractionsDanielJacksonintroducesanewapproachtosoftwaredesignthatdrawsontraditionalformalmethodsbutexploitsautomatedtoolstofind

2、flawsasearlyaspossible.Thisapproach—whichJacksoncalls“lightweightformalmethods”or“agilemodel-ing”—takesfromformalspecificationtheideaofapreciseandexpressivenotationbasedonatinycoreofsimpleandrobustconceptsbutreplacesconventionalanalysisbasedontheo-remprovingwithafullyautomatedanalys

3、isthatgivesdesignersimmediatefeedback.JacksonhasdevelopedAlloy,alanguagethatcapturestheessenceofsoftwareabstractionssimplyandsuccinctly,usingaminimaltoolkitofmathematicalnotions.Thedesignercanuseautomatedanalysisnotonlytocorrecterrorsbutalsotomakemodelsthataremorepreciseandelegant.T

4、hisapproach,Jacksonsays,canrescuedesignersfrom“thetarpitofimplementationtech-nologies”andreturnthemtothinkingdeeplyaboutunderlyingconcepts.SoftwareAbstractionsintroducesthekeyelementsoftheapproach:alogic,whichpro-SoftwareAbstractionsvidesthebuildingblocksofthelanguage;alanguage,whic

5、haddsasmallamountofsyntaxtothelogicforstructuringdescriptions;andananalysis,aformofconstraintsolvingthatoffersbothsimulation(generatingsamplestatesandexecutions)andchecking(findingcoun-terexamplestoclaimedproperties).ThebookusesAlloyasavehiclebecauseofitssimplici-Logic,Language,andA

6、nalysistyandtoolsupport,butthebook’slessonsaremostlylanguage-independent,andcouldalsobeappliedinthecontextofothermodelinglanguages.DanielJacksonisProfessorintheDepartmentofElectricalEngineeringandComputerScienceandleadstheSoftwareDesignGroupattheComputerScienceandArtificialIntellige

7、nceLabatMIT.“Abstractionistheessenceofsimpleandeffectivesoftwaredesign,andlogicistheessentialJacksonDanielJacksontoolforexploringandvalidatingabstractions.Thesebasicinsights,whichhavebeenlabori-ouslyrediscoveredbymanypracticingprogrammers,arenowaccessibletostudentsandpro-fessionalsa

8、talllevelsofexperie