versionesc

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}