; TeX output 1997.12.30:1234soX 1 ecrm1000IdonotwanttheLaT*eX-commandsintheindexAThisisbGorrowedfromthe IstandardU packqagedoGc.dtxXIU alsoexcludethecommandsusedtogeneratetheindex(1*soUsGGecrm1728ThehN9>GGectt1728semantic-pacykage!", cmsy1086 ecrm1200PweterlMllerNeergaard]D7` ectt1200turtle@diku.dkhttp://www.diku.dk/students/turtle%vVjDecemwbSerl30,1997-bލ"!u ecbx0900Abstract_ o$ . ecrm0900ThispacbQolsmڬ3`I2WInferenceRulesI43T ranslationDiagrams+C5`4SomeNotesabQouttheFiles t7̍ILcKFȜI'qL ectt1000semanticisaLfAzTUY&E9X2 b> cmmi10"*⋹-packqageeasy-Iing!zthewritingofnotationofseman-Itics!andcompilers.׀T*ouseittheIleDsemantic.styshouldbGeplaced,Iso'thatLfAzTUY&E9Xcanndit. InyourIdoGcument!preambleyoushouldincludeI\usepackage{semantic}XInVthefollowingIwilldescribGetheIuse?ofthedierentpartsofOsemantic:IsymbGols,inferenceWyrulesandtransla-Ition diagrams. Thereisalsoasec-Ition3describingtheinstallationandgiv-IingFjashortintroGductiontothetwolesIsemantic.dtxU andsemantic.ins.XLikedQmostothercomputer-programs,II&have&Pprovidedthispackqagewithsev-FȜeralLbugs,Winsuenciesandinconsis-tencies. WWTheseshouldbGeregardedasfeaturesofthepackqage. KT*oincreasethe excitementofusingthepackqagethese\featuresappGearineventomeunpredictableYplaces.,Iftheyhoweverget`toannoyingandseriouslyreduceyourssatisfactionwithsemanticthenplease02notifyme.Y*oucouldalsodropmejanote,rifyouwouldliketobGein-formed,U whenIupGdatesemantic.7dIncontinuationofthisIMwillesp-ciallydrawyourattentiontotwotrou-blesomenareas:MthesyntaxandthedoGc-umentation. ˴Whenlayingdownthesyntax"I"Xhavetriedtosatisfytocon-I8щffr @ -:q% cmsy6K"ecrm0800This(lehasvÒersion1.22cmmi8 andisdated1996/01/31(2qsoItrary2considerations:+atousethewell- IknownLfAzTUY&E9X-syntaxandtogiveasyn-Itax,thatiseasytypGedandread.2ThisIhashleadtosomecompromises,whichImostgSprobaplysatisfyneither. AndIbGeing~daneandthereforenotnativeIenglish-spGeakingitisevenharderthanInormalktoexpressclearlyinthedoGcu-Imentation,whatKmyintentionwas.7Anyfeedback6wouldthereforebGegreatlyap- preciated.Alastand%compulsarypartisaspGecialthankstoJesperGrothLhr,whoKhasbGeen -testerofseveralversionsleadingx:tomanyimprovements.andKai'Neegrd,1whoreadandcommentedtheU doGcumentation.#~I1`Symcbpols~IT*osuppGortwritingdenotationalsemanticsthecommands\compand\eval&az(qL ectt0900\eval &az\comp IareUprovidedtodescribGetheevqaluationofprogramsrespectivelyexpressions.ITheyVMhavethesamesyntax:s\comp{ !", cmsy10h)HЃ ecti1000c}/ommandwi23c}{henvir}/onmentɸi>N},whichyieldsICW[[h*qL ecit1000commandVi.A(]]ahenvir}/onmentɸiy.If\1youneedtodescribGemorethanonekindofevqal-Iuations,e.g.bGothE!andE^ O!cmsy7}ܹ,youcanprovideanoptionalargumentimmediatelyIafter\comprespGectively\eval.Iand=>, whichisavqailableinbGothmathematicsandtext.ZBytypinga*or+afterI->U or=>yougetthestarred*handplussedversions:q!^,)^,!^ٓRcmr7+ and)^+.XInT6theinferencesymbols-environmentT6thevqastma0jorityofLfAzTUY&E9X-commandsIworkṡnormally*.׶ItishowevernotpGossibletoensure,athatthesymbGols|,a-and(3ޠsoI=works100%likeoutsidetheenvironment^1|2,Գandforinstance\cline{::: -:::} IcannotEbGeusedinthisenvironmentE(ithoweverEworksifitispartofacommandIdenedU outsideotheenvironment).!֍I2`InferenceG\Rules~IInferenceU ruleslike\inference$𨍍IIt(1)U :荑oR`E )2V eccc1000TrZue+`s >0)^0 ;v ^0Q`while?E9dosF<)^00ghwfe (׎V-while?$E$do$s$=>\rho''}عIt(2)U :<#c`E )Fhalseg@wfeu (׍`while?E9dosF<)!2and2fe (׎ 8TUK cmsy8!-:wqAacmr61$p2fe (׎0,TU!-:wq2(LU areU easilysetusing\inference.qThesyntaxisb\inference[5 cmsy9hnameiJ]{hline1*i\\\N45" cmmi9:::=B\\Nhline;cmmi6n7i}{hc$onclusion.i1}Iwhere9n0soyoualsocantypGeaxioms.hpEachlineconsitsofpremisessepGeratedIbyU &:bhpr$emise1*i*~&::: ʦ&hpr$emisemiINotethatmcanalsobGezerowhichisusedwhentypingaxioms.TheoptionalInameU issettotherightoftheinference.XThe4rulesissetsothelineushwiththecenterofsmalllettersinthesur-Iroundingvtext.Inthiswayvsecondaryconditionsornames(liketherstexampleIabGove)canbewritteninthesurroundingtext.[ItalsomakesitpossibletosettheIrulesU inatablelikeshownherewiththelastexample:jwR^T*ransitiveU (1):荒p,MU !^p^09,M^0 ;p^09,M^0#Y!U p^00r,M^00nwfeQp (׍Op,MU !^p^00r,M^0044^T*ransitiveU (2):n2feF4E (׍p,MU !^p,M\vXAnU inferencerulecanunproblematiclybGenestedwithinanother,like:.Q<#`n 9)feF4E (׍p,MU !^p,M=.xL!-:wq2p,MU !^p^09,M^0fwfe (׍;p,MU !^p^09,M^0byxL!-:wq1:6p^09,M'U !p^00r,M^00_ )wfe% (׍qEp,MU !^p^00r,M^00 {TU!-:wq1XThe"appGearanceoftheinferencesrulescanpartlybecontrolledbythefollowing$n\setpremisesend\setpremisesspace \setnamespaceIlengths:ȍ<#"=!premisesend Íu cmex10z31Z}|31Z{Թpremise"=premisesSpace Íz31 }|31 {+Rpremisewfevh (׍65conclusion( pnamespace Í,焫z31 }|31 {M̟TUname\ PgThelengthsarechangedusingthethreecommands\setnamespace{hlengthUi"Yx},I\setpremisesend{hlengthUi"Yx}[og\setpremisesspace{hlengthUi}.hlengthUi.:!canbGeIgiven inbGothabsoluteunitslikeptandcmandinrelativeunitslikeemandex.IThe defaultvqaluesare:1 33133&fes2bemforpremisesspace, o33o3&fes4 emforpremisesendog A1A&fes2 pemI 1ffr E !i-:07Lecrm06001KInside6theenÒvironment61&ectt0800|,N-and=aredenedasmacros.0Thesemacrosexamensthenext cÒharacter3andifitis-or=,KG>and>resp} ecsl0900expressionistobAeIev|yaluatedinaen#3#4\predicateend{%kr$#1N\vdash$\texttt{#2}$\stackrel{#3}{\Rightarrow}_S#4$}IThentheinference(bAorro]vY) JSs-=0D`s>v7{q 0ncmsy50Y) JSs-=00֟Ife՟ ؝r9DӍ`NTl(s)>v7{q0Y) JSs-=00:saeTlRL$can$bAeaccomplishedb&examened,Xeandifitis\end,semanticconcludesthatthepremisedo{v}s'&D|-$s$=>{v'}s''} kr{DN|-Tl($s$)=>{v'}s''}>IPleasenotethattheinferencesymbols-en,himplementationDplanguageiky}b\interpreter{hsour$cei ,himplemenationAlanguageih}b\compiler{hsour$cei ,hmachinei)d,htar$getٺi}b\machine{hmachinei)d}ITheZargumentscanbGeaeitherastringdescribingthelanguage(pleasedonotuse Ia3=macroatthestartofthestring)oroneofthefourcommands. However3=theIcombinations)givingnomeaningareexcludedlikeimplementingainterpreteronIaU program,whichyieldtheerrormessage:}fP!NPackagesemanticError:Aprogramcannotbeatthebottom.u`SeeNthesemanticpackagedocumentationforexplanation.u`Type rHNforimmediatehelp.zq...}XWhenyouareusingacommandasanargumentsemanticwillcopythelan-IguagefromthenestedcommandandautomaticlyplacethetwoguresinpropGor-Ition toeachother.YdInthiswaybigtranslationdiagramscaneasilybGedrawn.YdTheIhole&constructionshouldbGeplacedusingaf\putcommand,'wherether}/eferenceIp}/oint\isithecenterofthebGottomofthegurecorrespondingtotheoutermostIcommand.TI+/think+gafewexamples(withthereferencepGointmarkedby+gr +g)willIclarifyU someofthesepGoint:S%32fd32fdLΟ(feLΟ(fe*S@TL'r32fdLΟfeLΟfe32LLΟ Ήfe32LLΟ Ήfe32fe*P32fdP32fd632fd"32fdLΟfeTLΟfe"LΟfe6LΟfe՚'!*CT32fdhLΟfeTLΟfe32TLήTLΟ Ήfe32hLhLΟ Ήfe^32fe[*P[*MB*M"32fd"T&T0,)*M)*M*CrIisU obtainedbythecommands}b\begin{picture}(220,75)(0,-35) fP\put(10,0){\interpreter{S,L'}}fP\put(110,0){\program{P,\compiler{C,\machine{M},\program{P,M}}}}b\end{picture}(6EsoINotejfromthesecondexample,oJthatwhen\compilerisusedasimplementation Ilanguage-argument3itisbyconventionattributedtotherightofthegure. mItIiséalsoworthmentioningthatthereisnostrictdemandonwhichcommandyouIshoulduchoGoseastheoutermost,ie.thesecondexamplecouldalsobewritten(withIaU changeinthecoGordinatesto\putduetothenewreferencepoint)asb\put(160,-20){\compiler{\program{P,C},\machine{M},\program{P,M}}}Istarting'ointhemiddleinsteadofusingaleft-to-right-approachin'factitwillIoften6bGeeasiesttostartinthemiddleasthisgivestheleastnestingmakingitIeasierU toendtheargumentsattherightpGosition.XThoughusingnestingitisinsomerarecasesadequatetousedierentlanguageIsymbGols̔onthetwosidesofthelineoftouch.CE.g.whendescribingbGootstrappringItheVpGoorU-codeimplementationcanbesymbolizedbyAU^,)KwhichstillisexecutedIonRaU-machine.iThiscanbGedonebyprovidingthesymbGol-commandwithanIoptionaljargumentimmediatelyafterthecommandname.s^InthiswaythebGoot-Istrapping:Z񨍍32fdP32fd32fd׀32fdLΟfe LΟfeLΟfeLΟfe՚܀!32fdP32fd32fd32fdLΟfeLΟfeLΟfeLΟfe՚!@TML*U@TML@TML32fdP32fd32fd 32fdLΟfe;LΟfe LΟfeLΟfe՚!32fdP32fd32fd׀32fdLΟfe LΟfeLΟfeLΟfe՚܀!@TML*U@TML@TML32fdP32fdO32fd;32fdLΟfemLΟfe;LΟfeOLΟfe՚@!'@TML[*UB*U)*U 32fd T T*U, *U^,*U^׀32fd׀TۀT*U,ۀ*U^IisU typGedb\compiler{\compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{ y\compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{ML,U,U}}}XWhencalculatingthedimensionsofthepicture-environmentitisgoGodtoIknowU thedimensionsofthegures,whichisgiveninunitsof\unitlength:$8Icompiler:q80*40Iinterpreter:q20*40machine:q20*17.1program:q20*40!֍I4`SomeG\NotesabpouttheFiles~Isemanticisdistributedinthetwolessemantic.dtxandsemantic.ins.Isemantic.dtxꐹisthemostimpGortantasitcontainsalltheessentialsusersguide,IcoGdeanddocumentationofthecodewhilesemantic.insisusedonlytoguideI@6 ecss1000@doGcstripU ingeneratingsemantic.styfromsemantic.dtx.XT*o2get[[and]]usedin\comp,6\evaland\exesemantictriestoloadtheIpackqage@bbGoldwrittenby23A.|Jeffrey.ZIfthisisnotinstalledonyoursystem,theIsymbGolsyaresimulatedbydrawingtogethertosharps.ߡIywillhoweverrecommendIthatU youget@bbGoldfromyournearestCT*AN-archive.XInadditiontotheusersguideyoukqanalsogetthefullydoGcumentedcoGde.@Y*ouIwillRWhoweveronlyneedthisifyouwillsneakinhowIRVimplementedthemacrosorIchangeM somepartofthepackqage.nY*oushouldstartbyeditingsemantic.dtxandImakeU thetwolines(nearline1545)(7Tsob\OnlyDescription8%NMaketoacommenttogetthedocumentation b\DisableCrossrefs+%NRemovecommentiftheindexisreadyorifIinU toacommentandremove%fromthebGeginingofthetwonextlines:b%\CodelineIndexW%NMakeaindexofthecommandusageb%\RecordChangesW%NMakethechangeshistoryIThenyyoushouldrunLfAzTUY&E9Xtwiceontheeditedletogetacorrecttableof Icontents.qThenU yougeneratetheindexandchangehistoryusingmakeindex:bmakeindexN-sgind.istsemanticbmakeindexN-sgglo.ist-osemantic.glssemantic.gloIAndU atlastthedoGcumentationisreadyforprintingafteranotherrunofLfAzTUY&E9X. Xsemantic.dtx,isdesignedtobGeusedwith@docand@docstrip. ItthereforeIconsistsofthepackqagecoGdebutmostofallofalotofcommentscontaningItheusersguideandthedoGcumentationofthecode.jUWhenTUY&E9XisrunnedonIsemantic.ins,@doGcisusedtoremoveallthesecommentsandtheresultiswrittenIin:Uthepackqage-lesemantic.sty.!WhenyoumaketheusersguidebyrunningILfAzTUY&E9Xrionsemantic.dtx,yLfATUY&E9XrstskipsabGout650linesofcomments(contain-Iing:thesourceoftheusersguide)bGeforeitgetstothelinesnormallymakinguptheIpackqage-le.IThenfollows850linesofintermixedcommentsandcoGdedeningtheIcommands>inthepackqage.At>lastLfAzTUY&E9Xcomestoaline\documentclass{ltxdoc}I(@ltxdoGc̹isLfAzTUY&E9X2")m'sstandardclassfordocumenting).WAfteracoupleofpack-IagesloadingOandsomecommanddenitionitreaches\begin{document}andI\docinput{semantic.dtx}.7ThismakesLfAzTUY&E9X'sreadingoversemantic.dtxonceImoreU butthistimeskippingthe%-charsintherstcolumn. ?OL_7qqecrm2074cIA!",q cmsy10A aAtnlastthebGorrowingformalstu:Y*ouaencouragedtocopy*,Huse,delete]tetc.thepackqage(semantic.dtxandsemantic.ins)asmuchasyourheartIdesiresaslongasyoupassitonincomplete(ie.notonlysemantic.sty).FY*ouIare?welcometosneakinthecoGdeandgetinspiration(A littlewarninghowever:Ithis2ismyrstbunchofrealTUY&E9X-coGde!).fY*oushouldjustremembGer:2c`K G19951996IP} ecsl09009+:ecrm05008*= manfnt7qqecrm20745 cmsy945" cmmi92V eccc10001&ectt080007Lecrm0600,Cscmtt8+GGectt1728UsGGecrm1728 1 ecrm1000 !", cmsy10 O!cmsy7 0ncmsy5 b> cmmi10K`y cmr10ٓRcmr7< lcircle10O line10u cmex10r