资源描述：
《a hoare logic for monitors in javanew》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、AHoareLogicforMonitorsinJavaOctober25,2002ErikaAbraham-Mumm1;2,FrankS.deBoer3,Willem-PauldeRoever1,andMartinSte en11Christian-Albrechts-UniversityKiel,Germany2Albert-Ludwigs-UniversityFreiburg,Germany3CWIAmsterdam,TheNetherlandsAbstract.Besidesthefeaturesofaclas
2、s-basedobject-orientedlan-guage,Javaintegratesconcurrencyviaitsthread-classes,allowingforamultithreaded
owofcontrol.Besidesshared-variableconcurrencyviainstancevariables,synchronousmessagepassing,anddynamicthreadcreation,Java'sconcurrencymodelo ersreentrantsynchro
3、nizationmon-itorsviaspeci cmethodcalls,waitandnotify.Toreasonaboutsafety-propertiesofmultithreadedprograms,weintro-duceanassertionalproofmethodforJavaMT(Multi-ThreadedJava"),asmallconcurrentsublanguageofJava,coveringthementionedconcur-rencyissues,speci cally,Java
4、'smonitordiscipline,aswellastheobject-basedcoreofJava.1IntroductionThesemanticalfoundationsofJava[16]havebeenthoroughlystudiedeversincethelanguagegainedwidespreadpopularity(seee.g.[6,31,13]).TheresearchconcerningJava'sprooftheorymainlyconcentratedonvariousaspectso
5、fse-quentialsub-languages(seee.g.[20,34,28]).In[5]asoundandcompleteproofsystemispresentedforJava'sreentrantmultithreadingconcept.Inthispaperweillustratehowinformationaboutothermechanismscanbeincorporatedintheproofsystembymeansofauxiliaryvariableswhichdescribetheco
6、rresponding
owofcontrol:Wedescribeanextensionoftheproofsystemtomonitorsyn-chronization.WeintroduceanabstractprogramminglanguageJavaMT,asubsetofJava,featuringdynamicobjectcreation,methodinvocation,objectreferenceswithaliasing,and,speci cally,concurrencyandJava'smon
7、itordiscipline.ThebehaviorofaJavaMTprogramresultsfromtheconcurrentexecutionofmethods.Tosupportacleaninterfacebetweeninternalandexternalobjectbehavior,JavaMTdoesnotallowquali edreferencestoinstancevariables.Asaconsequence,shared-variableconcurrencyiscausedbysimulta
8、neousexecutionwithinasingleobject,only,butnotacrossobjectboundaries.Inordertocaptureprogrambehaviourinamodularway,theassertionallogicandtheproofsystemar
