; TeX output 1996.03.05:1400y?rDtGGcmr17Tqypsesetting7tBSIVDMwithLdKGXQ cmr12AT[-E;gX'dMarioWVolczkroDept.8ofComputerScienceTheUnivrersityPMancrhesterM139PLCU.K.kh2߆T cmtt12mario@cs.man.ac.uk,...!uknet!man.cs!mario]fj?09June1992 "VVersion3.01+č>4Nff cmbx12Contents>5"V cmbx101MOv9erview2>2MUsingT63MT9ypQesettingTformulas١95MK`y cmr103.1dTheUUformulaEnvironment[㍍......................6M3.2dConstructionsj=.............................7d3.2.1TheUUformboxEnvironment?K.................9M3.3dOtherUUGeneralPointsUUabGoutF*ormulasts...............10>4MT9ypQesettingTdatatypQes=11>5MHo9wTtoTypQesetF unctions13M5.1dInvqariants#1...............................14>6MHo9wTtoTypQesetOperations14>7MProQofs16>8MCustomisingTtheSt9yleφ17M8.1dChangingUUtheSpacing........................17M8.2dControllingUULineandParagraphBreaks..............18M8.3dUnforeseenUUChangesM.........................19>9MInstallingTthevdm lesШ]20>10MNewTvdmcommands(in9troQducedfortheA- cmcsc10Absiversion):7{201*y?>11MAc9knowledgementsW22!č>1VLOverview>ThisbdoGcumentdescribesastyleoption,%vdm,forbusewithL5ffٓRcmr7A͉TU>'ExX. Thepurpose >ofUUvdmistomakethetypGesettingofVDMspeci cationseasy*.qOthergoalsare:M !", cmsy10WT*oenableusersofvdmtocommunicatetheirspGeci cationstoothers,$pos-Wsiblyinavqarietyofconcretesyntaxes,*withouthavingtochangetheirWsourceUU lesMWT*oenableauserofvdmtoconcentrateonhis^1.spGeci cations,andignoreWthedetailedlayoutasmuchaspGossible.rAsidee ectofthisisthattheWe ortprequiredtoimproveplayoutisconcentratedinoneplace,wKwithintheWvdmUUmacros.>(ThisOversionofthevdmstyleoptionusestheAbsiconcretesyntax.AnydoGcument>preparedusingearlierversionsisstillaccepted,,butthewayitistypGesetwill>matchmorecloselytheAbsistandardconcretesyntax.HTherearealsoafew>additionalcommands(summarisedattheend).6Notethatthisis!': cmti10notacomplete>styleUU leforallofAbsivdm.)MButenoughevqangelising.HkLet'sgettothetherealmeat.ThisdoGcumentis>brokenUUupintothefollowingsections:MWGeneralUUpGointsaboutusingvdmMWTypGesettingUUformulasMWHowUUtotypGesetdatatypGesMWHowUUtotypGesetfunctionsMWHowUUtotypGesetoperationsMWHowUUtotypGesetproofsMWHowUUtotailor/extendthesystemforyourownapplication.>Y*ou2shouldde nitelyreadthe rsttwo2sections|thenyou'llknowroughlywhat>you'reinfor,andwhetheryouwanttocontinue.5Theremainingsectionscan>bGeUUreadasandwhenyouneedthem.AdBo cmr9BIndk9eepingwiththebAesttraditionsofTuAEXdocumen9tation,xparagraphsthatcontain >material9thatisnotessen9tialfornovices,butvitalifyouwanttoparameteriseor>extendTthesystem,areinsmallert9ypAe,likethisone.MJust6togiveapreliminaryexample,ohereissomeoutputfromvdm,andthe >correspGondingUUinput:>X-ffv J= "5-:#Aacmr61L"|{Ycmr8ReadX`his/her'forevÎeryo cmmi10;omc)䍑 &K cmsy84 ݉\)@ ifptrs9=fgthenZomelseletPgones=fph2ptrs9jRCs(omc(p))=1ginletPomc^ O!cmsy70Y=gone;#n:Tq lasy10 #omcinletPomc^00=omc^0|y8fph7!(omc^0(p);RC;7!RCȸ81)*n4jph2ptrs 8gone[ginde}'c(u cmex10SUWfelemsũBODY6(omc(p))cFpjph2gone[g;omc^00ղ)jGjDESTROYPTR[(VObjr];Ptr:Oop)oxkext~OwrJOM:OopT΍ћm2h &!L?Basic*Np*TObje}'ct'kpre:ptrڥ2elems BODY6(omc(objr]))kpQostLom{=s(G4#omKy8fobj9u7!(omc(objr]);BODYN7!BODY)8fptrg)g>\begin{vdm} >\begin{fn}{dec}{ptrs,om}?\\>\signature{]\setof{Oop}?\x\mapof{Oop}{Object}\to\mapof{Oop}{Object}>}>\If?ptrs=\emptyset>\Then?om>\Else\Let?gone=\set{p\inptrs|RC(om(p))=1}\Ing\Let?om'=gone\dsubom\Ing\Let?om''=om'\owr\map{p?\mapsto\chg{om'(p)}{RC}{RC\minus1}|?p\inptrs\diffgone}\Ingdec(\Union\set{\elems{BODY(om(p))}?|p\ingone},om'')>\Fi>\end{fn}>\begin{op}[DESTROYPTR]>\args{?Obj,Ptr:Oop}>\ext{?\WrOM:\mapof{Oop}{Basic_Object}}>\pre{?ptr\in \elems{BODY(om(obj))}}>\post{?om=~{om}\owr\map{obj\mapsto\chg{om(obj)}{BODY}{BODY?\diff\set{ptr}}}}>\end{op}>\end{vdm}!č>2VLUsingffC߆Tff cmtt12Cvdm|GeneralPoints>T*oUUgetatvdm,includevdmasadoGcumentstyleoption,e.g.:3y?g\documentstyle[12pt,vdm]{report}~AJvBT:oJvthebAestofm9yknowledge,WtheuseofDߤN cmtt9DvdmBdoAesnotcon ictwithanyoftheother >doAcumen9tystyles,exceptwhensomethinghasbAeenrede ned.Anattemptwillbemade>toTdoAcumen9tallsuchrede nitions.>OncevdmhasbGeenincluded,iyoucanthenusethevdmenvironment.[OF*orexam- >ple,~m?\begin{vdm}|....m?\end{vdm}>All"spGeci cationmaterialshouldbeplacedwithinthevdmenvironment.ڣThe>usepofvdmonlya ectstextwithinthevdmenvironment,7exceptpforthefollowing>globalUUchanges(whichareonlyrelevqantwheninmathordisplaymathmoGde):J81.WThe`mathcoGdesofa...z`andA...Z`have`beenchanged.6InplainEnglish,WthismeansthatwhenyoutypGelettersinmathmodetheinter-letterspac-Wing]smaybGedi erentthanitwouldbGehadyounotincludedvdmasanWoption.^2This0isbGecauseL5ffA͉TU>'ExXmathmodeisusuallytunedforsinglelet-WterCidenti ers,GOasusedbymathematiciansformillenia.kHowever,GOyouandWIDbGothlknowthatmostmeaningfulidenti ershavemorethanoneletterWinthem,sovdmprovidesbGetterspacingforthem.'oAsanexample,ifyouWtypGea$identifier$,dL5ffA͉TU>'ExXwouldnormallyprintidentifierG,dwhereastheWuseUUofvdmwillyieldidenti er.WBIf8y9oureallywanttousethe`normal'inter-letterspacing,BsayD\defaultMathcodesRa.B.@J82.WUnderscoreԓgivesyouanunderscore,bandnotasubscript.IfyouwantaWsubscriptuse@,1e.g.,x0istypGedx@0,oruseTU>'ExX's\sb!macro.An@isWstilleRan@whennotinmathmoGde.Occasionallyyoumay ndthatan@WinmathmoGdedo}'esnP'tܲgiveyouasubscript(particularlywhenusedwithWmovingB+arguments).8JShouldthishappGen,}ayouareadvisedtouseTU>'ExX'sW\sbjNmacro,UUe.g.,$x\sb{0}$.YTpBIfTny9oudon'tuseunderscoresmuch,{andyouwanttouseD_Bforsubscripts,{youcan Wsa9yHD\underscoreonB.B(andHD\underscoreoffGbBtoHmakeitreverttoitsusualmeaningWinTDvdmB).@J83.W-쮲typGesetsahyphen,andnotaminussign.7VDMspGeci cationsusually Wcontainalotmorelong}-identi ersthansubtractions, soonthewholethisWalteration.jshouldsave.je ort.dIfyoureallywanttodoasinglesubtractionWsign,NuseP\minus# >. IfPyou ndthedefaultisinappropriate,youcanrevertWto 3theoriginalbGehaviourusing\mathminus8;\textminus=%istheinverse.WExample:qa-b?\ne\mathminusa-bUUgivesac-bh6=aC8b.>Ulffv J= "5-:2LThisqisnotthecaseifyÎouareusingPSL#A TAEMX,asthatdo'ExXandL5ffA͉TU>'EX~hasalwaysbGeenatie(aspacebetweenwordsatwhich x⍑Wthe}lineisneverbroken). W*ellinvdmitisn't.~xwillgiveyouas(U`#mx. F*orqWlongnqidenti ers,tsuchas8䍍(X㐸Flong4u,tsay~{long}.NotethatthisonlyappliesinWmathmo}'de;elsewherea~isstillatie.J86.WInmathmoGde,&thedoublequotecharacter''isactuallyamacro.GPlacingWtextebGetweenpairsofdoublequotescausesthattexttobGesetinthenormalWtextUUfont.qF*orexample,$x="a?variable"$givesyoux\=avqariable-N;.ZBIfy9ouwanttochangethefontusedfortextplacedbAetweenquotes,׿rede ne WthecommandD\mathTextFont@7B.[@Bydefaultitisde nedtobAeD\rm+B(D\mathrm$BforWtheTNewF:on9tSelectionScheme).J87.WTheEfollowingmacroshavebGeenalteredinanon-trivialway:R\forall+, W\existsB(seeUUlater).@\BWhen\y9outypAesetsomeVDMthe;Hleftmarginb9yanamountequaltoD\parindent2{$B,DtheindentationatthebAeginning>ofTeac9hparagraph.pIfyouwanttochangethis,changethev|ralueofD\VDMindent2U0B,e.g.:c̰D\setlength{\VDMindent}{0cm}>Bwillmak9eyourspAecscomeout ushleft.Thisdocumen9thasbeent9ypesetwith >D\VDMindentpU0BequalTto38F cmsy9FD\parindent1NB.MSimilarly:,therigh9thandmarginiscontrolledbyaparametercalledD\VDMrindent6B.>ByTdefaultitisalsosettoD\parindent2U0B.BY:oucanha9veaparticularlinespacinginforcewithintheDvdmBen9vironment.@The>spacing(,withinaDvdmBen9vironment(,isdictatedb9ytheD\VDMbaselineskipSBcommand.>NotehthatthisisHj cmti9Hnot/Balength,Jbutacommand.!BydefaultitexpandstoD\baselineskip>Bsothatthelinespacingisthatofthesurroundingtext,ƛwhatev9ersizethatmaybAe.T:o>mak9eTitsmaller,youmaywanttosayPXD\renewcommand{\VDMbaselineskip}{0.8\baselineskip}>BforTexample.&č>3VLTyps3esettingffformulas>MostofthetextyouenterwithinvdmenvironmentswillbGeinTU>'ExX'smathmode,>but*VDM* doGesitsbesttoconcealthisfactfromyou,2sothatyoushouldrarely*,>ifUever,havetotypGeadollarsign.s!However,severalnewfeatureshavebGeen51y?>provided forthetypGesettingoflogicalformulas.YFirstly*,dopGeratorswithsensible >names"havebGeenprovided: puse\Iff",U\Implies.U,U\Or,U\Andxand\NotEHforthe>opGerators,;);_;^and:.!(T*oretaincompatibilitywithapreviousversion,>\iffR,UU\implies-U=,UU\andandUU\negareUUstillprovided,but\orjisnot.)MAma8jorchangehascomeintheareaofquanti edexpressions.nInVDM,>they haveverywell-de nedforms,sotheL5ffA͉TU>'ExXsequences\forall)and\exists>haveUUbGeenre-de nedtotakearguments.qF*orexample,togetk9x\2S8p(x4D)썑>typGečg\exists{x?\inS}{p(x)}>Notetheseparatingdotthatwasputinautomatically*.ROIfyouwantoneofthese >dotsUUbyitself,youcanhaveonebysaying\suchthat2:.MInUUaddition,twoUUnewquanti ers,\unique+jand\nexists-U=,havebGeenadded:cfd`9!x\2S۸8p(x4D)*` msbm10@glx\2SԾ8p(x4D)ۀ\unique{x?\inS}{p(x)}ۀ\nexists{x?\inS}{p(x)}MAdditionally*,4toԹcomplement\unique),thereis\uniqueval9T.Thisisthe>so-calledUU\iota-function"thatreturnstheuniquevqalue,ifthereisone:꫍㍍fd`x\2SИ8p(x4D)ۀ\uniqueval{x?\inS}{p(x)}8㍑ABIfy9ouwanttousetheoldversionsofD\forall'PBandD\existsBtheyarea9v|railableunder >theTpseudon9ymsofD\Forall'=BandD\Exists$(nB.MIfFyou ndthatthebGodyFofthequanti edexpressionistoGolongto t>comfortablyPonaline,Qthereare*-formsoftheabGovePcommandsthatplacethe>bGody4ofthequanti edexpressiononanewline,slightlyindented.OF*orexample,k9x\2Sk]p(x4D)8^q}(x)_:p(x)h)r(x)8^S2}(x)O>canUUbGeobtainedwithč]\exists*{x?\inS}{p(x)\Andq(x)\Or\Notp(x)\Implies?r(x)\AndS(x)}MIf"youneed\Strachey"brackets,V0e.g.,M[UX[e[]],V0place"thematerialtoappGear>withinUUthebracketsUUwithin\term{?...},UUthus:q$M\term{e}$.MAspGecial@controlsequence,Fz\const#h,Fzisavqailableforconstants.T*oget,Fzfor>example,UUAYesgŸjANoE,UUtypGe\const{Yes}|\const{No}.@BIfy9oudon'tlikethefontthatconstantsaresetin,ɭyoucanchangethembyrede ning >theTcommandD\constantFont@B.pBydefaultitexpandstoD\scBB. >LN cmbx12L3.1\TheformulaLEnvironmentuT>Occasionallyyoumaywantaformulaonitsown,bGetweenparagraphsoftext,>say*..Normally,theprovidedenvironmentsandcommandssuce,butsometimes6?y?>theyUdon't.IfyouneedanoGddequationtostandonitsown,usetheformula >environment:b\begin{formula}bx?=10b\Or \forall{i?\in\Nat}{i\ne10\Impliesi\nex}b\end{formula}>TheJformulaenvironmentJissimilartodisplayedJmathmoGde,Lexcept:llformulas>are indentedby\VDMindent8,:not\mathindent=޲,andlinebreakscanbGemade>using8\\2.oAlso,pwithin8theformulaenvironment8everythingappGears ushleft,>asUUoppGosedtobeingcentred.6>L3.2\ConstructionsuT>A\particularly] nicefeatureofvdmisthatyoucantypGesetmulti-lineconstructions>suchIasthoseintheearlierexamplewithouthavingtoworryabGout,'say*,liningIup>\thens"sand\elses"with\ifs".&Inthefollowingde nitions,wheneveryouseethe>termDhmath-moGde-expressioni,zyoushouldtypGeanexpressionasifinmathmode,>but youneedn'tputdollarsignsin.AlloftheconstructionsdescribGedbelow>can}bGeusedwhereahmath-mode-expressioniisrequired.Eachconstructionis>shownbyexample;theoutputontheleftresultsfromtheinputontheright.>AlsoInotethateachmacronamebGeginswithanupper-caseletter.NTU>'ExXand>L5ffA͉TU>'ExXdjfrequentlyusethelower-casevqariantsforcompletelyunrelatedthings.>Naturally*,UUchaoswillensueifyoumixthenamesup.MTypGesettinganif4isdoneusing\Ifhmath-mode-expressioni\Then:Ըhmath->moGde-expressioni\ElseFhmath-mode-expressioni\Fi.,x䍍㍍fd`ifk 1x\2S`thenz,Sk]8x`elsevfgۀ\If?x\inSۀ\Then?S\diffxۀ\Else?\emptysetۀ\Fiۀ\end{verbatim}+ꪍMIfUUyounest\IfLsthenyoumustencloseinner\IfLswithinbraces:=꫍㍍fd`iflٵ:::`thenz,if{:::z,thenv:::z,elseҵ:::$`elseۀ\If?...ۀ\Then{\If?...\Then?...\Else?...\Fiۀ}\Elseۀ\Fi=ꪍMY*oujdareadvisedtoplacetheextrabracesexactlyasabGove;tdon'tjdletextra->neousUUspacesinterveneUUbGetweenthekeywordsandthebraces.7Ly?MThe3\If'macro3alwaysstartsanewlineforthethenandelseLparts.fIfyou >wantUUTU>'ExXtotrytochoGoselinebreaks,use\SIfinstead:& ㍍fd`ifk 1a{=bthen:cWβ=dAi+8e`elsevph=q]+8rLm+s +t++uۀ\SIf?a=bۀ\Then?c=d+eۀ\Else?p=q+r+s+t+uۀ\Fi&x㍍MletY...inwA6constructionsfaredoneinasimilarway: C\Let%ʸhmath-moGde->expressioni\In3hmath-moGde-expressioni,and\SLet# hmath-mode-expressioni>\InQLhmath-moGde-expressioni.x䍍㍍fd`letqEx\=f(y};z:)in`g}(x4D)8+hc(x)ۀ\Let?x=f(y,z)\Inۀg(x)+h(x)#Ǎ㍍fd`letqEx\=f(y};z:)injx4D^2ۀ\SLet?x=f(y,z)\In{x^2}ꪍMNoticeTthat\SLettakesasecondargument,Twhichispartofthesame`para->graph',UUwhere\LetdoGesnot.MTheUUtypGesettingofacasesclauseismorecomplicated.qIttakestheform:W\Cases{UUhmath-moGde-expressioni}Wfrom-hmath-moGde-expressioni&UUto-hmath-mode-expressioni\\Wfrom-hmath-moGde-expressioni&UUto-hmath-mode-expressioni\\W...W\Otherwise{UUhmath-moGde-expressioni}W\EndcasesMThe`\Otherwise9Af eld`isoptional. AThisconstructionfollowsageneralpattern>thatiscommoninvdminput:Slistsofthingsareseparatedby\\ s,$andsub elds>areUUseparatedby&sor:s.ABInrealit9y:,thereisanother,optionalargumen9t,aftertheD\Endcases.AB._dIfy9ouwereto >tryTt9ypAesettingsomethinglikec̰D(...var=\Cases..."\Endcases)>By9ou'd" ndtheclosingrightparenthesisinanunexpAectedplace(onthesamelineas>theg=,| infact).T:ogettexttotherigh9toftheD\Endcases1UFByoucanplaceanoptional>argumen9tTwithinbracketsafterit:c̰D(...var=\Cases..."\Endcases[)]>BAdmittedly:,TthisloAoksalittlestrange,butitdoesw9ork.MHereUUisanexampleof\Cases&*inaction:8 Wy?kcasessele}'ctز(x4D)of n)nil!fgkmk-Lstز(hd;tl)!fhdg8[elemstlkothersxkendEcX?\Cases{?select(x)} X?\nil>&?\emptyset\\X?mk-Lst(hd,tl) &?\set{hd}\union\elems{tl}X?\Otherwise{?x}X?\EndcasesMNotewthe\\o@isasep}'arator0andwnotaterminator|youdon'tneedoneafter>theZlastitem. Also,\the\Otherwise94canappGearanywherebetweenZthe\Cases{}>andUUthe\Endcases2:,butitwillalwaysUUbGetypesetlast.A'BSome'pAeopleprefertheselectorstoappearlinedupontheleft, someontherigh9t.If >y9ouwantthemtoappAearontheleft,.sayD\leftCases2VB;ifyouwantthemontheright,>sa9y\D\rightCases7B.The\scopAeoftheD\leftCases6BandD\rightCases;v*Bcommandsisthe>curren9tTgroup.pBydefault,yougetD\rightCases7B.6>3.2.1a#TheTformboxEn9vironmentuT>Occasionallyyoumight ndthatyouwanttoputalinebreakinaplacethat >can'thandle\\`.F*orexample,ifyouhavea\Cases'AȲcommandandtherhsof>a1 particularcaseistoGobig,hyoucan'tuse\\:tobreakthelinedirectly*,asit>will^bGeinterpretedastheseparatorbetween^cases.U Thenyoumusttheformbox>environment.nIt7issimilartotheformulaenvironment7inthatyoucanputall>sortsIofthingsinit,butitcanbGeusedwithinotherconstructions,unlikethe>formulaUUenvironment,whichcanonlybGeusedattheoutermostlevel.MThisUUexampleshouldconveyUUthegeneralidea:g\Cases{?f(x)}gmk-Very_long_constructor(foo,bar)?&|{\begin{formbox}|long_predicate_with(foo)?\\\And?long_predicate_with(bar)|\end{formbox}}g...kcasesf(x4D)ofkmk-V;ery|p|long|pc}'onstructor(foo;bar) Q]!long|p|pr}'edicateYpYwithc(foo)^8long|p|pr}'edicateYpYwithc(bar)ԍ:::kend9]ߍ>Note theextrasbracesaroundtheformbox;thesearerequiredto\hide"the\\>fromUUthe\Cases"C.9 bSy?>L3.3\OtherGeneralPointsab`outFormulasuT>\\Lwill^3alwaysخstartanewline.oSometimesthisisdoneinadditiontosome >otherifunction(asinthe\Cases% macro,2whereitdelimitsaparticularcase),but>youshouldbGeabletouse\\Lalmostanywheretoforcealinebreak.Indeed,>soGonerlorlateryou'llwanttotypGesetalongformulaandTU>'ExXwillnotbGeable>tobreakthelinesensibly*,1orwillchoGoseanunpleasantbreak.JInthiscaseyou'll>haveUUtouse\\ O.MF*requently;youneedtoindentthingswithinmulti-lineformulas.%LT*ohelp>youdothis,Facommandisprovidedwhichbreaksaline,Fandindentsthenext>lineߌbyanamountwhichyoucansupply(inunitsofems).mThe\T?command>takesUUasingleargumentthatcontrolshowmuchthenextlinewillbGeindented:꫍㍍fd`aC^8bz)hbx^8amG_dAi^8eۀa?\Andb\T2ۀ\Implies?b\Anda\T1ۀ\Or?d\AndeꪍMAlongp similarlinesisthe\R`command.ThisdoGesalinebreak,vlike\\ ,but>thenUUpushestheformulaonthenextlineasfartotherightasitcan:꫍㍍fd`(aC^8b)hbx^ac)r_dAi^8eۀ(a?\Andb\Impliesb\Anda)\Rۀ\Or?d\AndeꪍMBeware:XitmayenduppushingitfurthertotherightthanyouexpGected!>ThisUUisAABug,andAWillNotBeFixed,soyou'llhavetoworkaroundit.MThe\IfC,1\Let%,1etc.,constructionsareallunusualinthatit'simpGossibleto>typGesetUUsomethingsensiblytotherightofthem.qF*orexample,ifyoutryOg\exists{x?\inS}{w\If?x=0\ThenS=Q\ElseS=P\Fi}g\Or?S=\emptyset>thenUUyou'llgetk9x\2S8if Çx\=08thenS=Q8elseSS=P_S=fg' >whichUUisunlikelytobGewhatyouwanted.MY*oushouldalsoremembGerthatwherevdmwantsahmath-moGde-expressioni,>TU>'ExX willbGeplacedinmathmode.Thisisusuallytherightthingtodo,9but>oGccasionallyyoumightwantanaturallanguagecommenttoappGearthere.In>thisRcaseyou'llhavetoinsertan\mbox"#ora\parbox-edepGendingonwhether>yourUUcommentmightspanoneormorelines:%꫍㍍fd`ifk 1theUUconditionistrue`thenz,doUUthetruepart`elsevdoUUthefalsepartۀ\If?\mbox{theconditionistrue}ۀ\Then?\mbox{dothetruepart}ۀ\Else?"dothefalsepart"ۀ\Fi>" ffv J= "5-:3LFJorX`will'read`should'.10 mHy?>TheMelse-partillustrateshowquotescanbGeusedananabbreviationfor >\mbox{...}UUwithinmathmoGde.MFinally*,*falltheconstructionsabGovewillnotbreakatapageboundary*._This>means_vthatyou'reinbigtroubleifyouwanttotypGesetathree-page\Cases!d.The>onlystatementIcanmaketomitigatethisis:Gyoushouldn'thaveexpressions>that0Mcomplicatedinthe rstplace|whodoyouexpGecttoreadthem?eoRemem->bGer:\truthisbeauty",soifyourformulasarenotbGeautiful,thenchancesare>they'reUUnottrueeither. ݍ>4VLTyps3esettingffdatatyps3es>TheUUfollowingtableliststheprimitivetypGesandvqaluesavqailable:EYǀffp"fdͤ ff͟fdf0;1;::: UOg(š ff]-N ff)\Nat< ffͤ ff͟fdf1;2;::: UOg(š ff]-N1 ff)\Natonei,\Nati  ffͤ ff͟fdf::: UO;1;0;1;:::g͡ ff]-Z= ff)\Int< ffͤ ff͟fdRationals( ff]-Q  ff)\Rat< ffͤ ff͟fdRealUUnumbGersi- ff]-R ff)\Real< ffͤ ff͟fdftrue3;falseŤg ff]-B= ff)\Bool< ffͤ ff͟fdT*ruth8 ff]-trueyu ff)\true,\True* ffͤ ff͟fdF*alsehoGod%֡ ff]-falseyu ff)\false),\False%L ffͤ ff͟fdNilDL ff]-nilyu ff)\nil< ffffp"MIf{youneedanewkeyword,Dyoucancreateoneeasily*.For{example,Difyour>favouriteUUbrandoflogichas\maybGe"asavqalue,youcansayBg\makeNewKeyword{\maybe}{maybe}>and#henceforth\maybe*4isavqalidcontrolsequencethatproGducesthetext >ma9ybQe^.`TheOtextofthesecondargumentto\makeNewKeywordW_canbGeany->thing;UUitdoGesn'thaveUUtomatchyourcontrolsequencename.ABIfy9oudon'tlikethefontthatkeywordsaresetin,youcanchangeitbyrede ning >theTcommandD\keywordFontBeginSequencey4B.pBydefaultitexpandstoD\sfBB.MTheUUfollowingtypGe-relatedcommandsareprovided:Rԏj.qffQfdͤ ff͟fdOutput ff; InputA ffq ffffQͤ ff͟fdx4D-set%R ff; \setof{x}* ff {setUUtypGeconstructor iB ff ͤ ff͟fdfac;b;cg ff; \set{a,b,c}  ff {setUUenumerationE ffͤ ff͟fdfg#,Ρ ff; \emptysetH ff {theUUemptyset( ffͤ ff͟fdx4D^*3롄 ff; \seqof{x}* ff {seq.qtypGeUUconstructor"% ffͤ ff͟fd[ac;b;a;c]͡ ff; \seq{a,b,a,c}ğ ff {seq.qenumeration ffͤ ff͟fd[]' ff; \emptyseqH ff {theUUemptysequence0` ff H\ͤ H\ff͟fdxT΍dGm2\ !yy H\ff; \mapof{x}{y} H\ff {mapUUtypGeconstructor͟ H\ffͤ H\ff͟fdxT΍ m2\ UX!y A H\ff; \mapinto{x}{y}Lǟ H\ff {one-oneUUmaptypGe H\ff ͤ ff͟fdfph7!x4Dg l ff; \map{p\mapsto?x}͟ ff {mapUUenumeration@ ffͤ ff͟fdfg#,Ρ ff; \emptymapH ff {theUUemptymap!iB ffffQ11 z4y?>HereUUaretherelevqantopGerators:F8.yD!F2jD\inՌFywD\owr,ȑ Ka msbm9KyaiD\sconc E(E5" cmmi9E=D!F2jD\notinՌI/2i lasy9IwD\dres,ȑMt : cmbx9MlenDvdm(Bde nefory9ouacontrolsequencewhichswitchesfont,-andputstherightspacing>in.pF:orTexample,c̰D\newMonadicOperator{\inv}{inv}>Bwillde netheD\invBcon9trolsequencetoprintMinCv%B.|uHenceforthyoucansay:,e.g., >D\inv{Foo}B.pAllTsuc9hsequencestakeoneargument(theyaremonadic,afterall).MY*ouUUcande neanewtypGeusing\type{typGe-name}{type}:, `Complex\=R8R\type{Complex}{\Real\x?\Real}xMCompGositesUUtypescanbetypesetusingthecompositeenvironment:&1ȍ㍍fd`compQose Date}'cf of w_dayٿ:f1;:::;366g;tye}'arٿ:f1583;:::;2599g`endٿ\begin{composite}{Datec} Yday?:\set{1,\ldots,366},\\Yyear:\set{1583,\ldots,2599}ٿ\end{composite}&x㍑MThereisalsoacomposite*environment(andanequivqalent\scompose5 Kcon- >trolUUsequence)thatplacestheentirecompGositetypGeonasingleline: x䍍㍍Ǎ`compQose CelsiusuofTRTend\begin{composite*}{Celsius}\Real\end{composite*})Ǎ㍍Ǎ`compQose CelsiusuofTRTend\scompose{Celsius}{\Real}ꪍM`Records'UUcanbGede nedusingtherecordenvironment:W\begin{record}{record-typGe-name}W eld-nameUU: eld-typGe\\W...W\end{record}12 Gy?>TheUUcolonsareusedassub- eldseparators.%꫍㍍ `PERSON::(KNM29:Char^GFEM29:B\begin{record}{PERSON}  NM?:\seqof{Char}\\ FEM?:\Bool\end{record}%ꪍMIfUUthede nitionisshort,youmayprefertouseashortform:Sg\defrecord{PERSON}{ rNM?:\seqof{Char}\\rFEM?:\Boolg}S@"BSome"pAeoplepreferthe eldnamestoappearlinedupontheleft,someontherigh9t. >If|y9ouwantthemtoappAearontheleft,sayD\leftRecord7B;ifyouwantthemonthe>righ9t,{sayD\rightRecord;3B.ThescopAeoftheD\leftRecord8BandD\rightRecord=Bcommands>areTthecurren9tgroup.pBydefault,yougetD\rightRecord;\B.MUpGdatingdO eldsofcompositesusingthe-functioncanbespeci edusing >\chgR:1ȍ㍍fd`(p;FEMj7!:manc(q}))ۀ\chg{p}{FEM}{\Not?man(q)}ꪍMNoticeUUthatthe,parentheses,commaand7!wereinsertedautomatically*. 컍>5VLHowfftoTyps3esetFfunctions>TypGesettingUU-expressionsiseasy:꫍㍍fd`x4D;yx׸8x4D^2闲+y}^2ۀ\LambdaFn{x,y}{x^2+y^2}x㍑MAssGwith\forall'32,~\exists)Ӱand\unique,~\LamdbaFn4Shasa*-formthatplaces>theUUbGodyofthefunctionbelowandtotheright:|eg)fd`x4D;y};zY #tw(x4D^2闲+8y}^2в+z:^2) 33Zcmr5133xW g P2ۀ\LambdaFn*{x,y,z}{(x^2+y^2+z^2)^{\frac12}} MThere|isalsoafn(function)environment|forde ningnamedfunctions.}hasUUthefollowingstructure:W\begin{fn}{name-of-function}{UUargument-list}W\signature{signature-of-function}WhoptionalUUpreconditioniWhoptionalUUpGostconditioniWbGodyUUoffunction(ahmath-moGde-expressioni)W\end{fn}MSeeffthethirdpageforanexample.The\signature;LisoptionalandcanbGe>placed OanywherewithinthebGody|it OwillalwaysbGetypGesetbeforethebody*.13y?>Useful!.7NoteZthatyoucanalsoenterfunctionsde nedimplicitlywithpre-and>pGost-conditions;UUseethenextsectiononhowtoenterthem.MAllFofthematerialinthesectiononformulasisrelevqantwithinthebGodyFof>theUUfunction.MIfyoufrequentlyinterspGerseyourfunctionde nitionswithtext(and>youshould),youcansavesometypingbyusingthevdmfnenvironment.>\begin]{vdmfn} ϲ...\end{vdmfn}isequivqalentto\begin&{vdm}\begin{fn}>...\end{fn}\end{vdm}.MThefnenvironmentalsohasa*-formthatdoGesnotinsertparentheses>aroundUUtheargumentlist.qF*orexample:%꫍㍍fd`MPqG[UX[p]]䍑 [4 [ڟ݉\)@õ:::ۀ\begin{fn*}{MP}{\term{p}\rho\sigma}ۀ...ۀ\end{fn*}&8MIfUUyourequirethe䍓4݉\)@8symbGolbyitself,thenyoucangetitbysaying\DEFUI.6>L5.1\Inv@ariantsuT>T*oUUtypGesetaninvqariantonacompGositeob8ject,usethefollowingstructure:=꫍㍍ `D::{dayu:DayxBye}'aru:Y;e}'ar `where`inv-Dzٲ(mk-D(d;y}))䍑 4 ݉\)@tis!-le}'apyr(y})_dϡ365\begin{record}{D}day?:Day\\year?:Year\end{record}\where\begin{fn}{inv-D}{mk-D(d,y)}is-leapyr(y)?\Ord\le365\end{fn}P >6VLHowfftoTyps3esetOperations>OpGerationsUUaretypesetwithintheopenvironment.qTheUUgeneralstructureis:W\begin{op}[hname-of-opGerationi]W\args{hlist-of-argumentsi}W\res{hresult(s)i}W\ext{hlist-of-externalsi}Whpre-conditioniWhpGost-conditioniW\end{op}MThea,orderofthevqariouspartswithintheopenvironmenta,isnotimpGortant;>theyUUwillalwaysUUbGeprintedinacanonicalstyle(seepage3foranexample).14y?MAnyof\args ɲ,dx\resdl,dx\ext,dxhpre-conditioniزorhpGost-conditionimaybGe >omitted. \begin{vdmop}isanabbreviationfor\begin{vdm}\begin{op};>\end{vdmop}UUisanabbreviationfor\end{op}\end{vdm}.MTherhname-of-opGerationicanbeanyone-lineexpression;6itistypGesetinmath>moGde.DCAnalternativewayofspGecifyingthenameoftheoperationistoomitthe>optionalVargument(within[]),anduse\opname{hname-of-opGerationi},any->whereUUwithinthebGodyUUoftheopenvironment.MThelhlist-of-argumentsiisahmath-moGde-expressionithatcanspanmultiple>lines;UUforceanewlinewith\\ O.qIfpresentitisplacedwithinparentheses.MThe}hresult(s)iisalsoanyhmath-moGde-expressioni.AItistypGesettotheright>ofUUanyarguments.MTheUUhlist-of-externalsitakesthefollowingform:W\ext{ahoptionalUU\RdjorUU\WrLiUUhexternal-name(s)i:qǸhexternal-typGesi\\ahoptionalUU\RdjorUU\WrLiUUhexternal-name(s)i:qǸhexternal-typGesi\\W...W}>Alternatively*,|nif6thelistofexternalsislong(say*,|nmorethan velines)the>externalsUUenvironmmentcanbGeused:W\begin{externals}ahoptionalUU\RdjorUU\WrLiUUhexternal-name(s)i:qǸhexternal-typGesi\\ahoptionalUU\RdjorUU\WrLiUUhexternal-name(s)i:qǸhexternal-typGesi\\W...W\end{externals}B_cBSome_cpAeopleprefertheexternalsiden9ti erstoappearlinedupontheleft,some >on therigh9t.IfyouwantthemtoappAearontheleft,JsayD\leftExternalsF3:B;ifyou>w9ant4themontherigh9t,|~say4D\rightExternalsKsB.zoThe4scopAeoftheD\leftExternals>BandD\rightExternalsRBcommandsarethecurren9tgroup. 8Bydefault,youget>D\leftExternals&4B.MTheUUhpre-conditioniandhpGost-conditionitakesimilarforms:W\pre{hmath-moGde-expressioni}>orW\begin{precond} Whmath-moGde-expressioniW\end{precond}>andW\post{hmath-moGde-expressioni}>or15y?W\begin{postcond} Whmath-moGde-expressioniW\end{postcond}'>UseHthe\begin"L6...\endvstyleHifthehmath-moGde-expressioniislongerthanafew>lines.$AlldoftheconstructsmentionedinthesectiononformulascanbGeused>withinUUpre-andpGost-conditions.!>7VLPros3ofs>Here'sUUanexampleoftypGesettingproofsinthe\naturaldeduction"style.)jfd\fromwjE1C_E2M1%jfrom@CE1wjinferZE2C_E1w4_-I(h1)M2%jfrom@CE2wjinferZE2C_E1w4_-I(h2)\infervE2C_E1iN1_-E(h,1,2)yg\begin{proof}|\From?E@1\OrE@2\\g1$\From?E@1\\\Infer?E@2\OrE@1 \by$\vee$-I(h1)\\g2$\From?E@2\\\Infer?E@2\OrE@1 \by$\vee$-I(h2)\\|\Infer?E@2\OrE@1\by$\vee$-E(h,1,2)\\g\end{proof}1MProGofsareembeddedwithintheproofenvironment.D\(Aproofdoesnothave>tobGewithinavdmenvironment.)2Eachlineoftheproofendswith\\k.2Lines>that[}bGeginasubproofhave[}\From after[}theequationnumber.?Lines[}thatenda>subproGof"have\Infer%aftertheequationnumbGer.`Otherlineshave\&afterthe>equation numbGer(seenextexample). Ifyoudon'tneedanequationnumbGer,>justomitit,butyoumusthaveoneofeither\From*,\Infer%jor\&UPoneachproGof>line.e5If/youwanttoincludeajusti cationofaparticularproGoflineattheright>hand!endoftheline,,3typGeitaftera\by.`\byBisoptional;3youneedn'tincludeit>ifUUyoudon'tneedajusti cation.MPointsUUworthbGearinginmind:MWY*ouareautomaticallyplacedinmathmoGdeafterthe\From2 ,H\Infer'NorW\&a;UUthemathmoGdeendsatthenext\byjor\\ O.MWY*ou&0c}'annotbreakalineinthemiddlesimplybyusing\\ZbGefore\by';5youWmustUUuseseparateproGoflinestosplitaformula.16Ey?MWY*ouUTarewithinatabbingenvironmentUTwithinaproGof,soyoucanuseall Wthe''usualtabbingcommands(\= ,0d\> ^,0detc.)bctolinethingsupacrossproGofWlines.NotethatyouwillexplicitlyhavetoentermathmoGdeagainafterWanyUUofthesecommandsthough.fMHere'sUUanotherexample:"fd\fromwj8x\2XE8E3(x4D);s92XM1%j:9x\2X$8:E3(x4D)n*8-defn(h)M2%j::E3(s!=x4D)im:9-E(1,h)\infervE3(s!=x4D)a2>\begin{proof}H\From?\forall{x\inX}{E(x);s\inX}x\\>1?\&\Not\exists{x\inX}{\NotE(x)}\by$\Forall$-defn(h)\\>2?\&\Not\NotE(s/x)D?\by$\Not\Exists$-E(1,h)\\H\Infer?E(s/x)?y\\>\end{proof}@LB.)BThe.)amoun9tofspaceusedbytheproAofnumbAercanbec9hangedbychangingthe >lengthD\ProofNumberWidthS;yB. ThedistancefromtheleftmargintotheproAofn9umberis>dictatedTb9yD\ProofIndent;\B.%>8VLCustomisingfftheStyle>Some op}'eopleareneversatis ed. W*eallknowthatit'strue.Inordertocater >forthosewhoaren'tsatis edwiththeoutputfromvdm, someattempthasbGeen>madegtoallowalimiteddegreeofcustomisationbytheuser.@Inparticular,>you canaltersomeoftheinternalspacingchosenbyvdm,ԓandevenhaveyour>ownmacroscalledatchosenplaceswithinvdm'smacros.UNaturally*,cyouarenot>advisedltotrythisunlessyoufeelyouhavesomeideaofwhatyouwant,and>whatnyouaredoing.Inthissectionwelistthethingsthatyoucanchange,4in>orderUUofincreasingdiculty*.2>L8.1\ChangingtheSpacinguT>In6severalplaces,essentiallyarbitraryspacingshavebGeenchosenbytheauthor.>TheFdimensionsofthesespacesaregivenbyrubb}'errlengths.^4 ¼Ifyouwantto>change anyofthem,&useL5ffA͉TU>'ExX's\setlength:or\addtolengthE5commands.^YF*or>example,g\setlength{\postHeaderSkip}{13.33pt?plus2ptminus1pt}>Rffv J= "5-:4LSeeXtheL#A TAEMXbshrink]b9y:.4Forexample,pD12ptplus2ptminus1ptBmeansthatthelengthwillbAein>theTrange11{14pt,with12ptasits\natural"length.MThe.spacesinquestionallappGeararoundvdmitemssuchasoperations,6xand >inSbGetweenma8jorpartsofsuchitems.qThenamesofthelengthsshouldconvey>where6theyapply*.lThefollowingtablelistsallthelengths,oDandtheirdefault>settings.dNNote,thatanexisabGouttheheightofan\x"inthecurrentfont,4and>anUUemisabGoutthewidthofan\M"inthecurrentfont.LˍAjџffR*^fdͤ ff͟fdL}'ength{D ffDefaultsize+jΟ ff *Use}'dwithin8 ffffR*^͟ ff͟fd\preOperationSkipF ff2exUU+0.5ex0.2ex͟ ff *opUUenv+ ff ͟ ff͟fd\postOperationSkipF ff2exUU+0.5ex0.2ex͟ ffQ+ ff͟ ff͟fd\postHeaderSkipF ff.5exUU+.2ex.2ex  ffQ+ ff͟ ff͟fd\postExternalsSkipF ff.5exUU+.2ex.2ex  ffQ+ ff͟ ff͟fd\postPreConditionSkipF ff.5exUU+.2ex.2ex  ffQ+ ffffR*^fd͟ ff͟fd\preFunctionSkipF ff2exUU+.5ex.2exϟ ff *fnUUenv+ ff͟ ff͟fd\postFunctionSkipF ff2exUU+.5ex.2exϟ ffQ+ ff͟ ff͟fd\betweenSignatureAndBodySkipF ff1.2exUU+.3ex.2ex ffQ+ ff͟ ff͟fd\betweenFunctionAndPreSkipF ff1.2exUU+.3ex.2ex ffQ+ ffffR*^fd͟ ff͟fd\preTypeSkipF ff1.2exUU+.5ex.3ex ff *typeUUcommand͟ ff͟ ff͟fd\postTypeSkipF ff1.2exUU+.5ex.3ex ffQ+ ffffR*^fd͟ ff͟fd\preCompositeSkipF ff1.2exUU+.5ex.3ex ff *compositeUUenvş ff͟ ff͟fd\postCompositeSkipF ff1.2exUU+.5ex.3ex ffQ+ ffffR*^fd͟ ff͟fd\preRecordSkipF ff.75exUU+.3ex.2ex ff *recordUUenv ff͟ ff͟fd\postRecordSkipF ff.75exUU+.3ex.2ex ffQ+ ffffR*^fd͟ ff͟fd\preFormulaSkipF ff1.2exUU+.5ex.3ex ff *formulaUUenvE ff͟ ff͟fd\postFormulaSkipF ff1.2exUU+.5ex.3ex ffQ+ ffffR*^fd͟ ff͟fd\preProofSkipF ff.75exUU+.3ex.2ex ff *proofUUenvŹ ff͟ ff͟fd\postProofSkipF ff.75exUU+.3ex.2ex ffQ+ ffffR*^U>L8.2\ControllingLineandParagraphBreaksuT>TU>'ExX>musesthenotionofp}'enaltiestodecidewherelineandpagebreaksgo.V*arious>vqaluesofpGenaltyareusedatplaceswithinvdmtocontrolbreaks.}T*ofully>understandhowtochoGosebreaks, readTheTKß'E-Xb}'ook. However, putsimply*,>pGenalties~arewholenumbers~intherange10000to10000.CA\vqalueof10000>meansf\neverbreakhere,"andavqalueof10000means\alwaysbreakhere.">V*alues/inbGetween/penaliseorencouragebreakingproportionally*,sothat,e.g.,a>vqalue.of500encouragesabreak,6butbynomeansforcesit.dA.valueofzerois>neutral.MT*o8"assigntoapGenalty\p ,=write\p=1000,=forexample.h ThetablebGelowlist>theUUpGenaltiesusedbyvdm,andtheirdefaultvqalues.18'y?=eMßff9{fdͤ ff͟fdPenaltyNamej̋ ffDefaultUUV*alue͟ ff9WhereUUUsedw` ffff9{͟ ff͟fd\preOperationPenaltyY= ff0L8.3\UnforeseenChangesuT>ItisatruismthatnomatterhowgoGodthedesignerofapieceofsoftwareis, >henycanneverforeseeallofitsuses.3Inthiscase,theauthorisquitecertain>that^pGeoplewillusevdmforallsortsofthingsapartfromtypesettingVDM>spGeci cations.h4T*o8caterforthosewho ndthatvdmdoesalmost,>Zbutnotquite,>whattheywant,$anumbGerofho}'okshavebGeenleftinplace.bThesehooksare>macros,5whichoatthemomentdolittleornothing,5butwhichcanbGerede ned>byuserstochangethebasicopGerationofvdm(seethevdmindexstyleforone>suchuse).Needlesstosay*,2#anyonewishingtorede neahoGokshouldalready>bGe_qcompetentinthewaysofL5ffA͉TU>'ExXatleast,aandprobablyTU>'EXaswell.Rather>thantryingtoexplainwhatthehoGoksdo,2andwheretheydoit,theusershould>loGokCthroughthecommentedversionofvdm(usuallystoredasvdm.doc)and> gureitoutforhimself."BelowarelistedalltheprovidedhoGoks,etheirdefault>de nitions,UUandwheretheyareused.19y?rY> ff[0dͤٛ ff͟&e*#fcmti8Name~ofhookk9i ffDefault~de nitionnK7ٛ ff@ff[0ͤٛ ffg&eNCscmtt8NopXenÎvironment ffff[0ٛ͟ ff͟&eN\preOperationHook* ff\penalty\preOperationPenalty 4ٛ ff ٛ͟ ff͟&e\betweenHeaderAndExternalsHook* ff\penalty\preExternalPenalty 8ٛ ffٛ͟ ff͟&e\betweenExternalsAndPreConditionHook* ff\penalty\prePreConditionPenalty 'ٛ ffٛ͟ ff͟&e\betweenPreAndPostConditionHook* ff\penalty\prePostConditionPenalty #ٛ ffٛ͟ ff͟&e\postOperationHook* ff\penalty\postOperationPenalty 0Lٛ ffff[0dͤٛ ffg&efnXenÎvironment ffff[0ٛ͟ ff͟&eN\preFunctionHook* ff\penalty\preFunctionPenalty 8ٛ ff ٛ͟ ff͟&e\betweenSignatureAndBodyHook* ff\penalty\betweenSignatureAndBodyPenalty ٛ͟ ffٛ͟ ff͟&e\betweenFunctionAndPreHook* ff\vskip-\lastskip g)ٛ ffٛ͟ ff* ff\vskip\betweenFunctionAndPreSkip'ٛ ffٛ͟ ff* ff\penalty\betweenSignatureAndBodyPenalty ٛ͟ ffٛ͟ ff͟&e\postFunctionHook* ff\penalty\postFunctionPenalty 4ٛ ffff[0dͤٛ ff_&erecordXenÎvironment ffff[0ٛ͟ ff͟&eN\preRecordHook* ff\penalty\preRecordPenalty AMٛ ff ٛ͟ ff͟&e\postRecordHook* ff\penalty\postRecordPenalty = ٛ ffff[0ͤٛ ff9VLInstallingfftheCvdm les>Placethe levdm.styinyourstandarddirectoryforL5ffA͉TU>'ExXstyle les(your >systemHadministratorwillknowwherethisis).IfyouhavetheAMSfonts,>change]theappropriatelineinvdm.sty(seeinstructionsattheheadofthe le).!č>10^fdNewCvdmcommands(intros3ducedfortheO-ff cmcsc10Obsi^fdversion)MWThereUUisanewkeyword,UU\remUI.MWOpGerationsv,canalsohavev,anerr}'orcondition:part,~btypesetv,afterthepost-Wcondition.Theyderrorconditionisplacedinanerrcondenvironment.AnWalternative shortform,N\errN,Nisalsoavqailable,NwhichworksinthesameWwayUUas\preand\postF.WInsuppGortofthisnewpart,t?thereisahook,W\betweenPostAndErrConditionHook,gde nedԙtobGe\penaltyW\preErrConditionPenalty֑(the1defaultpGenaltyis500).\Thepre-Wcedingfwhitespaceisde nedby\preErrConditionSkipp"(default.5ex+W.2exUU.2ex).MW\OthersBisUUanaliasfor\Otherwise77.MWSequentsUUaresuppGortedusingthesequentcommand,thus:20캠y?䍍㍍fdyA`B yT;ruthc;Be}'auty};eq}-intr`T;ruth{=Be}'auty\sequent{A}{B} \sequent*{Truth,Beauty,eq-intr}{Truth=Beauty}'ꪍMWOptionalUUitemscanbGetypesetusing\OptUI,thus:1ˍyb}8fr}'edb\Opt{fred}ꮍMWThereUUaretwoUUnewmonadicopGerators,\absand\merge"C.MWAUUnon-emptysequencetypGecanbede nedusing\neseqof-U=,thus:1ȍ㍍fdyN^+\neseqof{\Nat}x㍍MWRestrictedŵtypGes(thosewithinvqariants)canbGetypGeset,withorwithout Winitialisation,UUusing\ritype+jand\rtype"C,thus:<1ȍ㍍ yPartition{=(N-setGr)-set'yin9v0inv-Partitionc(p)syDict=B(L}'etterT΍Cm2ڥ !4Dictز)yin9v0trueyinitڲ(true3;fg)\rtype{Partition} {\setof{(\setof{\Nat})}} {inv-Partition(p)}\ritype{Dict} {\Bool?\x(\mapof{Letter}{Dict})} {\true} {(\true,\emptymap)}`(defaultW.5exUU+.3ex.2ex)and\betweenInvAndInitSkipz*h(samedefault).MWRecordtypGesmayalsohaveinvqariantsandinitialstatesattached,usingWtheUU\invandUU\init ꛲commandsUUwithintherecordenvironment,UUthus:;꫍㍍ yD::dayw:DayDye}'arw:Y;e}'ar'yin9v0(mk-D(d;y}))4݉\)@0is!-le}'apyr(y})_dϡ365yinitday=40^ye}'arڥ=1962\begin{record}{D} day?:Day\\ year?:Year\inv{(mk-D(d,y))?\DEF is-leapyr(y)?\Ord\le365}\init{day=40?\Andyear=1962}\end{record};ꪍWT*o?gowiththeseare\betweenRecordAndInvHook,W\betweenInvAndInitHook,3-\betweenRecordAndInvSkip9(default.5ex+W.2exUU.1ex),and\betweenInvAndInitSkipz*h(samedefault).21y?>11^fdAcknowledgements>ManypGeoplehavepassedonusefulsuggestionsandcommentsabGoutvdmand >this,doGcumentation;/manythankstoallofthem.%MInparticularIwouldlike>to=$acknowledgetheextensivetestingdonebyLynnMarshallwhilepreparing>her thesis,andherhelpfulcommentsandideas,andthenumerousworthwhile>discussionswithCli Jones.Cli ,inparticular,deservesthehighestcommen->dationiforbravery*,einiactuallyusingthesemacrosinhisbGook.NThanksitoDavid>CarlisleUUforhelpingwiththeconversionUUtoTU>'ExX3.22?;yO-ff cmcsc10NCscmtt8Mt : cmbx9LN cmbx12Ka msbm9I/2i lasy9Hj cmti9Gzi cmex9F cmsy9E5" cmmi9DߤN cmtt9C߆Tff cmtt12Bo cmr9A- cmcsc109t}\cmti76 cmmi10K`y cmr10ٓRcmr7Zcmr5u cmex10 c