Science

MartinWard

ComputerScienceDept

ScienceLabsSouthRdDurhamDH13LE

January17,2003

Abstract

Whatdoesitmeantosaythatoneprogramis“moreabstract”thenanother?Whatis“abstract”aboutanabstractdatatype?Whatisthedifferencebetweena“high-level”programanda“low-level”program?Inthispaperweattempttoanswerthesequestionsbyformallydefininganabstractionrelationbetweenprogramswhichmatchesourintuitiveideasaboutabstraction.Therelationisbasedonexaminingtheoperationalsemanticsoftheprograms,expressedasasetoftraces(sequencesofstates)fromagiveninitialstatetoapossiblefinalstate.

KEYWORDS:

Abstraction,SoftwareMaintenance,Transformations,Refinement,TransformationalProgramming

1Introduction

Indiscussingsoftwaredevelopment,refinementofspecificationsintoprograms,reverseengineeringfromprogramsintospecifications,andotherrelatedareas,conceptssuchas“high-levelprogram”verses“low-levelprogram”,“crossinglevelsofabstraction”,“abstractdatatypes”,andsoonarebandiedaboutwithoutalwaysbeinggivenacleardefinition.Theconceptof“refinement”hasbeenformallydefined:forexamplein[1,2,3,7];butasweshallseebelow,theinformalconceptofabstractionwouldappeartobemuchsharperthantheconceptofrefinement,sincemanyprogramswhichwewould(informally)regardasverydifferentintheirdegreeofabstraction,are(formally)equivalentinthesensethateachisaformalrefinementoftheother.

Someoftheintuitiveideasaboutabstractionwewouldliketocapturearelistedbelow.Thesearetherequirementswhichwewouldexpectanyabstractionrelationtosatisfy:

1.Abstractspecificationssaywhataprogramdoeswithoutnecessarilysayinghowitdoesit.2.Abstractionisaprocessofgeneralisation,removingrestrictions,eliminatingdetail,removinginessentialinformation(suchasthealgorithmicdetails).3.Abstractspecificationshave“morepotentialimplementations”,movingtoalowerlevelmeansrestrictingthenumberofpotentialimplementations.

2Examples

1.Compare:

(a)Calculatetheproductofaandbandstoretheresultinc;

(b)Calculatetheproductofaandbusingonlyadditionandstoretheresultinc.

1

Someexampleswillhelptofixourintuitiveideasaboutthedifferentformsofabstraction:

2.(a)Aspecificationwhichassignsanyvaluetoxwhichislargerthanthevalueofy:

󰀒x󰀓/󰀒󰀓.(x>y)

(b)Arefinementofthisis:x:=y+1.

3.(a)Arecursivefunction(thisformofrecursionoccursforexampleinthesolutionofthe

famous“TowersofHanoi”problem):

functF(n,x)≡ifn>0thenF(n−1,φ(n,F(n−1,x)))

elsexfi.

(b)Anequivalentiterativeformis:

functF(n,x)≡

forc:=2n−1step−1to1do

x:=φ(ntz(c)+1,x)od;x.functntz(c)≡“thenumberoftrailingzerosinthebinaryrepresentationofc”.

4.(a)Somesortingexamples:Thefirstisaspecificationofaprogramwhichsortsthesegment

a..bofarrayA:

SORT(a,b)=DFA[a..b]:=A󰀂[a..b].(sorted(A[a..b])∧perm(A[a..b],A󰀂[a..b]))Where

sorted(A[a..b]=DF∀i,a󰀂iand

perm(A[a..b],A󰀂[a..b])=DF∃π:a..b󰀁→a..b.∀i,a󰀂i󰀂b.A[i]=A󰀂[π[i]]

whereπ:a..b󰀁→a..bmeanspiisabijection(a1–1andontofunction)fromtheset{a,a+1,...,b}toitself,i.e.πisapermutationofa..b;(b)Thesecondisaspecificationofaquicksortprogram:

QSORT1(a,b)=

beginp:󰀒A[a..b],p󰀓:=󰀒A󰀂[a..b],p󰀂󰀓.

(A󰀂[a..p󰀂−1]󰀂A󰀂[p󰀂]󰀂A󰀂[p󰀂+1..b]∧perm(A[a..b],A󰀂[a..b]));SORT(a,p−1);SORT(p+1,b)end

(c)Thethird(QSORT2)isafullimplementationofthequicksortalgorithm(forexample

using“medianofthree”partitioning,see[4,6]).[7]formallyprovestheequivalenceofthisalgorithmtothespecificationSORT(a,b).Eachoftheseexamplesillustratesadifferentaspectof“abstraction”,Iwouldarguethatineachcasethefirstversionisthemostabstract,withlaterversionsbecomingmoreconcrete.However,withtheexceptionofcase(2),alltheexamplesarecasesofformalequivalence.

Clearlyaproperrefinementofaspecification(i.e.arefinementwhichisnotequivalent)oughttobeconsideredas“moreconcrete”thanthespecification,notleastbecausesomeimplementationfreedomhasbeenlost(seerequirement3).Forsimilarreasonsitisimportanttorestricttheabstractionrelationtoprogramsandspecificationswhicharealreadyrelatedbyrefinementorequivalence.However,asalreadynoted,refinementbyitselfisnotasufficienttestforabstraction.Acursoryexaminationoftheexamplesrevealsoneobviouscommonfeature:themoreabstractversionsareallshorterthantheconcreteversions.Thisleadstothefollowing(ratherna¨ıve)definitionofabstraction:

2

Definition1IfS1andS2arestatementssuchthatS2refinesS1thenwesayS1ismoreabstractthanS2ifandonlyifS1isshorterthanS2.

Thisdefinitionisunsatisfactoryforseveralreasons.Firstwefeelthatabstractionismoreofasemanticissuethancanbecapturedinacrudesyntactictest:forexample,addingalongsequenceofskipstatementstoanabstractspecificationdoesnotturnitintoaconcreteimplementation!Thisparticularfailingcanberectifiedbyinsistingontheapplicationofasmallsetof“simplifying”transformations(suchasskipdeletion)totheprogramsbeforetheirsizesarecompared.Amoresubstantivecounterexampleisaprogramwhichcarriesoutafairlycomplextaskwithafewshortlinesofcode.Herethehigh-leveldescriptionof“whattheprogramdoes”couldturnouttobeconsiderablylongerthantheprogramitself.Forexampleconsiderthefollowinggraph-markingalgorithm:

beginmark(root)where

procmark(x)≡ifm[x]=0

thenm[x]:=1;mark(l[x]);mark(r[x])fi.end

Thisprogrammarksallthenodesxreachablefromtherootnoderootviaunmarkednodes.Forsimplicityweassumethatanyunusedpointerspointtoaspecialnodewhichisalwaysmarked.Theabstractspecificationinvolvesdefiningwhenanodeisreachable:

󰀂

MARK≡m:=m󰀂.∀x.(x∈reachable(root,m)⇒m󰀂[x]=1)󰀃󰀂∧(x∈/reachable(root,m)⇒m[x]=m[x])

reachable(root,m)=DF

󰀁

reachablen(root,m)

where:

n<ω

reachable0(root,m)=DF{root}

reachablen+1(root,m)=DFreachablen(root,m)

∪{y|∃x∈reachablen(root,m).(y=l[x]∨y=r[x])∧m[y]=0}

i.e.reachablen(root,m)isthesetofnodesreachablefromrootinnorfewerstepsthroughasequence

ofnodeswhichareunmarkedinm.

Analternativedefinitionofreachablewhichmaycorrespondmorecloselytotheintuitiveidea,istodefineareachablenodetobeanunmarkednodeforwhichthereisapathofunmarkednodesreachingfromtheroottothatnode:

reachable(root,m)=DF{x|∃p∈paths(root,m).p[󰀠(p)]=x}

󰀁

paths(root,m)=DF{󰀒x1,...,xn󰀓|x1=root∧∀i,1󰀂i󰀂n.m[xi]=0

n<ω

∧∀i,1󰀂iEitherofthesedefinitionsresultsinanabstractprogramwhichisconsiderablylongerthanthe

recursiveimplementation.

Wearelookingforasemanticdefinitionofabstraction:asdiscussedabove,denotationalse-manticsaloneareinsufficienttoexpresstherelationsowewillexamineoperationalsemantics.In[8]and[7]weintroducedawide-spectrumprogrammingandspecificationlanguage(calledWSL)withitsformalsyntaxanddenotationalsemantics.Aproperstatesconsistsofafinitenon-emptysetVofvariables,eachofwhichisassignedavaluetakenfromtheuniversalsetofvalues,H.Thespecialstate⊥isusedtodenotenonterminationorerror.VHdenotesthesetofallstateonVandH(including⊥).AWSLprogramS,executingfromaninitialstates∈VH,mayeither

3

runforeverwithoutterminating(inwhichcasethe“finalstate”is⊥),ormustterminateinsomestatet∈WHforsomesetoffinalvariablesW.(ThesetWisdeduciblefromVandS).SinceWSLprogramsmaybenondeterministic,theremaybeasetofpossiblefinalstatesforeachinitialstate.SothedenotationalsemanticsofaWSLprogramcanbegivenbyastatetransformationf,afunctionfromVHto℘(WH),whichmapseachinitialstatestothesetf(s)ofpossiblefinalstates.

3OperationalSemantics

Statetransformationsaresufficienttoexpressthedenotationalsemanticsofprogramsandspecific-ations.However,todefineourabstractionrelationweneedamore“detailed”semantics,namelyoperationalsemantics.Theoperationalsemanticsofaprogramgivesforeachinitialandfinalstatethesetoftraces(sequencesofintermediatestates)whichtheprogrampassesthrough.

Definition2Traces:Atracefromfinitenon-emptysetsofvariablesVtoWonasetHofvaluesisafinitesequenceofstatesoflength󰀃2whosefirstelementisinVHandfinalelementinWH.Thelengthofatraceσis󰀠(σ),thefirstelementisσ[1]andthelastelementisσ[󰀠(σ)].Asubsequenceofσmaybedenotedσ[a..b].Theconcatenationoftwotracesρandσisdenotedρ++σDefinition3Statetrace:AstatetraceTfromVtoWisasetoftracesfromVtoWonHwitheachtraceσ∈ThavingitsfirstelementinVHandlastelementinWH.Ifthetraceσ∈Tincludes⊥asitsnthelement(forn>1)thenTmustalsoincludeallpossiblewaysofextendingσfromthe(n−1)thelementonwards.LetTH(V,W)denotethesetofallstatetracesfromVtoWonHandletΓVWHbethesetofalltracesfromVtoWonH.Then:󰀂

T∈TH(V,W)⇐⇒󰀒⊥,⊥󰀓∈T∧∀σ∈T.σ[1]∈VH∧σ[󰀠(σ)]∈WH

󰀃

∧∀i,2󰀂i󰀂󰀠(σ).(σ[i]=⊥⇒∀ρ∈ΓVWH.σ[1..i−1]++ρ∈T)

ForeachstatetraceTtherecorrespondsastatetransformation,fTformedbytakingfT(s)tobethesetoffinalelementsofthetracesinTwhoseinitialelementiss,i.e.

fT(s)=DF{t∈WH|∃σ∈T.(σ[1]=s∧σ[󰀠(σ)]=t)}

In[5,7]thesemanticsofstatetransformationsarefurtherdevelopedandusedtoprovevariousrefinementsandtransformationsofprograms.

Ifweexaminetheoperationalsemanticsofthevariousexampleswenotethatthemoreconcreteversionsareeitherproperrefinementsoftheabstractcases,orhavemorestatesintheirtraces(compareQSORT1whichcontainsaspecificationstatementwhereQSORT2hasaloop),orhavemore(local)variablesintheinnerstatesintheirtraces(theiterativeversionofexample(3a)usesthelocalvariablec).Thethirdcaseisexpressedinthisdefinitionofabstractiononstates:

󰀂arestateswhereV⊆V󰀂and∀x∈Definition4Abstractiononstates:Ifs∈VHands󰀂∈VH

V.s(x)=s󰀂(x)(i.e.sands󰀂havethesamevaluesonvariablesinV)thenwesaysismoreabstractthans󰀂(ors󰀂ismoreconcretethans)andwrites󰀔s󰀂

Weusethisrelationtodefineabstractionbetweensequencesofstates,wherethemoreconcretesequencemay“fillin”gapsintheabstractsequence:

󰀂Definition5Abstractiononstatesequences:Ifρ=󰀒s1,...,sn󰀓andρ󰀂=󰀒s󰀂1,...,sm󰀓arese-󰀂󰀂󰀂quencesofstateswiths1,s󰀂1∈VHandsn,sm∈WHands1=s1andsn=smandn,m>1andthere

isa1-1increasingfunctionπfrom{2,...,n−1}to{2,...,m−1}suchthat∀i,1󰀂󰀂thenwesaythatρandismoreabstractthanρandwriteρ󰀔ρ.

Finally,thisextendstoadefinitionofabstractiononstatetraces:

4

Definition6Abstractiononstatetraces:IfTandT󰀂arestatetracesinTH(V,W)andif∀ρ∈T.∃ρ󰀂∈T󰀂.(ρ󰀔ρ󰀂)thenwesaythatTismoreabstractthanT󰀂andwriteT󰀔T󰀂.

ThisdefinitionsatisfiestheLemma:

Lemma1ForanystatetracesT,T󰀂∈TH(V,W)withcorrespondingstatetransformationP,P󰀂∈FH(V,W):

IfT󰀔T󰀂thenP󰀂P󰀂Inotherwords,aconcreteversionofanabstractprogramisalwaysarefinementofit.Theconversedoesnotholdingeneral:thesortingprogramsareallequivalentbutclearlyatdifferentlevelsofabstraction.

Themostabstractpossibleprogramisalsotheleastrefined,namelyabort.Thisfitswithourintuitionofabstractionastheremovalofinformation:insomesenseabortcontainsnoinformationatallanddoesnotrestricttheimplementorinanyway.3.1

TheReplacementTheorem

Animportantpropertyforanynotionofrefinementisthereplacementproperty:ifanycomponentofastatementisreplacedbyanyrefinementthentheresultingstatementisarefinementoftheoriginalone.Thisiseasilyprovedbyaninduction,onalexicalorderof:(i)Thedepthofrecursionnesting;(ii)Thelengthoftheprogramtext.

Wehaveacorrespondingtheoremfortheabstractionrelation:ifwereplaceanycomponentofaprogrambyamoreabstract(moreconcrete)componentthenthewholeprogrambecomesmoreabstract(concrete).

4Non-SemanticSpecifications

1.Calculatetheproductofaandbandstoretheresultinc.

2.Calculatetheproductofaandbusingonlyadditionandstoretheresultinc.

Wehaveyettoconsiderindetailthefirstexamplewhichconsidersthefollowingspecifications:

Thefirstofthesespecificationsmaybeexpressedasthesingleatomicspecification󰀒c󰀓/󰀒󰀓.(c=a.b),whichassignssomevaluetocsuchthattheconditionc=a.bissatisfied.Thesecondspecific-ationsayssomethingaboutthekindofstepsallowedinthecomputation,itcannotthereforebeexpressedsimplyasaspecificationstatement.Aspecificationstatementonlydefinesthedenota-tionalsemantics,butthisspecificationputsarestrictionontheoperationalsemantics:inthiscasethevalueofeachvariableineachstatemustbeeitheraknownconstantorasumordifferenceofvaluesofvariablesinthepreviousstate.Onewayofexpressingthisrestrictionisasfollows:begina0:=a;b0:=b;n:=“somepositiveinteger”:fori:=1step1tondo

Carryoutsomeadditionorsubtractionorassignaconstantvaluetoavariable...od;[c=a0.b0]end

Heretheifstatementinthelooppicksarandomaddition/subtractionoperationbetweenanytwovariablesandthefinalguardensuresthattheoutcomeoftheseoperationsresultsinchavingthevaluea0.b0.(See[7]foradefinitionoftheguardstatement).Weclaimthatthiscorrectlyexpressesthespecificationinthesensethatthisprogrammeetsthespecificationandismoreabstractthananyotherprogramwhichmeetsthespecification.Notehoweverthatthefollowingprogramcouldbearguedasmeetingourspecificationalthoughitisclearlyagainstthespiritoftheinformalspecification:

5

begina0:=a;b0:=b;n:=a.b:c:=0;

fori:=1step1tondo

c:=c+1od

5Conclusion

Inthispaperwehavesoughttoprovideaformaldefinitionofan“abstraction”relationwhichcorrespondsmorecloselytotheintuitiveideasofabstractandconcreteprograms,andhigh-levelverseslow-levelprograms.Asimplesyntacticdefinition(size)isshowntobeinadequate,andanydefinitionofabstractionwhichisbasedonlyonthedenotationalsemanticsofapairofprogramsisalsoshowntobeinadequate.Ourdefinitionisthereforebasedontheoperationalsemanticsofprograms:aprogramS1isanabstractionofanotherprogramS2ifeachofthepossibleexecutionsequencesforS1consistsofasubsequenceofapossibleexecutionsequenceforS2.

6References

[1]R.J.R.Back,CorrectnessPreservingProgramRefinements,MathematicalCentreTracts#131,Math-ematischCentrum,Amsterdam,1980.[2]R.J.R.Back&J.vonWright,“RefinementConceptsFormalisedinHigher-OrderLogic,”FormalAspects

ofComputing2(1990),247–272.[3]C.C.Morgan,ProgrammingfromSpecifications,Prentice-Hall,EnglewoodCliffs,NJ,1994,Second

Edition.[4]R.Sedgewick,Algorithms,AddisonWesley,Reading,MA,1988.

[5]M.Ward,“ProvingProgramRefinementsandTransformations,”OxfordUniversity,DPhilThesis,1989.[6]M.Ward,“DerivationofaSortingAlgorithm,”DurhamUniversity,TechnicalReport,1990,󰀂http://

www.dur.ac.uk/∼dcs0mpw/martin/papers/sorting-t.ps.gz󰀃.[7]M.Ward,“FoundationsforaPracticalTheoryofProgramRefinementandTransformation,”Durham

University,TechnicalReport,1994,󰀂http://www.dur.ac.uk/∼dcs0mpw/martin/papers/foundation2-t.ps.gz󰀃.[8]M.Ward,“AbstractingaSpecificationfromCode,”J.SoftwareMaintenance:ResearchandPractice5

(June,1993),101–122,󰀂http://www.dur.ac.uk/∼dcs0mpw/martin/papers/prog-spec.ps.gz󰀃.

6