A Formal Software Development Approach Using Refinement Calculus

(整期优先)网络出版时间:2001-03-13
/ 1
TheadvantageofCOOZ(CompleteObject-OrientedZ)istospecifylargescalesoftware,butitdoesnotsupportrefinementcalculus.Thusitsapplicationisconfinedforsoftwaredevelopment.IncludingrefinementcalculusintoCOOZovercomesitsdisadvantageduringdesignandimplementation.Theseparationbetweenthedesignandimplementationforstructureandnotationisremovedaswell.Thenthesoftwarecanbedevelopedsmoothlyinthesameframe.ThecombinationofCOOZandrefinementcalculuscanbuildobject-orientedframe,inwhichthespecificationinCOOZisrefinedstepwisetocodebycalculus.Inthispaper,thedevelopmentmodelisestablished,whichisbasedonCOOZandrefinementcalculus.Datarefinementishardertodealwithinarefinementtoolthanordinaryalgorithmicrefinement,sincedatarefinementusuallyhastobedoneonalargeprogramcomponentatonce.Astotheimplementationtechnologyofrefinementcalculus,thedatarefinementcalculatorisconstructedandanapproachfordatarefinementwhichisbasedondatarefinementcalculusandprogramwindowinferenceisoffered.