748 Chapter3 DescribinSg yntaxandSemant.ics
3.5.3 AxiomaticSemantics
Axiomatic semantics, thus namedbecauseit is basedon mathematicallogic, is t h e m o s t a b s t r a c t a p p r o a c h t o s e m a n t i c s s p e c i f i c a t i o n d i s c u s s e di n t h i s c h a p t e r . Rather than directly specifring the meaning of a program, axiomatic semantics s p e c i f i e sw h a t c a n b e p r o v e n a b o u t t h e p r o g r a m . R e c a l l t h a t o n e o f t h e p o s s i b l e usesof semanticspecificationsis to prove the correctnessof programs.
In axiomaticsemantics,thereisnomodelofthestateofamachineorpro- g r a m o r r n o d e l o f s t a t e c h a n g e st h a t t a k e p l a c e w h e n t h e p r o g r a m i s e x e c u t e d . The meaning of a program is basedon relationships among program variables and constants,which are the samefor every execution of the progru-.
Axiomatic semanticshastwo distinct applications:program verification and program semanticsspecification.This sectionfocuseson program verification in its descriptionof axiomaticsemantics.
Axiomatic semanticswasdefinedin conjunctionwith the developmentof an approachto proving the correctnessof programs.Suchcorrectneisproofs, when they canbeconstructed,showthat aprogram performs the computation describedby its specification.In a proof, eachstatementof a program is both precededand followed by a logical expressionthat specifiesconstruint, on pro- gram variables.These, rather than the entire stateof an abstractmachine (as with operationalsemantics),areusedto specifzthe meaningof the statement. The notation usedto describeconstraints-indeed, the languageof axiomatic semantics-is predicate calculus.Although simple Boolean expressionsare often adequateto expressconstraints,in somecasesthey arenot.
When axiomatic semanticsis used to specify formally the meaning of a statement,the meaningis definedby the statement’seffecton assertionrrborrt the dataaffectedbv the statemenr.
3.5.3.1 Assertions
The logical expressionsusedin axiomaticsemanticsare calledpredicates,or assertions. An assertionimmediately preceding a program sratemenrdescribes the constraintson the program variablesat that point in the program. An asser- tion immediately following astatementdescribesthe new constraintson those variables(and possiblyothers) after executionof the statement.These asser- tions arecalledthe precondition andpostcondition, respectively,of the srate- ment. For two adjacentstatements,the postcondition of the first servesasthe precondition of the second.Developing an axiomaticdescriptionor proof of a given program requires that every statement in the program has both a pre- condition and a postcondition.
In the following sections,we examineassertionsfrom the point of view that preconditions for statementsare computed from given postconditions, although it is possibleto considerthesein the oppositesense.We assumeall variablesareintegert),?e.Asasimpleexample,considerthefollowing assign- ment statementand postcondition:
sum=2*x+1{sum>1i
ls rpter. ntics
;sible
pro- rted. rbles
rand rtion
rt of rofs, tion loth pro- : (as ent. Latic are
ofa fout
r o f bes ;er- ose ;er- rte- the i o f re-
ew trSt all
F-
arepresentecl
in braces
ilc,
ffif:fjlti ihirrtrt.-.ittJtltTt
statemt”‘,. to distin- on. p”*ili. ir..o,rairionfor
3’5 Describing
the Meaningosf programs:
Dynamiscemantics
749
*o postcondition assertions
ij,lt*tam
In axiomaticsemantics,the meaning of a specific
statementis defined by :1lll’,?i3fi::;i3J:,ldj::”nidi[,H,’,”.*ou,,.,iio’,,p..iq,p,
In the following r,,br..iions, we focus on correctness
and programs, which is proofs of statements
eralconcept
of axiomatiscemantics.is
acommon useof axiomaticsemantics.Tt
ments and to ,,r,. p…iselythe,r.njffif,|:fl::_
anteethe validiv
precondition that will guar- of the associatedpost.onaiiion. For exampre,in the
programs in renns of logic .rp;;;;;s.
program
verification is one
application of axiomatic descriptiois
3.5.3.2 Weakestpreconditions
The weakest precondition is the leasrrestrictive
“f ;;;;;.r.
ment and postconditiongiven i’ section state-
i.I.l.r,.r* , ro1, {x , so}, and allvalid”preconditiotr.
Th. *eakest ,ri’ii..onditions Iil,r’.rlt l?].’:’ “r in
If the weakestprecondition can be
postcondition
computed from the most generar for each of the sratemenrrypd of a language,then
cessesused to compure thesepreconditio.rr’p.o,,’a. the pro_
the semanticsof that langurg.i structed for programs in ihnil”r,
, .-o..?* J.r..rptio’ or
F,,rrh.rrrro..i.lrr..,rr.ss proofs
can be con_
*n:*lli:.*”…,,,ri,.o?1f,:’f, ,,ff {i.nf
sratemenr,,,”,il”:’J:TH,r.’,’n’ffi
This precondition isth.rr.rr.j.r
,T”,,l*jll
j,L:ilf, :x}il..”j::iffi
;f,}lnx:**.mHfl
por.orraliio, ro.the
99 secondlastsrate_
menr’This processcontinues
At that unt’ ,1i q.s-;t;; of theprogramisreached.
point, the preconditionof the fi;:;;;;;:ment statesthe underwhichthe-programwill compute
specification
;::,Hl’;;i3iji:i’,p,,t of,r,.p.rg,amt,heprosramhasbeen
An inference rule is a method of inferring the truth of one assertionon
:ni:::
r;|*r*tues
ofoth..lrr.rtions.Th;;;,r.rat formof,,,inference
51,52,… ,sz S
This rulestatesthatif s1,s2,…, andsn aretrue,thenthetruthof inferred’ The top part of aninference
part is rule is calledi,, calledits consequent.
“rrr”””dent;
s canbe the botto’r
An axiom is a logical statementthat is assumedto be true. Therefore, axiomisaninferencerulewithout anantececlent.
– For someprogram statements,the .”-p;;;;ion
from rhe statementand a posrcondition
r. iffir”a
an
of a weakest precondition
can be specifiedby a’
conditions thedesiredresultsI.f theseconditions
150 Chapter3
DescribinSg yntaxandSemantics
axiom.In mostcasesh,owever,theweakestpreconditioncanbespecifiedonly by an inference rule.
To useaxiornaticsemanticswith a given programming language,whether for correctnessproofs or for formal semantiis specificatiJns,e”ithJran axiom or an inference rule must exist for each kind of statement in the language.In the following subsections,\Mepresent an axiom for assignmentstatementsand inferencerulesfor statementsequencess,electionstatements,andlogicalpre- testloop statementsN. ote that we assumethat neither arithmetic noi Booiean expressionshavesideeffects.
3.5.3.3 AssignmenSt tatements
The precondition and postcondition of an assignmentstatement together d e f i n e p r e c i s e l y i t s m e a n i n g . T o d e f i n e t h e m e a n i n g o f a n a s s i g n m e n ts t a t e – ment’ given a postcondition, there must be a way to compute its precondition from that postcondition.
Let x = E be a generalassignmentstatementand Q be its postcondition. Then, its precondition, P , is defined by the axiom
P = Q”-E
which meansthat P is computedasQ with all instancesof x replacedby E. For example,if we havethe assignmentstatementand postconditi,on
a=b/z-1ia.10)
the weakestprecondition is computed by substiruting b / z – t for a in the postcondition {a . 1o}, asfollows:
b/2 1<10 b<22
Thus, the weakestprecondition for the given assignmentstatement and post- condition is {b . 221.Remember that the assignmenraxiom is guarant"id to be_corr:ectonly in the absenceof side effects.An assignmentsti'tement has a sideeffectif it changessomevariableother than its rarget.
The usualnotation for speci$ringthe axiomaticsemanticsof agivenstate- ment form is
{P}S{Q}
where P is the precondition, Q is the postcondition, and S is the srarement form. In the caseof the assignmentstatement,the notation is
{Q"-n} t =E{Q}
ttly
her rom .In and lre-
lean
ther nte- ition
tion.
,.For
L n t h e
post- eedto :hasa
state-
-ement
3.5 Describintghe Meaningosf ProgramsD:ynamjSc emantics 157
As another exampleof computing a precondition for an assignmentstate- ment, considerthe foliowing:
x=2*y 3{tr25}
The preconditioniscomputedasfollows:
)*\/ y>1-4
3>25
14} is the weakestprecondition for this assignmentstatementand
So {y t postcondition.
Note that the appearanceof the left sideof the assignmentstatementin its right sidedoesnot affectthe processof computing the weakestprecondition’ For example,for
X=X+y 3 {t ‘ 10}
the weakestprecondition is
x+y 3>10 y>13 X
R e c a l l t h a t a x i o r n a t i cs e t n a n t i c sw a s d e v e l o p e dt o p r o v e t h e c o r r e c t n e s so f programs.In light of that, it is natural at this point to wonder how the axiom l o r a s s i g n r n e n ts t a t e m e n t sc a n b e u s e d t o p r o v e a n y t h i n g . H e r e i s h o w : A g i v e n assignmenrstatementwith both a precondition and a postconditioncan be con- s i d e l e d a l o g i c a l s t a t e m e n t , o r t h e o r e m . I f t h e a s s i g n m e n ta x i o m , w h e n a p p l i e d to the postcondition and the assignmentstatement,producesthe given pre- condition, the theorernis proved.For example,considerthe logical statement
{xt3ix=x 3{*’ o} Using the assignmentaxiom on
x = x – 3 {x t 0}
produces{x , :}, which is the given precondition. Therefore, we haveproven the examplelogical statement.
Next, considerthe logical statement tx > 5J x 3 {*’ 0}
In this case,the given precondition, {x t 5}, is not the sameasthe assertion producedbytheaxiom.However,it isobviousthat{x > s}implies{x ‘ 3}.
752 Chapter3
1.$ .
T o use this in a proof, an inference rule, named the rule of cnnsequence, is needed.The form of the rule of consequenceis
{P}S{Q},P’-rP,Q=’Q’ {P’}S{Q’}
The =>qrmbolmeans”implies,”andScanbeanyprograrnstaternent.-fherule canbestatedasfollows:If thelogicalstatement{P}S{Q}istrue,theassertion P’ implies the assertionP ,and the assertionQ irnpliesthe assertionQ’, then it can be inferred that {P’} S {Q’}. Itr other words, the rule of consequencesays that a postcondition can alwaysbe weakenedand a precondition can alwaysbe strengthened.This is quite useful in program proofs. For example,it allows the completion of the proof of the lastlogicalstatementexarnpleabove.If we let P be{x ‘ 3},Q andQ’be {x t 0},andP’be {x ‘ 5},wehave
DescribinSg yntaxandSemantics
txt5ix:
x-3txtOl
Thefirsttermoftheantecedent({* t 3} X=X- 3 {* t o})wasproven with the assignment axiom. The second and third terms are obvious. f’here- fore, by the rule of consequence, the consequent is true.
3.5.3.4 Sequences
T h e w e a k e s tp r e c o n d i t i o n f o r a s e q u e n c eo f s t a t e m e n t sc a n n o t b e d e s c r i b e db y an axiom, becausethe precondition dependson the particular kinds of state- ments in the sequence.In this case,the precondition can only be describedwith aninferencerule.Let S1and52beadjacentprogramstaternentsI.f S1and52 have the following pre- and postconditions
{PUS1{P2} {P2}52{P3i
the inferencerule for sucha two-statementsequenceis
{PU S1{P2},{P2}52 {P3} {P1}S1,52 {P3}
So, for our example,{P1}S1;52 {P3} describesthe axiornaticsemanticsof thesequenceS1;52.The inferencerulestatesthattogetthesequencepre- condition, the precondition of the secondstatementis computed. This new assertionis then usedasthe postcondition of the first statement,which can then be used to compute the precondition of the first statement, which is alsothe precondition of the whole sequence.If S1 and 52 are the assignment statements
3’5 Describing
theMeanings programs:
Dynamic semantics
xl=E1 and x2=E2
then we have
{P3*2-s2}x2= E2 {p3} {(P3*z-nz)”r-nr}x1= E1 ip3*z,eu}
Therefore, rhe wlake_spt recondition for the sequ-encexl
y=3*x+l.
X=V+?. J
{x.1o}
The precondition for the secondassignmentstatementis Y<7
which is usedasthe postcondirion for the first statement.The precondition
of
153
= E1;
For example,consid* th. f"ilowing sequenceandpostcondition:
postconditionp3 is
r
= p2
x2 *ir6
the first assignmentstatement can now
3*x+1--t x<2
'
for
{(p3"2__-Ez)xr_El}.
so' {x ' 2} is the precondition of both the first starementand the statementsequence. rwo-
3.5.3.5 Selection
consider theinference
y;ffil ruleforselection statements,
if B then 51 etse 52
we consideronly selectionsthat include else crausesT. he inferencerule is
{B andP} S1{e}, i(not B) andp} S2{e}
{P}if BrhenSt "r*
STie}
This rule indicates that selection statements must be proven both when
Boolean control expressionis ffue the and when it i, irtr.. The first rogical stare_
ment abovethe line representsthe then clause;th. r..ond representsthe erse
be computed,
thegeneral form
754 Chapte3r DescribinSgyntaxandSemantjcs
clause.According ro the inferencerule, we need a precondition P that can be usedin the precondition of both the then and else clauses.
Consider the following exampleof the cornputation of the precondition using the selecrioninferencerule. The exampleselectionstatementis
A s i g n i f i c a natm o u n to f w o r k hasbeendoneonthePossibilitY of usingdenotationalal nguage descriptiontos generate compilerasutomaticalYl(Jones, 1980;Milosetal.,1984;
Bodwinet al.,1982).These effortshaveshownthatthe methodisfeasibleb,uttheworl< hasneverprogressetdo the pointwhereit canbeusedto generatuesefucl ompilers.
y=y+r{VrO}
3.5.3.6 LogicalPretestLooPs
Another essendalconstructof imperativeprogramming languages is the logicalpfetest,or while loop. Cornputing the weakestpre- condition for a while loop is inherently more difficult than for a sequence,becausethe number of iterations cannot alwaysbe predetermined.In a casewhere the number of iterations is known,
ifx>0then
\/\/- v-tL
efse
V=V+1 JJ
‘1
Supposethe posrcondition,Q, for this selectionstatementis {y canusethe axiomfor assignmenton the then clause
y=y-1{V’0}
> o}.We
Thisproduces{y – 1 r 0}or{y r 1}.ItcanbeusedasthePpartofthe
ffipreconditionforthethenclause.Nowweapp1ythesameaxiom to the else clause
o} or {y ‘
use{y > r} for the precondition of the whole selectionstatement.
1}’ Because{y t f}=>{y t -1},theruleofconsequencealiowsusto
which producesthe precondition {y
+ 1 >
the loop canbe unrolled and treatedasa sequence.
The problem of computing the weakestprecondition for loops is similar
to rhe probl.- of proving a theorem about all positiveintegers.In the latter case,induction isnormally used,andthe sameinductivemethod canbeusedfor someloops.The principal stepin induction is finding an inductive hypothesis. The correspondingstepin the axiomaticsemanticsof a while loop is finding an asserrioncalled a loop invariant, which is crucial to finding the weakest precondition.
The inferencerule for computirlg the precondition for a while loop is
{I and B} S {l
{I} while B do S end {I and (not B)}
where I is the loop invariant. This seemssimple, but it is not. The cornplexity lies in finding an appropriateloop invariant.
–
3.5 Describintghe Meaningosf ProgramsD:ynamiSc emantjcs t55
The axiomatic description of-a while loop is written as {P}wtrile B do S end {Q}
The loop invariant must satisfira number of requirements to be useful. First, the weakestprecondition for the while loop must guaranteethe truth of the loop invariant. In turn, the loop invariant must guaranteethe truth of thepostconditionuponlooptermination.Theseconstraintsmoveusfrom the inf’erencerule to the axiornaticdescription.During executionof the loop, the truth of the loop invariant must be unaffectedby the evaluationof the loop- controllingBooleanexpressionandtheloopbodystatementsF. {ence,thenarne irturtriant.
Another complicatingf-actorfor while loopsis the questionof loop termi- nation.A loopthatdoesnot terminatecannotbecorrect,andin factcomputes nothing. If Q is the postconclitionthat holds irnrnediatelyafter loop exit, then a precondition P for the loop is one that guaranteesQ at loop exit and also guaranteesthat the loop terminates.
T’he compieteaxiomaticdescriptionof a while constructrequiresall of the following’to be true, in which I is the loop invariant:
P=tI
{I and B} S {I} (Iand(notB))=’ Q the loop terminates
If a loop colnputesa sequenceof numeric values,it may be possibleto find a loop invariant using an approachthat is usedfor determining the inductive hypothesiswhen mathematicalinduction is used to prove a statementabout a rnathematicalsequence.The relationshipbetweenthe number of iterations and the precondition for the loop body is computed for a few casesw, ith the hope that a pattern emergesthat will apply to the generalcase.It is helpful to treat the processof producing a weakestprecondition asa function, wp. In general
wp(staternent,postcondition) = preconclition
A *p function is often calledapredicate transfoffner, becauseit takesapredi- cate,or assertion,asa parameterand returns another predicate.
To find I, the loop postconditionQ isusedto computepreconditionsfor severaldifferentnurnbersofiterationsoftheloopbody,startingwith none.If the loop body contains a single assignmentstatement,the axiom for assign- ment statementscanbeusedto computethesecases.Considerthe example loop:
while y
Rernemberthat the equalsign is being usedfor rwo different purposeshere. In assertionsi,t meansmathematicalequality;outsideassertionsi,t meansthe assignmentoperator.
756 Chapte3r DescribinSgyntaaxndSemantics
For zero iterations, the weakestprecondition is, obviously,
{v=x}
For one iteration, it is wp(V=y+I,{V=x})={V+1-x},or{y=x-r}
For rwo iterations, it is
wp(V=y +7, {V=x – ri)={y +1- x – 1},or{y =x – 2} For three iterations,it is
wp(V=y+I, iV=x-2j)={y+1-x-z},or{y=x 3}
It is now obvious that {y . x} will suffice for casesof one or more iterations. Combining this with {y = x} for the zero iterations case,we get {y <= x}, whichcanbeusedfortheloopinvariant.Apreconditionforthewhile state- ment canbe determinedfrom the loop invariant.In fact,I canbe usedasthe precondition, P .
We must ensure that our choice satisfiesthe four criteria for I for our exampleloop. First, becauseP = I, P => I. The secondrequirement is that it must be true that
{I and B} S {I}
In our example,we have
{v<=xandy
Applying the assignmentaxiom to y=y+1{V<=x}
we get {y + 1 <= x}, which is equivalentto {y . x}, which is implied by {v <= xandY
Next, we must have {Iand(notB)}=' Q
In our example,we have
So,this is obviouslytrue. Next, loop termination must be considered.In this example,the questionis whether the loop
{v<=x}whileY
3.5 Describintghe Meanings programs:
of Dynamiscemantics 157
terminates.Recallingthatx andy areassumedto beintegervariables,it iseasy to seethat this loop doestenninate. The precondition [rraranteesthat y ini- tially is not larger-thanx. The loop body increments y with eachiteration, until y is equal to x. No matter how much smaller y is than x initially, it will even- tually becomeequalto x. So the loop will terminate.Becauseour choiceof I satisfiesall four criteria, it is a satisfacioryloop invariant and loop precondition.
_ The previous processused to compure th. irrrrrriant fop tt"p does not
alwaysproduce an assertionthat is the weakestprecondition (although it does in the example).
As another exampleof finding a loop invariant using the approachusedin mathematical induction, consider the fojlowing loop sratement:
whiles>1dos=s/zend{s=1}
As before, we use the assignmentaxiom to try to find a loop invariant and a precondition for the loop. For zero iterations, the weak.ri p…ondition is {s = r}. For one iteration.it is
wp(s=s/ 2, {s=ril ={s/ z=1),or{s =z} For two iterations,it is
wp(s=s/2,{s=2j)={s/z-2j,or{s =+} For three iterations,it is
wp(s=s/2,{s=+\l={s/2-+},or{s=B} From these cases,\Mecan seeclearly that the invariant is
{s is a nonnegative power o f z j
Onge again,the computed I can serveasP,and I passesthe four requirements.
Unlike our earlier exampleof finding a loop precondition, this one clearly is
lot a weakestprecondition. Consider using th. pr..ondition {s , r1. The logical statement
{st1}whiles>1dos=s/Zend{s=1}
can easilybe proven, m_dthis precondition is significantly broader than the one computed earlier.The loop and precondition are satisfiedfor any positive valuefor s, not just pow”ersof 2, asthe processindicates.Becauseof the rule of c o n s e q u e n c e u, s i n g a p r e c o n d i t i o n t h a t i s s t r o n g e r t h a n t h e w e a k e s t p r e c o n d i – tion doesnot invalidatea proof.
Finding loop invariants is not alwayseasy.It is helpful ro understand the nature of these invariants. First, a loop invariant is a weakenedversion of the loop postcondition and also r pr..orriition for the loop. so, I must be weak enough to be satisfiedprior to the beginning of loop execution,but when
combined with the loop exit condition,lt rn,rrt be strong enough to force the truth of the postcondition.
i I
I I I
I] t
158 Chapter
3 DescribiSngyntaaxndSemantjcs
Becauseof the difliculry.of proving loop termination, rhat requirernent is often ignored- If loop terrninaiior .ni, be ,ho-n, the axiornaricdescription of the loop is calledtotal correctness. If the other conclitionscan be rlet but terminatiotl is not guaranteed,it is calleclpartial correctness.
In nrore complexloops,_findinga suiiableloop invarianr,evenfor partial
correctnessr,equiresa goocl-deaol f ingenuity.Becausecompllting the pre-
conclitionfor awhile loop depenclson fir-,.lir-,agloop invariant,piurrirrg:th.
correctnessof progralllsr.i’ithwhile loopsusiirgaxiomaticsemanticscanbe difficult.
3.5.3.2 programproofs
This sectiotlproviclesvalidationsfcrrrlo sirnpleprog’rams.The first exalrple of a correctnessprotlf is for ..u.ry short prog-ram,consistingo- f a sequerr..nf t h r e e a s s i g u l t l e n st t : t t e l l r e n t t s h a t i n t e r c h a n g e t h e v a l u e s o f r w o v a r i a b l e s .
{x=AANDy=Bi i*-
J_
JI
L.
BANDv -a-}
)
Becausetrhe progranr consistsentirelv of assignmentstatementsin a sequence’the assiqrrtllentaxiotn ,rnclthe irrierence,irl. fo, sequencesca’ be usedto prove its correc-tnessT.he flrst stepis to usethe assignrr..rl,axiom ol the last statemenrand the postconclitionior the whore proir.rrr. ‘fhis yields the precondition
{x=BANDt. = A}
Nert, we usethis ner,r’preconditionasa posrconditionon the rliclcllestate- rnent and compute its precondition, which ii
{v=BANDT=A}
Next, we usethis new assertionasthe postconditionon the first srarernent
and applvthe assig’nment
ariom, which vi.lds
{v=BANDx=A}
which is the sallle:lsthe preconclitionon the progranl, exceptfbr t6e clrclerof operandson the ANDoperator.BecauseANDis’as1)n’,metric
is con-rplete.
The fbllowing eratnpleis a proof of correctnessof a pse.clococleprogra’r that computesthe flctorial function.
{xr
operator,our proof
3.5 DescribintgheMeaningosfProgramsD:ynamiscemantics {n>=0i
759
nnrrnt- – uvuffu
t1 .
-l t^ar .
LAUL L, while count
= fact * count,’ COunt.=COUnt-l. i
end {fact=nl}
fact
-fhe rnethod describedearlier for finding the loop invariant doesnot work for the loop in this example.Someingenuity is requiredhere,which canbe aided by a brief studyof the code.The loop computesthe factorialfunction in order oith. last rnuitiplication first; that is, (n – 1) * n is done first, assurningn is grezrterthan 1. So,part of the invariantcanbe
fact = (count+1) * (count+2) * * (n 1l * n
But we lnust alsclensurethat count is alwaysnonnegative,which we can do by adding that to the assertionabove’to get
I – (fact (count + 1) * n) AND(count >= 0)
Next, w-emust confirm that this I meets the requiremen$ for invariants. once againweletI alsobeusedforP,soPclearlyimpliesI.The nextques-
tion is
{I and B} S tI} IandBis
((fact = (count + 1) * (count
* n) AND (count >= 0)) AND
which reduces to
(fact.=(count+1)* *n)AND(count>0)
ln our case,we tnust compute the precondition of the body of the loop, using the invariant for the postcondition.For
tP)count = count – 1 {t} we compute P to be
t(fact = count. * (count + 1) * * n) AND (count>=1))
160 Chapte3r DescribinSgyntaxandSemantics
using this asthe postcondition for the first assignmentin the loop body,
{P} fact = fact. * count {{tact = count * (count + 1) *n)AND(count>=1))
In this case,P is
{(fact =(count.+1) *n)AND(count>=1)}
It is clearthat I and B implies this p, so by the rule of consequence, {I amoB}S{r}
istrue.Finally,thelasttestofI is
Iamo(NorB)=’ Q
For our examplet,his is
((fact = (count + 1) * n) AND (count >= O)) AND (count = 0)) => fact = nt
This is clearly true, for when count = o, the first part is precisely the defini- t i o n o f f a c t o r i a l . S o , o u r c h o i c e o f I m e e t s t h e r e q u i r e m e n t s ^ f o rr l o o p i n v a r i a n t . Now \Mecanuseour P (which is the sameasI) from the while asthe posrcon- dition on the secondassignmentof the program
{p}fact=1{tfact =(count+1) *n)AND (count. >= 0) )
which yields for P
(f = (count + f-) * n) AND (count >= 0))
using this asthe posrcondition for the first assignmentin the code
{P}count=n{tf =(count+1) *n)AND (count >= 0)) )
producesfor P
{t” + 1) *…* n = 1) AND(n >=0)}
The left operand of the ANDoperator is true (because1 = r) and the right operand is exactlythe precondition of the whole code segment,{n >= 0}. Therefore, the program hasbeenproven to be correct.
3.5.3.8 Evaluation
As statedpreviously,to define the semanticsof a complete programming lan-
{t’gt using the axiomaticmethod, there must be an axiom * rn inf.rence rule foreachstatementtypeinthelanguage.Defining axiomsorinferencerulesfor
BibliographiNc otes 767
sone of the statementsof programrninglanguageshasproven to be a difficult task.An obvious solution to this problem is to designthe languagewith the axiomaticlnethod in mind, so that only statementsfor which axionrsor infer- encerulescanbewritten areincluded.Unfortunately,suchalanguagewould necessarilyleaveout sorxeusefulandpowerfulparts.
Ariomatic semanticsis a powerful tool for researchinto program correct- nessproofs, and it providesan excellentframework in which to reasonabout programs,both during their constructionandlater.Its usefulnessin describing the meaning of programming languagesto languageusersand compiler writers is, however,highly lirnited.
Backus-NaurForm andcontext-freegrammarsareequivalentmetalanguages that are well suited for the task of describing the syntax of programming lan- guages.Not only are they concisedescriptivetools, but also the parsetrees that can be associatedwith their generativeactionsgive graphicalevidenceof the underlying syntacticstructures.Furthermore, they arenaturally relatedto recognition devicesfor the languagesthey generate,which leadsto the rela- tively easyconstructionof syntaxanalyzersfbr compilersfor theselanguages.
An attribute grammar is a descriptivefonnalism that can describeboth the syntaxand static semanticsof a language.Attribute grammarsare extensions to context-freegrammars.An attribute gramrnarconsistsof a grammar,a set of attributes,a set of attribute computation functions, and a set of predicates, which together describestaticsemanricsrules.
This chapterprovidesa brief introduction to three rnethodsof semantic description:operational,denotational,and axiomatic.Operational sernantics i s a r n e t h o d o f d e s c r i b i n gt h e m e a n i n g o f l a n g u a g ec o n s r r u c t si n t e r r n s o f t h e i r effectson an ideal rnachine.In denotationalsemantics,nrathematicalobjects areusedto representthe meaningsof languageconstructs.Languageentities areconvertedto thesemathernaticalobjectswith recursivefunctions.Axiornatic semanticsw, hich is basedon formal logic, wasdevisedasa tool for proving the correctnessof progralns.
Syntaxdescriptionusingcontext-freegranlmarsandBl{F arethoroughlydis- cussedin CleavelandandUzgalis(1976).
Researchin axiomatic semanticswas begun by Floyd (1967) and fur- ther developedby F{oare(1969).The sernanticsof a large part of Pascalwas describedby Floare and Wirth (1973)using this rnethod.The parts they did not completeinvolved functional sideeffectsand goto staternentsT. hese were found to be the most difficult to describe.
Chapter3
DescribinSg yntaxandSemantics
The techniqueof usingpreconditionsandpostconditionsduring the devel- opment of programsis described(and advocated)by Dijkstra (1976)and also discussedin detailin Gries(1981).
Good introductions to denotational semanticscan be found in Gordon (1979)andStoy(1977).Introductionsto allof thesemanticsdescriptionmethods discussedin this chapter can be found in Marcotty et al. (1976).Another good referencefor much of the chaptermaterialis Pagan(1981).The form of the deno- t a t i o n a l s e m a n t i cf u n c t i o n s i n t h i s c h a p t e r i s s i m i l a r t o t h a t f o u n d i n M e y e r ( 1 9 9 0 ) .