versionesc

esc  时间:2021-02-23  阅读:()
ESCJavaStaticAnalysisSpectrumPowerCostTypecheckingData-flowanalysisModelcheckingProgramverificationAutomatedManualESCIsThisProgramCorrectintsquare(intn)intk=0,r=0,s=1;while(k!
=n)r=r+s;s=s+2;k=k+1;returnr;}TypecheckingnotenoughtocheckthisNeitherisdata-flowanalysis,normodelcheckingProgramVerificationProgramverificationisthemostpowerfulstaticanalysismethodCanreasonaboutallpropertiesofprogramsCannotfullyautomateBut…Canautomatecertainparts(ESC/Java)TeacheshowtoreasonaboutprogramsinasystematicwaySpecifyingProgramsBeforewecheckaprogramwemustspecifywhatitdoesWeneedformalspecificationsEnglishcommentsarenotenoughWeuselogicnotationTheoryofpre-andpost-conditionsStatePredicatesApredicateisabooleanexpressionontheprogramstate(e.
g.
,variables,objectfields)Examples:x==8x=0)UsingPredicatestoSpecifyProgramsWefocusfirstonhowtospecifyastatementHoaretripleforstatementS{P}S{Q}SaysthatifSisstartedinastatethatsatisfiesP,andSterminates,thenitterminatesinQThisistheliberalversion,whichdoesn'tcareaboutterminationStrictversion:ifSisstartedinastatethatsatisfiesPthenSterminatesinQpreconditionpostconditionHoareTriples.
Examples.
{true}x=12{x==12}{y>=0}x=12{x==12}{true}x=12{x>=0}(Programssatisfymanypossiblespecifications){x=0}x=fact(n){x==n!
}{true}a=0;if(x!
=0){a=2*x;}{a==2*x}ComputingHoareTriplesWecomputethetriplesusingrulesOneruleforeachstatementkindRulesforcomposedstatementsAssignmentAssignmentisthesimplestoperationandthetrickiestonetoreasonabout!
{y>=2}x=5{}{x==y}x=x+1x=5{x==y}{}x=x+1{x==y}{}x=x+1{x2+y2==z2}{x2+y2==z2}x=x+1{}AssignmentRuleRuleforassignment{Q[x:=E]}x=E{Q}Examples:{12==12}x=12{x==12}{12>=0}x=12{x>=0x=x+1{x>=0}{x>=1}x=x+1{}QwithxreplacedbyEx==12withxreplacedby12RelaxingSpecificationsConsider{x>=1}x=x+1{x>=2}Itisverytightspecification.
WecanrelaxitExample:{x>=5}x=x+1{x>=2}(sincex>=5)x+1>=2)x=E{P}ifP)Q[x:=E]{Q}Assignments:forwardandbackwardTwowaystolookattherules:Backward:givenpost-condition,whatispre-conditionForward:givenpre-condition,whatispost-conditionx=E{}{Q}x=E{P}{}Assignments:forwardandbackwardTwowaystolookattherules:Backward:givenpost-condition,whatispre-conditionForward:givenpre-condition,whatispost-conditionx=E{Q[x:=E]}{Q}x=E{P}{}Assignments:forwardandbackwardTwowaystolookattherules:Backward:givenpost-condition,whatispre-conditionForward:givenpre-condition,whatispost-conditionx=E{Q[x:=E]}{Q}x=E{P}Exampleofrunningitforward{x==y}x=x+1{}Exampleofrunningitforward{x==y}x=x+1{}ForwardorBackwardForwardreasoningKnowthepreconditionWanttoknowwhatpostconditonthecodeestablishesBackwardreasoningKnowwhatwewanttocodetoestablishMustfindinwhatpreconditionthishappensBackwardisusedmostoftenStartwithwhatyouwanttoverifyInsteadofverifyingeverythingthecodedoesWeakestpreconditionwp(S,Q)istheweakestPsuchthat{P}S{Q}Orderonpredicates:Strong)Weakwpreturnsthe"best"possiblepredicatewp(x:=E,Q)=Q[x:=E]Ingeneral:S{P}ifP)wp(S,Q){Q}WeakestpreconditionThispointstoaverificationalgorithm:Givenfunctionbodyannotatedwithpre-conditionPandpost-conditionQ:ComputewpofQwithrespecttofunctonbodyAskatheoremprovertoshowthatPimpliesthewpThewpfunctionwewilluseisliberal(Pdoesnotguaranteetermination)Ifusingbothstrictandliberalinthesamecontext,theusualnotationiswlptheliberalversionandwpforthestrictoneStrongestpreconditionsp(S,P)isthestrongestQsuchthat{P}S{Q}Recall:Strong)Weakspreturnsthe"best"possiblepredicatesp(x:=E,P)=…Ingeneral:S{P}{Q}ifsp(S,P))QStrongestpostconditionStrongestpostconditionandweakestpreconditionsaresymmetricThispointstoanequivalentverificationalgorithm:Givenfunctionbodyannotatedwithpre-conditionPandpost-conditionQ:ComputespofPwithrespecttofunctonbodyAskatheoremprovertoshowthatthespimpliesQComposingSpecificationsIf{P}S1{R}and{R}S2{Q}then{P}S1;S2{Q}Example:x=x-1;y=y-1{x>=y}ComposingSpecificationsIf{P}S1{R}and{R}S2{Q}then{P}S1;S2{Q}Example:x=x-1;y=y-1{x>=y}Intermsofwpandspwp(S1;S2,Q)=wp(S1,wp(S2,Q))sp(S1;S2,P)=sp(S2,sp(S1,P))ConditionalsRulefortheconditional(flowgraph)Example:E{P}{P1}ifP&&E)P1TF{P2}ifP&&!
E)P2x==0{x>=0}TF{x==0}sincex>=0&&x==0)x==0{x>=1}sincex>=0&&x!
=0)x>=1Conditionals:ForwardandBackwardRecall:rulefortheconditionalForward:givenP,findP1andP2pickP1tobeP&&E,andP2tobeP&&!
EBackward:givenP1andP2,findPpickPtobe(P1&&E)||(P2&&!
E)OrpickPtobe(E)P1)&&(!
E)P2)E{P}{P1}providedP&&E)P1TF{P2}providedP&&!
E)P2JoinsRuleforthejoin:Forward:pickPtobeP1||P2Backward:pickP1,P2tobeP{P1}{P2}{P}providedP1)PandP2)PReviewE{P}{P1}ifP&&E)P1TF{P2}ifP&&!
E)P2{P1}{P2}{P}ifP1)PandP2)Px=E{P}{Q}ifP)Q[x:=E]ImplicationisalwaysinthedirectionofthecontrolflowReview:forwardE{P}{P&&E}TF{P&&!
E}{P1}{P2}{P1||P2}x=E{P}{\exists…}Review:backwardE{(E)P1)&&(!
E)P2)}{P1}TF{P2}{P}{P}{P}x=E{Q[x:=E]}{Q}Example:Absolutevaluestaticintabs(intx)//@ensures\result>=0{if(x0)c-returnx;}x0c--TFExample:Absolutevaluex0c--TFExample:Absolutevaluex0c--TFInSimplifyIMPLIESTRUE(AND(IMPLIES(c0)0x)0)IMPLIES(=x0)AND(IMPLIES(>c0)(>=x0)IMPLIES(=x0))))))1:Valid.
>Sofar…FrameworkforcheckingpreandpostconditionsofcomputationswithoutloopsSupposewewanttocheckthatsomeconditionholdsinsidethecomputation,ratherthanattheendstaticintabs(intx){if(x0)c-returnx;}Saywewanttocheckthatx>0hereAsserts{Q&&E}assert(E){Q}Backward:wp(assert(E),Q)=Q&&EForward:sp(assert(E),P)=assert(E)QQ&&Eassert(E)PExample:Absolutevaluewithassertstaticintabs(intx){if(x0)if(c>0)c-returnx;}x0)TFc>0c--TFExample:Absolutevaluewithassertx0)TFc>0c--TFExample:Absolutevaluewithassertx0)TFc>0c--TFAddingthepostconditionbackinx0)TFc>0c--TFAddingthepostconditionbackinx0)TFc>0c--TFAnotherExample:DoubleLocking"Anattempttore-acquireanacquiredlockorreleaseareleasedlockwillcauseadeadlock.
"Callstolockandunlockmustalternate.
locklockunlockunlockLockingRulesWeassumethatthebooleanpredicatelockedsaysifthelockisheldornot{!
locked&&P[locked:=true]}lock{P}lockbehavesasassert(!
locked);locked=true{locked&&P[locked:=false]}unlock{P}unlockbehavesasassert(locked);locked=falseLockingExample…lock…x==0…unlockx==0TT{!
L&&P[L:=true]}lock{P}{L&&P[L:=false]}unlock{P}{!
L}{!
L}LockingExample…lock…x==0…unlockx==0TT{!
L&&P[L:=true]}lock{P}{L&&P[L:=false]}unlock{P}{!
L}{!
L}LockingExample:forwarddirection…lock…x==0…unlock{!
locked}{!
locked&&x==0}{!
locked&&x0}x==0TT{!
locked&&x==0}{locked&&x==0}{locked=(x==0)}{locked&&x==0}{!
locked&&(x==0)}{!
locked&&x0}{!
locked}

819云互联(800元/月),香港BGP E5 2650 16G,日本 E5 2650 16G

819云互联 在本月发布了一个购买香港,日本独立服务器的活动,相对之前的首月活动性价比更高,最多只能享受1个月的活动 续费价格恢复原价 是有些颇高 这次819云互联与机房是合作伙伴 本次拿到机房 活动7天内购买独立服务器后期的长期续费价格 加大力度 确实来说这次的就可以买年付或者更长时间了…本次是5个机房可供选择,独立服务器最低默认是50M带宽,不限制流量,。官网:https://ww...

PacificRack(19.9美元/年)内存1Gbps带vps1GB洛杉矶QN机房,七月特价优惠

pacificrack怎么样?pacificrack商家发布了七月最新优惠VPS云服务器计划方案,推出新款优惠便宜VPS云服务器采用的是国产魔方管理系统,也就是PR-M系列,全系基于KVM虚拟架构,这次支持Windows server 2003、2008R2、2012R2、2016、2019、Windows 7、Windows 10以及Linux等操作系统,最低配置为1核心2G内存1Gbps带宽1...

cera:秋季美国便宜VPS促销,低至24/月起,多款VPS配置,自带免费Windows

介绍:819云怎么样?819云创办于2019,由一家从2017年开始从业的idc行业商家创办,主要从事云服务器,和物理机器819云—-带来了9月最新的秋季便宜vps促销活动,一共4款便宜vps,从2~32G内存,支持Windows系统,…高速建站的美国vps位于洛杉矶cera机房,服务器接入1Gbps带宽,采用魔方管理系统,适合新手玩耍!官方网站:https://www.8...

esc为你推荐
免费建站系统免费建站系统哪个好?网店系统也行ovOV摄像头是哪个国家的flash导航条谁来帮我看看这样的flash导航条 下面的页面该怎么设计硬盘人克隆一个人需要多少人多长时间啊免费免费建站最好的免费建站lockdowndios8.1怎么激活内置卡贴商标注册查询官网全国商标注册查询在哪里查呀?云挂机云软件挂机赚钱是骗子服务器连接异常主服务器连接异常office2007简体中文版求office2007免费版下载地址 无需破解无需激活无须密钥
淘宝二级域名 vmsnap3 国外空间 骨干网络 双拼域名 如何用qq邮箱发邮件 爱奇艺vip免费领取 web服务器安全 drupal安装 新睿云 阿里云个人邮箱 windowsserver2008 中美互联网论坛 server2008 建站行业 达拉斯 流媒体服务器软件 最年轻博士 qq空间登陆首页 灵动鬼影实录剧情 更多