Animating Z Using Logic Programming Techniques

AnimatingZUsingLogicProgrammingTechniquesMichaelWinikoffzPhilipDartEd.Kazmierczakfwinikoff,philip,[e-mail]˜fwinikoff,philip,edgDepartmentofComputerScienceTheUniversityofMelbourneAUSTRALIAzNowattheInstituteforSoftwareResearch,Fairmont,WVAbstract:Onemethodfordetectingerrorsinaformalspecificationisan-imation.Itiscomplementarytotheoremprovingandcanbehighlycost-effective,particularlyearlierindevelopment.InmytalkI’lldiscussanimationofthespecificationnotationZ.I’llar-guethat:1.itisdesirabletoperformanalysispriortoexecution;2.logicprogramminglanguagesareanattractivetargetforan-imationsofZ;3.modeanalysiscanhelpbridgethegapbetweenZandMer-cury.Thedetailsofamodeanalysisalgorithmwillbepresented.Animation?Automaticallyderivingprototypesfromspecifica-tions.Exploration:moregeneralthanexecution.IterativeconstructionofmathematicalmodelsEarlyfeedback–usefulforverificationPrototypecanbedemonstrated–usefulforvali-dationMoreaccessabletodevelopers(lightweight)Complementarytotheoremproving1Ourapproach1.Specifyinanotationwithsemanticsinfirstordersettheory;2.Translatespecificationintoalogicprogram;3.Executelogicprogramtoexplorepropertiesofthespecification.2WhyZ?(“Zed”,not“Zee”)ChallengingWellknownWidelyusedWhyMercury?LogicisclosetoZSoundExpressescontrolthroughseparateannotationsEfficient3SystemStructure(Z)FirstOrderSetTheoryExecutable(Mercury)ModeAnalysisSpecificationSubtypeTranslationAnalysisWenowfollowthejourneyofaspecification...4TranslatingtoLogic1.Typecheck&Infergenerics2.Expandschemaoperations3.Flattenexpressionsintopredicates4.SimplifyPredicates(eg.8):9:)5.Translateparagraphsintodefinitions6.TranslatedefinitionsintoHornclauses5TranslatingtoLogic:ExampleSd=[x:PZ;y:Njy=#x]Id=[S0jx0=?]Ad=[S;v?:Zjx0=x[fv?g]8S(x;y),9cxnat(y)^card(Z;x;cx)^y=cx8S(x;x0;y;y0),S(x;y)^S(x0;y0)8I(x0;y0),9esemptyset(Z;es)^x0=es^S(x0;y0)8A(x;y;x0;y0;v?),9sv;tmakeset(v?;sv)^union(Z;x;sv;t)^x0=t^S(x;x0;y;y0)6Analyses:Why?GlobalanalysiscangivemoregeneralresultsthanexecutionBetterfeedbackfornon-animatablespecificationsMoreflexibleanimationstrategypossible7ModeAnalysisAninstantiationisanabstractedsubstitution.Weab-stracttosetsofgroundvariables.Amodeisadescriptionoftheeffectofexecutingaformulaasafunctionfrominputinstantiationtooutputinstantiation.Ifaformulacanbegivenamodethenitcanbeexe-cutedinthatmode.Notethatsincewearelookingatanabstractexecu-tionweneedtodesignourmodeanalysiswithrespecttoagivenexecutionmodel.Sinceourexecutionmodelinvolvessequential,lefttorightexecutionofconjunctionsweneedtoensurethatconjunctionsareputintoanexecutableorder.8OutlineAnalysisModeAnalysisSubtypelogicLogicmodedlogicdeterminemodessequenceconjunctions9Optimisations:VariantEquivalenceClassesSupposewehaveaconjunctionofthreeformulaewithmodes:F1::fxg)fygF2::fxg)fzgF3::fyg)fqgThereareanumberofwaysinwhichtheconjunctioncouldbeexecuted.Alloftheseareequivalentandwewouldliketoonlyconsideroneofthem.F1^F2^F3F2^F1^F3F1^F3^F210ExampleLibrarymodes:nat(y)::fyg)?card(Z;x;cx)::fxg)fcxgemptyset(Z;es)::?)fesgmakeset(v?;sv)::fv?g)fsvg;fsvg)fv?gunion(Z;x;sv;t)::fx;svg)ftg;ftg)fx;svgx=y::fxg)fyg;fyg)fxgModesfoundbyanalysis:S(x;y)::fxg)fygS(x;x0;y;y0)::fx;x0g)fy;y0gI(x0;y0)::?)fx0;y0gA(v?;x;x0;y;y0)::fv?;xg)fx0;y;y0gA(v?;x;x0;y;y0)::fx0g)fv?;x;y;y0g11Example(continued)Ifwealsoallowthemodeunion(Z;x;sv;t)::ft;xg)fsvg;ft;svg)fxgthenwehavethefollowingadditionalmodes:A(v?;x;x0;y;y0)::fv?;x0g)fx;y;y0gA(v?;x;x0;y;y0)::fx;x0g)fv?;y;y0gThemodeanalysisgeneratesdifferentversionsofapredicatefordifferentmodes:8Aiiooo(v?;x;x0;y;y0),9sv;tmakesetio(v?;sv)^unioniiio(Z;x;sv;t)^equalsoi(x0;t)^Siioo(x;x0;y;y0)8Aooioo(v?;x;x0;y;y0),9sv;tequalsio(x0;t)unioniooi(Z;x;sv;t)Siioo(x;x0;y;y0)makesetoi(v?;sv)12SubtypesWhat?Determiningsubtypes(asopposedtobasetypes).Forexample,seqZasopposedtoP(ZZ).Why?EfficiencyRepresentationSofttyping:Introduceneededchecksandthenuseanalysistodeterminewhichareredundant.13SubtypeAnalysisOutlineAnalysisModeAnalysisSubtypedeleteredundantchecksLogicmodedlogicmodedlogicinsertsubtypechecksanalyseexecutionconstraints14ExampleRequirementsandConstraints8Aiiooo(v?;x;x0;y;y0),9sv;tmakesetio(v?;sv)^svF^xF^svF^unioniiio(Z;x;sv;t)^(tF,svF^xF)^tF^equalsoi(x0;t)^(x0F,tF)^xF^x0F^Siioo(x;x0;y;y0)8Aooioo(v?;x;x0;y;y0),9sv;tequalsio(x0;t)^x0F,tF^tF^unioniooi(Z;x;sv;t)^(tF,svF^xF)^xF^svF^xF^x0F^Siioo(x;x0;y;y0)^svF^makesetoi(v?;sv)15CompilingtoMercury8Aiiooo(v?;x;x0;y;y0),9sv;tmakesetio(v?;sv)^xF^unioniiio(Z;x;sv;t)^equalsoi(x0;t)^Siioo(x;x0;y;y0)A_iiooo(_v_q,_x,_x_p,_y,_y_p):-makeset_io(_v_q,_sv),finite(_x),num_o(__num),union_iiio(__num,_x,_sv,_t),equals_oi(_x_p,_t),’_$Delta_S_iioo’(_x,_x_p,_y,_y_p).16ToolkitNeedtoprovideanimplementationoftheZtoolkitfordifferentmodes.Someoperationscanbederivedautomaticallyfromother,moreprimitive,operations(e.g.62)Issues:finiteness(primes),overflow(Zvs.int)Correctness17RelatedWorkStateoftheartisfairlyprimitive.Criteria:Sound(proof?)AutomatedImplementedAnalysis18ComparisonTableSoundAutomatedImplementedAnalysisZ-HaskellNA✗✓NAzxNA✗✓NAUttin