程序设计语言概念(Concepts-of-Programming-Languages)-英文-第10

Chapter3DescribingSyntaxandSemanticsCopyright©2023Addison-Wesley.Allrightsreserved.1-2Chapter3TopicsIntroductionTheGeneralProblemofDescribingSyntaxFormalMethodsofDescribingSyntaxAttributeGrammarsDescribingtheMeaningsofPrograms:DynamicSemanticsCopyright©2023Addison-Wesley.Allrightsreserved.1-3IntroductionSyntax:theformorstructureoftheexpressions,statements,andprogramunitsSemantics:themeaningoftheexpressions,statements,andprogramunitsSyntaxandsemanticsprovidealanguage’sdefinitionUsersofalanguagedefinitionOtherlanguagedesignersImplementersProgrammers(theusersofthelanguage)Copyright©2023Addison-Wesley.Allrightsreserved.1-4TheGeneralProblemofDescribingSyntax:TerminologyAsentenceisastringofcharactersoversomealphabetAlanguageisasetofsentencesAlexemeisthelowestlevelsyntacticunitofalanguage(e.g.,*,sum,begin)Atokenisacategoryoflexemes(e.g.,identifier)Copyright©2023Addison-Wesley.Allrightsreserved.1-5FormalDefinitionofLanguagesRecognizersArecognitiondevicereadsinputstringsoverthealphabetofthelanguageanddecideswhethertheinputstringsbelongtothelanguageExample:syntaxanalysispartofacompiler-DetaileddiscussionofsyntaxanalysisappearsinChapter4GeneratorsAdevicethatgeneratessentencesofalanguageOnecandetermineifthesyntaxofaparticularsentenceissyntacticallycorrectbycomparingittothestructureofthegeneratorCopyright©2023Addison-Wesley.Allrightsreserved.1-6BNFandContext-FreeGrammarsContext-FreeGrammarsDevelopedbyNoamChomskyinthemid-1950sLanguagegenerators,meanttodescribethesyntaxofnaturallanguagesDefineaclassoflanguagescalledcontext-freelanguagesBackus-NaurForm(1959)InventedbyJohnBackustodescribethesyntaxofAlgol58BNFisequivalenttocontext-freegrammarsCopyright©2023Addison-Wesley.Allrightsreserved.1-7BNFFundamentalsInBNF,abstractionsareusedtorepresentclassesofsyntacticstructures--theyactlikesyntacticvariables(alsocallednonterminalsymbols,orjustterminals)Terminalsarelexemesortokens

Arulehasaleft-handside(LHS),whichisanonterminal,andaright-handside(RHS),whichisastringofterminalsand/ornonterminalsBNFFundamentals(continued)NonterminalsareoftenenclosedinanglebracketsExamplesofBNFrules:

<ident_list>→identifier|identifier,<ident_list>

<if_stmt>→if<logic_expr>then<stmt>Grammar:afinitenon-emptysetofrulesAstartsymbolisaspecialelementofthenonterminalsofagrammarCopyright©2023Addison-Wesley.Allrightsreserved.1-8Copyright©2023Addison-Wesley.Allrightsreserved.1-9BNFRulesAnabstraction(ornonterminalsymbol)canhavemorethanoneRHS

<stmt>

<single_stmt>|begin<stmt_list>endCopyright©2023Addison-Wesley.Allrightsreserved.1-10DescribingListsSyntacticlistsaredescribedusingrecursion

<ident_list>

ident|ident,<ident_list>Aderivationisarepeatedapplicationofrules,startingwiththestartsymbolandendingwithasentence(allterminalsymbols)Copyright©2023Addison-Wesley.Allrightsreserved.1-11AnExampleGrammar <program>

<stmts><stmts>

<stmt>|<stmt>;<stmts><stmt>

<var>=<expr><var>

a|b|c|d<expr>

<term>+<term>|<term>-<term><term>

<var>|constCopyright©2023Addison-Wesley.Allrightsreserved.1-12AnExampleDerivation <program>=><stmts>=><stmt>=><var>=<expr>=>a=<expr>=>a=<term>+<term>=>a=<var>+<term>=>a=b+<term>=>a=b+constCopyright©2023Addison-Wesley.Allrightsreserved.1-13DerivationsEverystringofsymbolsinaderivationisasententialformAsentenceisasententialformthathasonlyterminalsymbolsAleftmostderivationisoneinwhichtheleftmostnonterminalineachsententialformistheonethatisexpandedAderivationmaybeneitherleftmostnorrightmostCopyright©2023Addison-Wesley.Allrightsreserved.1-14ParseTreeAhierarchicalrepresentationofaderivation

<program><stmts><stmt>consta<var>=<expr><var>b<term>+<term>Copyright©2023Addison-Wesley.Allrightsreserved.1-15AmbiguityinGrammarsAgrammarisambiguousifandonlyifitgeneratesasententialformthathastwoormoredistinctparsetreesCopyright©2023Addison-Wesley.Allrightsreserved.1-16AnAmbiguousExpressionGrammar<expr>

<expr><op><expr>|const<op>

/|-<expr><expr><expr><expr><expr><expr><expr><expr><expr><expr><op><op><op><op>constconstconstconstconstconst--//<op>Copyright©2023Addison-Wesley.Allrightsreserved.1-17AnUnambiguousExpressionGrammarIfweusetheparsetreetoindicateprecedencelevelsoftheoperators,wecannothaveambiguity<expr>

<expr>-<term>|<term><term>

<term>/const|const<expr><expr><term><term><term>constconstconst/-Copyright©2023Addison-Wesley.Allrightsreserved.1-18AssociativityofOperatorsOperatorassociativitycanalsobeindicatedbyagrammar<expr>-><expr>+<expr>|const(ambiguous)<expr>-><expr>+const|const(unambiguous)<expr><expr><expr><expr>constconstconst++Copyright©2023Addison-Wesley.Allrightsreserved.1-19ExtendedBNFOptionalpartsareplacedinbrackets[]

<proc_call>->ident[(<expr_list>)]AlternativepartsofRHSsareplacedinsideparenthesesandseparatedviaverticalbars

<term>→<term>

(+|-)constRepetitions(0ormore)areplacedinsidebraces{}

<ident>→letter{letter|digit}Copyright©2023Addison-Wesley.Allrightsreserved.1-20BNFandEBNFBNF

<expr>

<expr>+<term> |<expr>-<term> |<term><term>

<term>*<factor> |<term>/<factor>|<factor>EBNF

<expr>

<term>{(+|-)<term>}<term>

<factor>{(*|/)<factor>}Copyright©2023Addison-Wesley.Allrightsreserved.1-21RecentVariationsinEBNFAlternativeRHSsareputonseparatelinesUseofacoloninsteadof=>UseofoptforoptionalpartsUseofoneofforchoicesCopyright©2023Addison-Wesley.Allrightsreserved.1-22StaticSemanticsNothingtodowithmeaningContext-freegrammars(CFGs)cannotdescribeallofthesyntaxofprogramminglanguagesCategoriesofconstructsthataretrouble:-Context-free,butcumbersome(e.g.,typesofoperandsinexpressions)-Non-context-free(e.g.,variablesmustbedeclaredbeforetheyareused)Copyright©2023Addison-Wesley.Allrightsreserved.1-23AttributeGrammarsAttributegrammars(AGs)haveadditionstoCFGstocarrysomesemanticinfoonparsetreenodesPrimaryvalueofAGs:StaticsemanticsspecificationCompilerdesign(staticsemanticschecking)Copyright©2023Addison-Wesley.Allrightsreserved.1-24AttributeGrammars:DefinitionDef:Anattributegrammarisacontext-freegrammarG=(S,N,T,P)withthefollowingadditions:ForeachgrammarsymbolxthereisasetA(x)ofattributevaluesEachrulehasasetoffunctionsthatdefinecertainattributesofthenonterminalsintheruleEachrulehasa(possiblyempty)setofpredicatestocheckforattributeconsistencyCopyright©2023Addison-Wesley.Allrightsreserved.1-25AttributeGrammars:DefinitionLetX0

X1...XnbearuleFunctionsoftheformS(X0)=f(A(X1),...,

A(Xn))definesynthesizedattributesFunctionsoftheformI(Xj)=f(A(X0),...,A(Xn)),fori<=j<=n,defineinheritedattributesInitially,thereareintrinsicattributesontheleavesCopyright©2023Addison-Wesley.Allrightsreserved.1-26AttributeGrammars:AnExampleSyntax<assign>-><var>=<expr><expr>-><var>+<var>|<var><var>A|B|Cactual_type:synthesizedfor<var>and<expr>

expected_type:inheritedfor<expr>

Copyright©2023Addison-Wesley.Allrightsreserved.1-27AttributeGrammar(continued)Syntaxrule:<expr>

<var>[1]+<var>[2] Semanticrules: <expr>.actual_type

<var>[1].actual_typePredicate: <var>[1].actual_type==<var>[2].actual_type <expr>.expected_type==<expr>.actual_typeSyntaxrule:<var>

idSemanticrule: <var>.actual_type

lookup(<var>.string)Copyright©2023Addison-Wesley.Allrightsreserved.1-28AttributeGrammars(continued)Howareattributevaluescomputed?Ifallattributeswereinherited,thetreecouldbedecoratedintop-downorder.Ifallattributesweresynthesized,thetreecouldbedecoratedinbottom-uporder.Inmanycases,bothkindsofattributesareused,anditissomecombinationoftop-downandbottom-upthatmustbeused.Copyright©2023Addison-Wesley.Allrightsreserved.1-29AttributeGrammars(continued)<expr>.expected_type

inheritedfromparent<var>[1].actual_type

lookup(A)<var>[2].actual_type

lookup(B)<var>[1].actual_type=?<var>[2].actual_type<expr>.actual_type

<var>[1].actual_type<expr>.actual_type=?<expr>.expected_typeCopyright©2023Addison-Wesley.Allrightsreserved.1-30SemanticsThereisnosinglewidelyacceptablenotationorformalismfordescribingsemanticsSeveralneedsforamethodologyandnotationforsemantics:ProgrammersneedtoknowwhatstatementsmeanCompilerwritersmustknowexactlywhatlanguageconstructsdoCorrectnessproofswouldbepossibleCompilergeneratorswouldbepossibleDesignerscoulddetectambiguitiesandinconsistenciesOperationalSemantics

OperationalSemanticsDescribethemeaningofaprogrambyexecutingitsstatementsonamachine,eithersimulatedoractual.Thechangeinthestateofthemachine(memory,registers,etc.)definesthemeaningofthestatementTouseoperationalsemanticsforahigh-levellanguage,avirtualmachineisneededCopyright©2023Addison-Wesley.Allrightsreserved.1-31Copyright©2023Addison-Wesley.Allrightsreserved.1-32OperationalSemanticsAhardwarepureinterpreterwouldbetooexpensiveAsoftwarepureinterpreteralsohasproblemsThedetailedcharacteristicsoftheparticularcomputerwouldmakeactionsdifficulttounderstandSuchasemanticdefinitionwouldbemachine-dependentCopyright©2023Addison-Wesley.Allrightsreserved.1-33OperationalSemantics(continued)Abetteralternative:AcompletecomputersimulationTheprocess:Buildatranslator(translatessourcecodetothemachinecodeofanidealizedcomputer)BuildasimulatorfortheidealizedcomputerEvaluationofoperationalsemantics:Goodifusedinformally(languagemanuals,etc.)Extremelycomplexifusedformally(e.g.,VDL),itwasusedfordescribingsemanticsofPL/I.Copyright©2023Addison-Wesley.Allrightsreserved.1-34OperationalSemantics(continued)Usesofoperationalsemantics:-Languagemanualsandtextbooks-TeachingprogramminglanguagesTwodifferentlevelsofusesofoperationalsemantics:-Naturaloperationalsemantics-StructuraloperationalsemanticsEvaluation-Goodifusedinformally(languagemanuals,etc.)-Extremelycomplexifusedformally(e.g.,VDL)DenotationalSemanticsBasedonrecursivefunctiontheoryThemostabstractsemanticsdescriptionmethodOriginallydevelopedbyScottandStrachey(1970)Copyright©2023Addison-Wesley.Allrightsreserved.1-35DenotationalSemantics-continuedTheprocessofbuildingadenotationalspecificationforalanguage:

-DefineamathematicalobjectforeachlanguageentityDefineafunctionthatmapsinstancesofthelanguageentitiesontoinstancesofthecorrespondingmathematicalobjectsThemeaningoflanguageconstructsaredefinedbyonlythevaluesoftheprogram'svariablesCopyright©2023Addison-Wesley.Allrightsreserved.1-36DenotationalSemantics:programstateThestateofaprogramisthevaluesofallitscurrentvariabless={<i1,v1>,<i2,v2>,…,<in,vn>}LetVARMAPbeafunctionthat,whengivenavariablenameandastate,returnsthecurrentvalueofthevariable

VARMAP(ij,s)=vjCopyright©2023Addison-Wesley.Allrightsreserved.1-37DecimalNumbers<dec_num>

'0'|'1'|'2'|'3'|'4'|'5'|'6'|'7'|'8'|'9'|<dec_num>('0'|'1'|'2'|'3'|'4'|'5'|'6'|'7'|'8'|'9')Mdec('0')=0,Mdec('1')=1,…,Mdec('9')=9Mdec(<dec_num>'0')=10*Mdec(<dec_num>)Mdec(<dec_num>'1’)=10*Mdec(<dec_num>)+1…Mdec(<dec_num>'9')=10*Mdec(<dec_num>)+9Copyright©2023Addison-Wesley.Allrightsreserved.1-38ExpressionsMapexpressionsontoZ

{error}Weassumeexpressionsaredecimalnumbers,variables,orbinaryexpressionshavingonearithmeticoperatorandtwooperands,eachofwhichcanbeanexpressionCopyright©2023Addison-Wesley.Allrightsreserved.1-39ExpressionsMe(<expr>,s)

=case<expr>of<dec_num>=>Mdec(<dec_num>,s)<var>=>ifVARMAP(<var>,s)==undefthenerrorelseVARMAP(<var>,s)<binary_expr>=>if(Me(<binary_expr>.<left_expr>,s)==undefORMe(<binary_expr>.<right_expr>,s)=undef)thenerrorelseif(<binary_expr>.<operator>=='+'thenMe(<binary_expr>.<left_expr>,s)+Me(<binary_expr>.<right_expr>,s)elseMe(<binary_expr>.<left_expr>,s)*Me(<binary_expr>.<right_expr>,s)...Copyright©2023Addison-Wesley.Allrightsreserved.1-40AssignmentStatementsMapsstatesetstostatesetsU{error}Ma(x:=E,s)=ifMe(E,s)==errorthenerrorelses’= {<i1,v1’>,<i2,v2’>,...,<in,vn’>},whereforj=1,2,...,n,ifij==xthenvj’=Me(E,s)elsevj’=VARMAP(ij,s)Copyright©2023Addison-Wesley.Allrightsreserved.1-41LogicalPretestLoopsMapsstatesetstostatesetsU{error}

Ml(whileBdoL,s)=

ifMb(B,s)==undefthenerrorelseifMb(B,s)==falsethenselseifMsl(L,s)==errorthenerrorelseMl(whileBdoL,Msl(L,s))Copyright©2023Addison-Wesley.Allrightsreserved.1-42LoopMeaningThemeaningoftheloopisthevalueoftheprogramvariablesafterthestatementsintheloophavebeenexecutedtheprescribednumberoftimes,assumingtherehavebeennoerrorsInessence,theloophasbeenconvertedfromiterationtorecursion,wheretherecursivecontrolismathematicallydefinedbyotherrecursivestatemappingfunctions-Recursion,whencomparedtoiteration,iseasiertodescribewithmathematicalrigorCopyright©2023Addison-Wesley.Allrightsreserved.1-43EvaluationofDenotationalSemanticsCanbeusedtoprovethecorrectnessofprogramsProvidesarigorouswaytothinkaboutprogramsCanbeanaidtolanguagedesignHasbeenusedincompilergenerationsystemsBecauseofitscomplexity,itareoflittleusetolanguageusersCopyright©2023Addison-Wesley.Allrightsreserved.1-44Copyright©2023Addison-Wesley.Allrightsreserved.1-45AxiomaticSemanticsBasedonformallogic(predicatecalculus)Originalpurpose:formalprogramverificationAxiomsorinferencerulesaredefinedforeachstatementtypeinthelanguage(toallowtransformationsoflogicexpressionsintomoreformallogicexpressions)ThelogicexpressionsarecalledassertionsCopyright©2023Addison-Wesley.Allrightsreserved.1-46AxiomaticSemantics(continued)Anassertionbeforeastatement(aprecondition)statestherelationshipsandconstraintsamongvariablesthataretrueatthatpointinexecutionAnassertionfollowingastatementisapostconditionAweakestpreconditionistheleastrestrictivepreconditionthatwillguaranteethepostconditionCopyright©2023Addison-Wesley.Allrightsreserved.1-47AxiomaticSemanticsFormPre-,postform:{P}statement{Q}Anexamplea=b+1{a>1}Onepossibleprecondition:{b>10}Weakestprecondition:{b>0}Copyright©2023Addison-Wesley.Allrightsreserved.1-48ProgramProofProcessThepostconditionfortheentireprogramisthedesiredresultWorkbackthroughtheprogramtothefirststatement.Ifthepreconditiononthefirststatementisthesameastheprogramspecification,theprogramiscorrect.Copyright©2023Addison-Wesley.Allrightsreserved.1-49AxiomaticSemantics:AssignmentAnaxiomforassignmentstatements

(x=E):{Qx->E}x=E{Q}TheRuleofConsequence:Copyright©2023Addison-Wesley.Allrightsreserved.1-50AxiomaticSemantics:SequencesAninferenceruleforsequencesoftheformS1;S2 {P1}S1{P2} {P2}S2{P3}AxiomaticSemantics:SelectionAninferencerulesforselection-ifBthenS1elseS2{BandP}S1{Q},{(notB)andP}S2{Q}