Spec2Box - Adelard
Contents
1. 9 2 9 3 Modules 9 2 9 4 Type definitions 9 4 9 5 Type expressions 9 4 9 6 State definition 9 7 9 7 Constant definitions 9 7 9 8 Function definitions 9 7 SpecBox User Manual version PC 2 21a Contents iii 9 9 Operation definitions 9 9 9 10 Statements 9 10 9 11 Expressions 9 13 9 12 Bindings and Patterns 9 20 9 13 Identifiers and basic tokens 9 22 9 14 Index to the grammar 9 24 9 15 Keywords 9 28 9 16 Operator precedence 9 29 9 17 Lexical rules 9 30 10 Illustrative examples 10 1 10 1 General observations 10 1 10 2 Notes on the ASCII syntax 10 2 10 3 Telegram analysis 10 4 10 4 Code 10 8 10 5 Bank Accounts 10 13 10 6 Binary Trees 10 17 11 1 11 1 Background 11 1 11 2 Sharing 11 8 11 3 Exports and imports 11 12 11 4 Instantiation and parameterization 11 13 12 Bibliography 12 1 13 1 SpecBox User Manual version PC 2 21a Contents SpecBox User Manual2. 4 3 44 DOS 4 5 The syntax checker 5 1 5 1 Syntarcheckeroptions 5 1 5 2 General operation 5 2 5 3 Selecting the start point 5 3 5 4 Selecting an insertion point 5 4 5 5 Action on error 5 4 5 6 Adding and correcting text 5 5 5 7 Editor 5 9 SpecBox User Manual version PC 2 21a 1 Contents 6 The analyser 6 1 6 1 Arities 6 1 6 2 VDM quotation expressions 6 3 6 3 Scope 6 4 6 4 Error messages 6 7 6 5 Caveats 6 13 6 6 Output during checking 6 14 6 7 Report file 6 14 6 8 Listing file 6 15 6 9 Cross reference file 6 15 7 TFX generator 7 1 7 1 General operation 7 1 7 2 Formatting 7 1 7 3 Comments 7 2 7 4 Line numbering 7 3 7 5 Subscripts 7 4 7 6 Running KTEX 7 5 7 7 bsivdm sty 7 6 8 Mural translator 8 1 8 1 Sytacticvariants 8 1 8 2 Unsupported classes 8 2 9 The SpecBox grammar 9 1 9 1 EBNF concrete syntax notation 9 1 9 2 Documents
3. type 63 precond pre expr 64 postcond post expr 65 fundefexpl 7 funtype fundefcont 66 fundefcont fundefbody fundefexplnyd 67 fundefbody identifier patparams patparams expr precond 68 fundefexplnyd identifier patparams patparams isnotyetdefn SpecBox User Manual version PC 2 21a Operation definitions 9 9 en 69 patparams pat pat 9 9 Operation definitions T0 opdefn identifier opdef 71 opdef opdefimpl opdefimplnyd opdefexpl 72 opdefimpl pattypeparams idtypepair externals precond postcond errs exception exception 73 opdefimplnyd pattypeparams idtypepair externals isnotyetdefn 74 externals ext extvar extvar 75 extvar readwritemode identifier identifier type 76 readwritemode rd wr 77 exception identifier expr gt expr 78 opdefexpl optype opdefcont 79 opdefcont opdefbody opdefexplnyd SpecBox User Manual version PC 2 21a 9 10 The SpecBox grammar 80 opdefbody identifier patparams stmt precond 81 opdefexplnyd identifier patparams isnotyetdefn 9 10 Statements 82 stmt assignment callstmt block nondetstmt forloops whileloop ifstmt casesstmt mccarthyst
4. Mnode Mnode lt Mrep mkk Key md Data rt Mrep inv mk Mnode lt mkk md rt A V lk collkeys It Ik gt mkk V rk collkeys rt mkk lt rk 4 4 1 Data is not yet defined 5 1 Key is not yet defined 6 1 state 2 State of 3 t Mrep end 7 1 functions 8 1 collkeys Mrep gt Key set 3 collkeys t A 3 cases 1 nil SpecBox User Manual version PC 2 21a Binary Trees 10 21 5 mk Mnode lt mkk md rt 6 collkeys It U mkk U collkeys rt end 9 1 operations 10 1 FINDB k Key d Data 2 ext rd t Mrep 3 pre k collkeys t 4 post 5 let mk Mnode lt mkk md rt t in 6 mkk A d md V 7 k gt mkk post FINDB k It lt d V 8 mkk gt k A post FINDB k rt rt d 11 1 INSERTB k Key d Data 2 ext wr t Mrep 3 pre k collkeys t 4 post 5 t nil t mk Mnode nil k d nil 6 V 7 is Mnode 1 A 8 let mk Mnode It old mkk md rt old T 9 in 10 k lt mkk A 11 J lt new Mrep 12 post INSERTB k d lt old lt new 13 t mk Mnode lt new mkk md rt old 14 15 V 16 mkk gt k A 17 rt new Mrep SpecBox User Manual version PC 2 21a 10 22 Illustrative examples 18 post INSERTB k d rt old rt new 19 t mk Mnode lt old mkk md rt new 20 21 22 12 1 end Tree SpecBox User Manual version PC 2 21a 11 MODULES This section gives some background to the use of the modulariza
5. 6 1 Output Report 7 1 Report tgm Telegram 2 count Z 3 ovlen B 8 1 functions 1 analyse telegram Telegram Report 2 analyse telegram wordl A 3 mk Report wordl charge words wordl 4 check words wordl 10 1 charge words Telegram gt Z 2 charge words wordl A 3 card j j inds wordl wordl j Z STOP SpecBox User Manual version PC 2 21a Telegram analysis 10 7 11 1 14 1 check words Telegram B check words wordl A w elems wordl len w gt 12 operations ANALYSE inpt Input out Output post len out len inpt A V i inds inpt out i analyse telegram inpt 1 end Telegram SpecBox User Manual version PC 2 21a 10 8 Illustrative examples 10 4 Code This example is from 1 starting on page 174 Notes e We strictly need is not yet defined for maxs and Letter and signatures for the functions e The invariant on the type Mcode in 1 uses the type Letter as though it was an expression which is picked up by the analyser module Code definitions types Mcode inmap Letter to Letter inv m forall x Letter amp x in set dom m Pcode map Letter to Mcode inv m forall x Letter amp x in set dom m Key map int to Letter inv m exists n int amp dom m 0 n SpecBox User Manual version PC 2 21a Code 10 9 Letter is not yet defined state Codei of c Pcode k Key e
6. SpecBox User Manual version PC 2 21a 1 2 Introduction the input file using the draft ISO VDM mathematical syntax A version of the parse tree can also be produced that can be input to the Mural 3 tool for the generation and discharge of proofs about the specification The system includes an on line help facility which can be invoked by pressing F1 When a menu is displayed the help is specific to the highlighted item otherwise it relates to the current activity Syntacticall correct SpecBox Acci E es rn rn rm rn rs a i Analyser Syntax JA Semantic Checker Syntax Checker Ascil VDM input file Report Generator I I I I Editor I I J J l l l l L and Mural files Mural Generator Translator Semantic Analyser report files FIGURE 1 OUTLINE STRUCTURE OF SpecBox SpecBox User Manual version PC 2 21a Method of operation 1 3 1 2 Method of operation This subsection outlines the general way SpecBox is used Refer to sections 3 to 7 for a detailed description of the functions provided A normal SpecBox session begins by typing specbox at the computer terminal After the system has loaded the top level menu is displayed with the item highlighted this is selected by pressing the key or the letter F The input file is then selected from the resulting menu or the pathname typed in After a file has been selected it
7. by expr do stmt 101 whileloop while expr do stmt 102 mccarthystmt guardedstmt guardedstmt othersstmt e 0 me guardedstmt guardedstmt othersstmt 103 ifstmt If expr then stmt elsifstmt else stmt if expr then stmt else stmt 104 elsifstmt elsif expr then stmt P 105 guardedstmt expr stmt 5 P H 106 casesstmt cases expr casesstmtaltn casesstmtaltn othersstmt end SpecBox User Manual version PC 2 21a Expressions 9 13 cases expr casesstmtaltn casesstmtaltn othersstmt oe end 107 casesstmtaltn pat pat stmt pat 2 stmt 108 othersstmt WAWA others 5 stmt 109 handlerstmt always trapstmt rectrapstmt 110 always always stmt in block 111 trapstmt trap patbind with stmt in block 112 rectrapstmt tixe trapbind trapbind in block 113 trapbind patbind gt stmt 114 return return expr 115 exit exit expr 9 11 Expressions applyexpr subsequence letexpr 116 expr SpecBox User Manual version PC 2 21a 9 14 The SpecBox grammar
8. letbeexpr defexpr quantifier uniqueexpr lambda isexpr recordconstr nameexpr literal bracexpr tupleexpr setormapexpr sequenceexpr recordmodifier ifexpr cases unaryexpr binexpr fieldselect polyfuninst undefined 117 defexpr def equalsdefn equalsdefn in expr 118 letexpr let letbind letbind in expr let simplebind stexpr in expr 119 letbeexpr 120 stexpr be st expr P SpecBox User Manual version PC 2 21a Expressions 9 15 121 letbind 122 valbind 123 letfunbind 124 unaryexpr 125 unaryop 126 binexpr 127 binaryop valbind letfunbind pattypebind expr identifier typevardecl fundef unaryop expr o p floor abs card len not dunion dinter power conc elems inds t hd dom merge inverse expr binaryop expr D gt SpecBox User Manual version PC 2 21a 9 16 The SpecBox grammar and or lt gt e lt gt lt lt subset psubset in set not in Peu Be WEN oy e set union munion uu Go Ui div inter comp mod
9. post POP c k1 i c k1 post PUSH i k3 c k3 V Key HI domce Z ky k2 gt e k c Kk SpecBox User Manual version PC 2 21a 11 12 Modules is contradictory in the case where ky ka which illustrates the potential pitfalls of this type of sharing Note that many values of the imported state Stack may be used in COLLECTION even though the module STACK is imported exactly once Another example of explicit addressing is shown by contrasting Mrep and Mnode on page 254 of 1 with Root Heap and Mnoder on pages 255 6 11 3 Exports and imports SpecBox currently recognizes simple objects declared in the imports part of the interface however it does not automatically set up corresponding definitions of pre and post conditions and so forth Thus the following simple example is recognized as correct by SpecBox 1 1 module STUDENTS 2 imports from NAMES 3 types Name 2 1 definitions 2 state 3 School of sch NAMES Name set A end 3 1 operations 2 ENROL n NAMES Name 3 ext wr sch NAMES Name set A pre n sch SpecBox User Manual version PC 2 21a Instantiation and parameterization 11 13 5 post sch sch U n 41 end STUDENTS 11 4 Instantiation and parameterization 11 4 1 Compiler dictionary This is taken from pp209 211 of 1 It addresses the specification of a compiler dictionary First we define a local dictionary 1 1 module LDICT 2 paramet
10. Most other classes can be checked using the menu item However since the concrete syntax used by the parser differs from the abstract and printed syntaxes some nonterminals particularly at the lower levels of the grammar are not accessible this way and an error message is produced if they are specified You can restrict the parse to these items within a higher syntactic class using the option on the parser menu see Section 5 2 5 2 General operation The syntax checker reads the input file and assembles the characters into tokens according to the lexical rules given in Section 9 As each token is completed it is written to the screen and then checked for grammatical correctness If the syntax of the input file is completely correct the message CHECK OK will appear in the bottom right of the screen when the end of the syntactic unit has been reached and the top level menu will be redisplayed The current line number is displayed at the bottom right of the screen during checking SpecBox User Manual version PC 2 21a Selecting the start point 5 3 If you are checking certain syntactic items the parser will be unable to deduce if the end of the item has been correctly reached This always occurs for example in the case of an expression since the following token might be a misspelt binary operator e g uinon for union Whenever there is a doubt the checker displays a menu headed End of text and highlights the toke
11. PC 2 21a 8 4 Mural translator SpecBox User Manual version PC 2 21a 9 1 9 THE SPECBOX GRAMMAR 9 1 EBNF concrete syntax notation The grammar consists of a collection of context free production rules in a standard way The EBNF notational conventions used are stated below 1 Each EBNF rule has the form non terminal rule body Therefore each EBNF rule is terminated by a semi colon symbol 2 Concatenation of items is specified by a comma 3 The bar symbol separates alternative choices within the body of a rule 4 Terminal symbols are quoted in double quotes e g abc Literal occurrences of a single quote within a terminal string are given literally e g a a 5 Non terminal symbols are specified by all lower case identifiers 6 Optional items are specified using the following notation 0 or 1 occurrences contents 7 Sequences of items are specified using the following notation SpecBox User Manual version PC 2 21a 9 2 The SpecBox grammar 0 or more repetitions contents The production rules are assumed to operate upon a stream of tokens produced by lexical analysis of a stream of characters the lexical rules are described in Section 9 17 An index to the grammar is provided in Section 9 14 The draft ISO VDM keywords are listed in Section 9 15 and the operator precedence is given in Section 9 16 9 2 Documents 1 do
12. an edit box appears headed Sort cross references Enter yes or no according to whether or not you want the cross reference file produced by the analyser to sort the entries into ASCII order Press or alone or click the right mouse button to retain the old setting SpecBox will only accept the words yes and no in response to this item See Section 6 9 for more information on the cross reference file Next an edit box labelled Virtual file drive will appear The purpose of this depends on whether you are using the 8086 or 80386 versions 8086 version Enter the drive name without a following for the disk you wish the parse tree to be stored on if it becomes too large to store in memory you should obtain the best performance from your system by specifying a virtual disk if your PC is configured in that way To specify the current drive clear the pathname using the key and then press Enter Press or alone or click the right mouse button to retain the old setting SpecBox User Manual version PC 2 21a DOS 4 5 80386 version Enter the pathname of the subdirectory in which temporary working files are to be stored If no subdirectory is configured the setting of the TEMP environment variable will be used if it is defined otherwise the root directory of the current disc will be used Press or alone or click the right mouse button to retain the old setting You can correct errors during input usin
13. in inds init inmap instantiation int inter inv inverse iota is lambda len let map merge mk_ mod module mu munion nat nati nil not of operations or others parameters post power pre psubset rat rd real rem return reverse rng seq seqi set skip st state subset then tixe tl to token trap true types undefined union using values while with wr yet Symbols amp k lt gt gt lt amp lt lt lt gt lt gt gt gt gt gt Q 1 l gt 1 7 SpecBox User Manual version PC 2 21a Operator precedence 9 29 9 16 Operator precedence The operator precedence is as follows Binary operators Prec Operator Prec Operator 1 gt 5 gt 2 A 5 7 2 V 5 3 x 5 3 6 U set union 3 e 6 U map merge 4 gt 6 4 lt 6 4 gt 6 i 4 lt T X 4 C 7 4 6 7 div 5 6 7 rem 5 g 7 N 5 4 7 o 5 4 8 mod 5 gt 9 T Unary operators bind more tightly than any of these SpecBox User Manual version PC 2 21a 9 30 The SpecBox grammar Type operators Precedence Operator 2 MN x Jef 9 17 Lexical rules This section describes the lexical rules obeyed by SpecBox and gives the relationship between the ASCII syntax and the mathematical syntax produced by the IATEX generator Identifiers nametoken Identifiers may be composed of upper and lower case lette
14. kk H SpecBox User Manual version PC 2 21a Expressions 9 17 128 quantifier 129 existsuniquequant 130 allquant 131 existsquant 132 uniqueexpr 133 setormapexpr 134 setinterval 135 setenum 136 emptyset 137 setcomp 138 mapenum existsuniquequant allquant existsquant exists1 bind amp expr forall multibind multibind amp expr exists multibind multibind amp expr iota bind amp expr emptyset emptymap setenum mapenum setcomp mapcomp setinterval WW WW gs el EXPT EXPT H 17 expr Ir expr iu 17 iu 17 expr Ir multibind Ir multibind comppred 7 expr gt expr expr 4 expr 7 SpecBox User Manual version PC 2 21a 9 18 The SpecBox grammar 139 emptymap 17 lo du 140 mapcomp expr gt expr multibind multibind comppred 141 comppred amp expr 142 sequenceexpr sequenceenum sequencecomp 143 sequenceenum lexpr expr 144 sequencecomp P expr bind comppred 145 recordconstr mkidentifier expr expr yr 146 recordmodifier mu expr fieldmod 5 fieldmo
15. the lines that scroll off the top cannot be accessed using the cursor keys Pressing causes the file to be reloaded so that the start can be accessed again This option is disabled during a parse as otherwise it would be too difficult for the parser to track changes The editor can be used to set the start of the check by positioning the cursor at the required position and pressing r10 See Section 5 3 for more details It can also be used to set an insertion point in the text Pressing causes a special character displayed as a small left arrow to be inserted in the source The syntax checker will stop when this character is encountered and produce the correction menu from which appropriate tokens can be selected Selecting a token will cause it to be inserted immediately before the insertion point The insertion point character can be deleted in the same way as any other character when no longer required See Section 5 4 for more details Miscellaneous functions With the keyboard the following actions control the miscellaneous functions SpecBox User Manual version PC 2 21a gt 5 5 11 Function 2 0 E Delete character at cursor Toggle insert and overwrite mode Delete character to left of cursor Mark insertion point Quit editor and reparse if parsing TY 4 Return to start of file not available if parsing mn n e Create new start of syntax check
16. to permit several instantiations of the same parameterized module e Module signatures are used to select entities with associated attributes e g type information and class for introduction into a scope ParmModSig introduces items for use in definitions and the parameter binding part ParmBind Internally defined items should not be defined using these names The names declared here are the formal parameter names that are involved in instantiating this module elsewhere ImpModSig as for ParmModSig so that SpecBox User Manual version PC 2 21a 11 8 Modules ImpModNm can be used to disambiguate constructs using name qualification i e ImpModNm item ParmimpModSig introduces items for use in definitions part and the name ParmInstModNm may be used to disambiguate constructs using name qualification ExpModSig selects particular items for use in the exports part e ParmBind is a series of bindings of formal parameter names to named entities each of which may have been provided by a standard module by a parameter or by a built in identifier Note that the present syntax makes it long winded to use certain built in operations as module parameters e g try directly providing gt or even hd The hierarchy of module imports and instantiation should be acyclic where the provision of actual parameters to modules is also taken into account e If the definitions part is omi
17. version PC 2 21a 4 1 4 UTILITIES This section describes the utilities reached from the top level menu for selecting the input file carrying out edits in conjunction with an external editor configuring the system and accessing the operating system 4 1 Selecting the input file Top level menu This function is selected to specify the source file at the start of a SpecBox session and to change the source file during the course of session When selected produces list of the files with the extension vdm in the current directory which can be directly selected Alternatively selecting the item gives an edit box into which you type the file name in standard DOS notation terminating it with a Enter gt If you omit the file extension SpecBox assumes it to be vdm You can specify a file name without an extension by terminating the name with a Errors can be corrected using the 81 Pe and keys SpecBox checks that the specified file exists and that you have write access to it and displays an error message if that is not the case Pressing any key removes the message and allows the filename to be entered again You can change the default directory by selecting SpecBox User Manual version PC 2 21a 4 2 Utilities Change directory The normal conventions of for the 6 urrent directory and for the parent can be used The
18. which allows errors to be corrected using normal word processor functions Pressing concludes the edit session and causes the parse to recommence Once the input file is altered the system will ask the user whether to save the edited version before moving on to analyse the file If you do not wish to correct the error you can jump past it by selecting the option on the edit menu this causes parsing to start again at the beginning of the next major syntactic item in the file Once a syntactically correct file has been produced the top level menu will reappear with the item highlighted Selecting this option causes semantic analysis to commence Diagnostic information is displayed as this analysis proceeds at the end three new files are created a report file giving a summary of the analysis an annotated version of the input file indicating where semantic errors have occurred and a cross reference listing indicating where each declaration is made and used If any semantic errors have occurred they may be put right by selecting the item on the top menu before running the syntax checker and analyser again A syntactically correct file may be converted to the mathematical syntax by selecting the option on the SpecBox User Manual version PC 2 21a Method of operation 1 5 main menu This causes a file of ATpX commands to be generated that will print a document in the mathematical notation If only part of the sourc
19. 165 bracbind simplebind 166 simplebind typebind setbind 167 patbind setbind 167 p pattypebind 168 pattypebind pat typebind 169 typebind pat type 170 setbind pat in set expr P H H H D 171 multibind setmultibind typemultibind en 172 setmultibind pat pat in set expr en 173 typemultibind pat pat type 174 pat sequencepat recordpat tuplepat patidorval setpat SpecBox User Manual version PC 2 21a Bindings and Patterns 9 21 175 176 177 178 179 180 181 182 183 184 185 186 setpat simplesetpat setunionpat sequencepat seqpatid seqpatidpat idseqpat recordpat seqlitpat tuplepat patidorval patident simpleset pat setunionpat patidorval s pat 47 paid y setpat union setpat seqlitpat seqpatid seqpatidpat idseqpat e seqlitpat patident e seqlitpat patident seqlitpat e patident seglitpat mkidentifier pat pat 0 SP pat 7 paid 37 mk 7 pat pat yr patident matchval identifier e SpecBox User Manual version PC 2 21a 9 22 The SpecBox grammar 187 matchval matchvalue 188 matchvalue literal 7 expr yr 189 mkidentifier
20. 2 21a 6 2 The analyser The arity of the function f with the above type is n m that is it takes n input arguments and returns m results where n gt 0 m gt 1 The arity of so called curried functions may be determined similarly the arity then consists of a sequence of two or more input tuples paired up with the number of resulting output values 6 1 2 Operations Like functions VDM operations have an arity which can be derived from the associated type OP Ay x X Aj gt Ri x x Rm The arity of the operation OP with the above type is n m that is it takes n input arguments and returns m results where n gt 0 m gt 1 Unlike functions operations may not be curried 6 1 3 Records Associated with each VDM record definition of the form RTy x seh Ty sel Ty T is a family of selector functions which may be overloaded together with a construction function mk RTy which has SpecBox User Manual version PC 2 21a VDM quotation expressions 6 3 type mk RTy Ty x Ty gt RTy Each selector function sel has type sel RTy Ty 6 1 4 Type invariants A type invariant is a boolean predicate taking a single argument as input with type inv Ty Ty B where Ty is the unconstrained type which Ty is a subset of 6 1 5 State initialisation The initialisation predicate for a state is a boolean predicate taking a single argument as
21. 2 21a Bank Accounts 10 15 Bank example 1 1 module Bank 2 definitions 2 1 types 3 1 Acdata own Cno 3 bal Balance 4 1 Overdraft N 5 1 Balance Z 6 1 Cno is not yet defined 7 1 Acno is not yet defined 8 1 state Bank of 2 acm Aeno gt Acdata odm Cno 2 Overdraft 9 1 inv mk Bank acm odm A 2 V mk Acdata cno bal rng acm 3 cno dom odm bal gt odm cno 4 end 10 1 operations 11 1 NEWC od Overdraft r Cno 2 ext wr odm Cno gt Overdraft SpecBox User Manual version PC 2 21a 10 16 Illustrative examples 3 post A r dom odm 5 odm odm U r gt od 121 NEWAC cu Cno r Acno 2 ext rd odm Cno gt Overdraft 3 wr acm Acno gt Acdata 4 pre cu dom odm A post 6 r dom acm 7 acm acm U r mk Acdata cu 0 13 1 ACINF cu Cno r Acno Balance 2 ext rd acm Acno 5 Acdata 3 post A r 0000 acm acno bal 5 acno dom acm 6 acm acno own cu 7 14 1 end Bank SpecBox User Manual version PC 2 21a Binary Trees 10 17 10 6 Binary Trees This example concerning the reification of binary trees is taken from 1 pages 197 and 254 Notes e draft ISO VDM doesn t allow hooked variables to be defined within patterns as they are always associated with the old values of state variables e post FINDB is of arity 4 input old state new state and output e an is expression is used in INSERTB is
22. 7 1 functions 2 oe s D 3 ge a b A 4 a gt b 8 1 create Z Z create l A 3 do sort 1 9 1 add Z x 2 Z add elem 1 A SpecBox User Manual version PC 2 21a Instantiation and parameterization 11 19 10 1 Lp L do sort elem 1 delete Z x 2 2 delete elem 1 A if i then else if elem hdl then tll else hdi delete elem tll end mailing list SpecBox User Manual version PC 2 21a 11 20 Modules SpecBox User Manual version PC 2 21a 12 1 12 BIBLIOGRAPHY 1 C B Jones Systematic software development using VDM Second Edition Prentice Hall International 1990 2 Leslie Lamport ATEX user s guide and reference manual Addison Wesley 1986 3 C B Jones K D Jones P A Lindsay and R Moore mural A Formal Development Support System Springer Verlag 1991 Stephen Bear Structuring for the VDM Specification Language in VDM 88 VDM The Way Ahead R Bloomfield L Marshall and R Jones eds Lecture Notes in Computer Science no 328 pp 2 25 Springer Verlag 1988 SE G Blaue A Copy Rule Approach to the Semantics of BSI VDM Modules BSI IST 5 19 no 216 July 1991 c 6 John Dawes The VDM SL reference guide Pitman 1991 SpecBox User Manual version PC 2 21a 12 2 Bibliography SpecBox User Manual version PC 2 21a Index 13 1 13 INDEX 80386 version 2 2 8086 ve
23. Mnode module Tree definitions types Mrep Mnode Mnode It Mrep mkk Key md Data rt Mrep inv mk Mnode lt mkk md rt forall 1k in set collkeys 1t amp lk lt mkk and forall rk in set collkeys rt amp mkk lt rk Data is not yet defined SpecBox User Manual version PC 2 21a 10 18 Illustrative examples Key is not yet defined state State of t Mrep end functions collkeys Mrep gt set of Key collkeys t cases t nil gt 0 mk Mnode lt mkk md rt gt collkeys 1t union mkk union collkeys rt end operations FINDB k Key d Data ext rd t Mrep pre k in set collkeys t post let mk Mnode lt mkk md rt t in k mkk and d md or k gt mkk and post FINDB k lt lt d or mkk gt k and post FINDB k rt rt d INSERTB k Key d Data ext wr t Mrep pre k not in set collkeys t SpecBox User Manual version PC 2 21a Binary Trees 10 19 post t nil and t mk_Mnode nil k d nil or is_Mnode t and let mk_Mnode lt_old mkk md rt_old t in k lt mkk and exists lt_new Mrep amp post_INSERTB k d 1t_old lt_new and t mk Mnode 1t new mkk md rt old or mkk lt k and exists rt new Mrep amp post INSERTB k d rt old rt new and t mk Mnode l1t old mkk md rt new end Tree SpecBox User Manual version PC 2 21a 10 20 Illustrative examples Tree example 11 module Tree 2 definitions 2 1 types 2 Mrep
24. as follows e The following general classes abortstmt cases charlit defexpr dont_care fundefexplnyd fundefimplnyd funtype identstmt idseqpat interface isexpr istoken lambda letbeexpr letbind letexpr mapcomp matchval opdefexplnyd opdefexpl opdefimplnyd optionaltype optype quotetype quotlit ratlit recordpat recordtype reverse seqitype seqlitpat seqpatidpat seqpatid sequencecomp setcomp setinterval setpatidval simplesetpat stexpr stmt subsequence textlit tupleexpr tuplepat typevardecl typevariable e The following binary expressions arithmetic divide arithmetic mod arithmetic exponentiation arithmetic integer division map iterate map composition function iterate function composition less than or equal greater than or equal e The following unary expressions SpecBox User Manual version PC 2 21a Unsupported classes 8 3 unary plus unary minus arithmetic abs floor distributed set intersection distributed sequence concatenation distributed map merge e Curried explicit function definitions e Pre conditions in explicit function definitions e Exceptions in implicit operation definitions e The basic types Q char and token There are also the following restrictions e isnotyetdefn is supported only for types e State initialisation must be written in the form init s A s mk State e Single field selectors only are allowed SpecBox User Manual version
25. concern the structure of declarations and definitions and can arise when an inconsistency in this structure has been detected An example of this is when an explicit function is said to have two parameters in its type but its definition then gives three parameters instead C 1 Repeated global declaration of lt kind gt lt name gt A redeclaration has been encountered for a globally declared VDM object of type kind and called name C 2 Multiple local decl of pattern identifier lt name gt The named item is declared more than once in the same local declaring context This error generally arises within patterns in cases and formal parameter lists C 3 Local declaration s fail to bind any variables A local declaration i e binding or pattern match failed to define any variables in a context in which it is required to do so such as formal parameter lists and quantifiers C 4 MatchValue pattern occurs in an erroneous context The MatchValue pattern occurs inside a pattern expression where the overall context forbids its use SpecBox User Manual version PC 2 21a 6 10 The analyser For example Match Value patterns should not occur anywhere within the parameter lists of functions or operations On the other hand they are often used within cases patterns A typical cause for such an error is in having too many brackets in pattern expressions C 5 Arity mismatch for parameters of lt kind gt lt n
26. current directory is displayed at the bottom of the screen during file selection Pressing or clicking the right mouse button returns to the main menu without affecting any previously entered filename SpecBox will load a file at startup if it is invoked with the command line specbox f lt filename gt or specbox f lt filename gt 4 2 External edits Top level menu ExterNal edit This function enables you to correct semantic errors without leaving SpecBox by giving access to an external editor of your choice External editing can also be used to put right syntax errors that cannot be corrected using SpecBox s internal editor The path to the editor is set up using the command described in Section 4 3 When ExterNal edit is selected the screen blanks and control is passed to the external editor which is instructed to SpecBox User Manual version PC 2 21a Configuration 4 3 load the input file to SpecBox The editor is then used in the normal way When the edit is complete and the file saved leaving the editor causes SpecBox to resume operation Since errors may have been introduced during editing SpecBox insists on carrying out syntax checking again on any file that has been externally edited even if it was syntactically correct before 4 3 Configuration Top level menu The configuration command allows you to select whether or not
27. is read into the built in editor and the top level menu reappears with the item highlighted with other syntactic units that can be analysed such as operation definition and expression displayed below The analysis does not have to begin at the start of the input file the built in editor can be used to position the start of the analysis anywhere in the file Selecting the appropriate syntactic unit causes parsing to commence The input file is listed to the screen as the analysis progresses If parsing is successful the message CHECK OK is displayed and the system returns to the top level display If a syntax error is encountered a beep is emitted and an error banner is displayed towards the bottom of the screen with diagnostic information below it The listing pauses at the word or symbol that caused the problem with the offending token highlighted The correction menu that appears contains alternative tokens as well as a general edit option usually the error is fairly simple to correct and the required token is SpecBox User Manual version PC 2 21a 1 4 Introduction selected from the menu which automatically replaces the highlighted one on the screen If necessary the structure of the grammar can be interrogated to determine which token is correct Alternatively the option can be chosen if the error is such the required replacement does not appear on the menu Whichever course is chosen the system is put into edit mode
28. mktoken 9 13 Identifiers and basic tokens 190 identifier tokenitem 191 tokenitem nametoken quotlit mktoken istoken pretoken posttoken invtoken inittoken 192 nametoken LEXICAL ITEM 193 quotlit LEXICAL ITEM 194 mktoken LEXICAL ITEM 195 istoken LEXICAL ITEM 196 pretoken LEXICAL ITEM 197 posttoken LEXICAL ITEM SpecBox User Manual version PC 2 21a Identifiers and basic tokens 9 23 198 invtoken LEXICAL ITEM 199 inittoken LEXICAL ITEM 200 literal boollit intlit ratlit charlit textlit nil 201 boollit true false 202 intlit LEXICAL ITEM 203 ratlit LEXICAL ITEM 204 charlit LEXICAL ITEM 205 textlit LEXICAL ITEM SpecBox User Manual version PC 2 21a 9 24 The SpecBox grammar 9 14 Index to the grammar allquant 130 elsifstmt 104 always 110 emptymap 139 applyexpr 9 emptyset 136 assignment 9 emptytype 43 equalsdefn 86 basictype 44 exception 77 binaryop 127 existsquant 131 bind 164 existsuniquequant 129 binexpr 126 exit 115 block 83 expr 116 boollit 201 bracbind 165 bracexpr 162 bractype 48 exprorcallstmt 93 externals 74 extvar 75 field 1 callstmt 94 fieldid 157 cases 151 fieldmod 147 casesaltn 2 fieldselect 155 casesstmt 106 forloops 7 casesstmtaltn 7 fundef 58 charlit 204 fundefbody 67 comppred 141 fundefcont 66 fundefexpl 65 fundefexplnyd 68 fundefim
29. sty to place the keywords printed in the keyword fount around the comment If you wish to distinguish annotations in some other way you may redefine the annotation environment appropriately instructions for redefining IATpX environments are given in 2 SpecBox User Manual version PC 2 21a 9 34 The SpecBox grammar Symbols The following table describes the ASCII representation of the VDM mathematical symbols and the equivalent mathematical form where the two differ significantly SpecBox User Manual version PC 2 21a Lexical rules 9 35 Ascii Math Ascii Math x T power F amp set of t t set x seq of 1 seqi of t tt lt lt inmap atob a gt b gt 2 map ato b a Zb gt lt 7 iota L gt 5 Lambda gt mu 7 gt bool B gt gt nat N lt gt e nati lt int Z A rat Q 1 real R i not A gt inter n gt gt union sets U lt 4 merge maps U gt gt in set munion not in set g psubset C comp o subset C and A 0 or V dinter N forall V dunion U exists J inverse 1 existsi 3 SpecBox User Manual version PC 2 21a 9 36 The SpecBox grammar SpecBox User Manual version PC 2 21a 10 ILLUSTRATIVE EXAMPLES This section contains some examples of VDM specifications written using the draft ISO VDM grammar They include a commentary on the differences between this grammar and that used in 1 The examples are
30. version PC 2 21a 1 1 1 INTRODUCTION SpecBox enables you to check formal specifications written in draft ISO VDM for syntax errors and certain semantic errors This User Manual gives comprehensive instructions for the operation of SpecBox It also describes the VDM grammar used by SpecBox giving the concrete syntax and some illustrative examples Firstly however the structure of SpecBox and its mode of working are briefly outlined l l Overview The structure of SpecBox is illustrated schematically in Figure 1 It is composed of the syntax checker the analyser the IATgX generator and the Mural translator plus a top level program that invokes these as required and provides file selection external editing and configuration The syntax checker reads the input file in ASCII format and analyses it to produce a parse tree If the file contains a syntax error an error message is displayed together with some diagnostic information The built in editor can then be used to correct the error or an external editor can be used for major changes A log file is produced of each parsing session When the input file is syntactically correct the parse tree is examined by the analyser for various semantic errors Diagnostic messages are displayed on the screen while this analysis is taking place and a report file an annotated listing and a cross reference file are produced SpecBox will also generate a file of ATEX macros to display
31. will not stop on them and their quick keys are not effective Help on the currently highlighted item is obtained by pressing r1 the help system is described more fully below Most menus can be cancelled by pressing or clicking the right mouse button the only exceptions are those where no clear default action exists 3 2 The help system SpecBox has a comprehensive help system that provides information and guidance at all stages of its operation The help information is arranged as a tree with each node containing some help text and a menu leading further down the tree the leaves have empty menus The menus also allow direct access to the root symbolised by V in the menus and to the last help item selected You can invoke the help system by pressing at any time or by selecting the item from the top level menu The help obtained by pressing depends upon the state of the system in the following way at a menu The help is specific to the highlighted item in most cases The exception occurs at menus that ask for confirmation of a specific command or situation e g Save altered file or End of text where the help SpecBox User Manual version PC 2 21a Displays 3 3 explains the reasons for the question and the consequences of the alternatives at an edit box The help summarises the edit commands in the built in editor The help summarises the edit commands and also provides access to a list of the VDM reserv
32. 1 field identifier type 42 optype typety gt typety 43 emptytype 7 yr 44 basictype bool nat nati int rat real char token 45 quotetype quotlit 46 typename identifier identifier SpecBox User Manual version PC 2 21a State definition 47 48 9 6 49 9 7 53 54 55 9 8 56 typevariable bractype State definition stateinfo invariant invinitdefn isnotyetdefn Constant definitions valuedefn valuedefncont valuedef Function definitions fundefn 9 7 identifier 7 type state identifier of field field invariant init invinitdefn end inv invinitdefn e 7 pat expr is not yet defined identifier type valuedefncont valuedef isnotyetdefn e 0 Z 3 expr identifier typevardecl fundef SpecBox User Manual version PC 2 21a 9 8 The SpecBox grammar 57 typevardecl typevariable typevariable 58 fundef fundefimpl fundefimplnyd fundefexpl 59 fundefimpl pattypeparams idtypepair precond postcond 60 fundefimplnyd pattypeparams idtypepair isnotyetdefn 61 pattypeparams typebind typebind yr 62 idtypepair identifier
33. SpecBox is invoked it will analyse each of the files in turn It will firstly carry out syntactic checking jumping past any errors that are encountered in exactly the same way as the continue facility In batch mode SpecBox writes a log file of the checking session with the file extension Log If there are no syntactic mistakes SpecBox normally goes on to semantic analysis and IATpX generation and if there are no semantic errors it will perform Mural translation The extent of analysis in batch mode can be restricted by using one or more of the following switches on the command line SpecBox User Manual version PC 2 21a Batch processing 3 5 s syntax check only a syntax check and semantic analysis only 1 syntax check and JATpX generation only m syntax check semantic analysis and Mural translation only All switches can alternatively be written x During batch processing BATCH MODE is displayed at the bottom left of the screen When batch processing is complete and if all the files were successfully opened SpecBox returns to the operating system If SpecBox was unable to open any of the files in the list an error message is printed containing the names of the files not analysed Batch mode can be aborted by pressing or clicking the right mouse button in which case SpecBox goes into interactive mode SpecBox User Manual version PC 2 21a 3 6 General features SpecBox User Manual
34. SpecBox will beep if it detects an error to specify the path to an external editor to select the disk to be used for storing large parse trees 8086 version or the temporary subdirectory 80386 version to enable use of the mouse and to disable cross reference sorting When is selected an edit box appears headed Editor pathname with the path to any editor previously set up shown in the box Enter the pathname of the editor in standard DOS format and terminate the entry using the key or press or alone or click the right mouse button to use the existing path The editor is called with this pathname followed on the same command line by the input file selected using the SpecBox command SpecBox does not check that the specified path exists and will give the Dos error Bad command or filename when the ExterNal edit command is called if it does not SpecBox User Manual version PC 2 21a 4 4 Utilities If you wish to disable the external edit function clear the pathname using the key and then press Enter When the external editor has been specified another edit box appears headed Beep on or off Enter on or off according to whether or not you want an audible warning of an error such as an incorrect input file specification or a syntax error in the input file Press or alone or click the right mouse button to retain the old setting SpecBox will only accept the words on and off in response to this item Next
35. SpecaBox User Manual Adelard 1996 All rights reserved worldwide The software described in this document is furnished under a licence and may be used or copied only in accordance with the terms of such a licence No part of this publication may be copied or distributed transmitted transcribed stored in a retrieval system or translated into any human or computer language in any form or by any means electronic mechanical magnetic manual or otherwise or disclosed to third parties without the express written permission of Adelard Manual version PC 2 21a 21st May 1996 Adelard Coborn House 3 Coborn Road London E3 2DA UK Telephone 44 0 181 983 1708 Fax 44 0 181 983 1845 All trademarks acknowledged Contents i CONTENTS Introduction 1 1 1 1 Overview 1 1 1 2 Method of operation 1 3 Installation 2 1 2 1 General 2 1 2 2 Use of a mouse 2 1 2 3 PC versions 2 2 General features 3 1 3 1 The menu system 3 1 3 2 The help system 3 2 3 3 Displays 3 3 3 4 Aborting the current activity 3 3 3 5 Batch processing 3 4 Utilities 4 1 4 1 Selecting the input file 4 1 4 2 External edits 4 2 4 3 Configuration
36. able area Moving the cursor to the right of SpecBox User Manual version PC 2 21a Editor 5 13 or below its original position will cause the block to terminate at the cursor moving the cursor above or to the left of its original position does not affect the block All the cursor movement keys can be used to position the block as required The selected area cannot extend beyond the top of the screen so only the visible highlighted area is affected by the delete operation Pressing causes the highlighted block to be deleted from the text and stored in the insert buffer Pressing cancels the operation Pressing has the same effect as D except that the selected area is not deleted Pressing inserts the contents of the insert buffer immediately before the cursor position and can thus be used for both copying and undeleting text With the mouse text can be deleted by clicking the left button at the start of the area then clicking Delete in the menu bar at the bottom of the screen A block indicated by a different colour on a colour screen or reverse video on a monochrome screen will appear running from the cursor to the end of the editable area Clicking the mouse to the right of or below its original position will cause the block to terminate at that point clicking above or to the left of its original position does not affect the block Clicking Delete again causes the highlighted block to be deleted f
37. ame gt The explicit definition of an object either function or operation was given using a different number of arguments to that specified elsewhere in its declaration i e its type C 6 Mismatched names in the definition of explicit lt kind gt lt name gt The explicit definition of object either function or operation was given using conflicting names to that specified elsewhere in its declaration i e its type State variable related errors VDM provides a model based formalism that makes central use of the notion of state variable Such variables are intended to characterise a system by the way they are used to retain information As such VDM has a number of useful notational conventions concerning the use of state variables in specifications The errors Classified under this section are thus related to the SpecBox User Manual version PC 2 21a Error messages 6 11 checking of these conventions D 1 Attempted use of lt name gt as state variable This error arises when a named item is used as though it were a state variable when it has not been globally declared as such Note that this error can only arise when a global state definition has also been given in the specification D 2 State variable lt name gt has read only access The declared state variable name was specified to have read only access In such cases explicitly referring to its old value is regarded as an error This is b
38. ans k i mod l m i c 141 DECODE t Letter m Letter 2 ext rde Pcode 3 rdk Key 4 post lenm lent A 5 let maxs domk Lin 6 Vicindst t 1 ptrans k i mod l m i c end Code 15 1 SpecBox User Manual version PC 2 21a Bank Accounts 10 13 10 5 Bank Accounts This example is from 1 starting on page 148 Note that the types Acno etc have been added and that the dot notation has to be used to reference fields in a composite object e g acm acno bal module Bank definitions types Acdata own Cno bal Balance Overdraft nat Balance int Cno is not yet defined Acno is not yet defined state Bank of acm map Acno to Acdata odm map Cno to Overdraft inv mk_Bank acm odm forall mk_Acdata cno bal in set rng acm amp cno in set dom odm and bal gt odm cno SpecBox User Manual version PC 2 21a 10 14 Illustrative examples end operations NEWC od Overdraft r Cno ext wr odm map Cno to Overdraft post r not in set dom odm and odm odm union r gt od NEWAC cu Cno r Acno ext rd odm map Cno to Overdraft wr acm map Acno to Acdata pre cu in set dom odm post r not in set dom acm and acm acm union r gt mk_Acdata cu 0 ACINF cu Cno r map Acno to Balance ext rd acm map Acno to Acdata post r 4i acno gt acm acno bal acno in set dom acm amp acm acno own cu end Bank SpecBox User Manual version PC
39. antiation and parameterization 11 15 9 1 module CDICT 2 parameters 3 types dC AttribsC Two parameters again 10 1 instantiation 2 ILDICT as LDICT Id IdC Attribs AttribsC 3 types A State 5 operations 6 LOOKUPL IdC gt AttribsC 7 STOREL IdC x AttribsC gt 8 ISINL IdC 58 11 1 exports 2 operations 3 ENTER gt 4 LEAVE 5 5 STORE IC x AttribsC gt 6 ISLOC IC B 7 LOOKUPC IC AttribsC 12 1 definitions 2 types 3 Cdict ILDICT State Necessary use of name qualification 13 1 state 2 State of cd Cdict 3 init mk State cdo A cdo A end 14 1 functions 2 mins N set N SpecBox User Manual version PC 2 21a 11 16 Modules 3 mins s is not yet defined 15 1 operations 2 STORE i Id a Attribs 3 ext wr cd Cdict 4 pre cd Z pre STOREL i a hd cd 5 post let 600 ed in 6 id ILDICT State 7 post STOREL i a hd cd0 Id 8 cd id tl edd 16 1 15200 i Id r B 2 ext rd cd Cdict 3 pre cd F A post post ISINL i hd cd hd cd r 17 1 LOOKUPC i Id r Attribs 2 ext rd cd Cdict 3 pre J j inds cd pre LOOKUPL i cd j A post let k mins pre LOOKUPL 1 cd j j ND 5 in 6 post LOOKUPL 1 cd k cd k r 18 1 ENTER 2 ext wr cd 1 3 post J cdo Cdict ILDICT init State cdo A ed edo cd 19 1 LEAVE 2 ext wr cd 1 3 pre cd F 4 post cd tl cd SpecBox U
40. as PModNm2 ParmBind2 Por fon Mod Sig etc exports Declaration of publicly visible entities defined within module ExpModSig definitions All items declared by this module end ModNm Note the following e If the parameter part is missing a standard module is defined the objects it exports are used in other modules by means of an imports clause e The imports clause serves the same purpose as the package specification in Ada However an imports clause must always be provided where objects from another module as to be used there is no equivalent of the Ada with ImpModNm e In the imports clause the names ImpModNm should all be names of standard i e non parameterized modules SpecBox User Manual version PC 2 21a Background 11 7 e If parameters are given the module becomes a parameterized module Parameterized modules are used in other modules by means of an instantiation clause in an analogous way to Ada generic packages e The names of parameters should not clash with other items defined by the module e In the instantiation clause the names PModNm must name a specific parameterized module The binding names in the ParmBinding are the names of the formal parameters of the associated module e The modules ModNm must be unique within the scope of the module importing them e The names InstModNm U ImpModNm must be unique e The names PModNm need not be unique
41. ates 6 3 1 Local declarations The VDM specification language has several ways of introducing local identifiers that have textually limited regions of scope Moreover these ways arise syntactically whenever a pattern can be used e use of state variables in operations e formal parameters to operations amp functions quantifiers lambda and iota expressions statement declaration forms dcl and def that introduce assignable local variables let and let be constructs case constructs SpecBox User Manual version PC 2 21a Error messages 6 7 6 4 Error messages During analysis various errors and problems with the given specification may be encountered As a result various messages are generated and sent to the screen and also to the listing file The messages are as follows Arity errors Such errors arise when the number of arguments to an operation or function call do not correspond to the arity given by declaration 4 1 Incorrect number of arguments for lt name gt The item was declared but its use is inconsistent with the declaration e g function application length of tuples Incorrect usage errors Such errors arise in misusing VDM objects in some way One example of misuse is to use an item that has not been declared Another is the attempt to use a state variable in a context in which it has not been imported B 1 Undeclared identifier lt name gt expecting lt class gt The specified obj
42. ax requires that each module is terminated with the original name of the module that it is finishing Warnings In SpecBox an error is typically something that has to be put right and counts strictly as evidence for a mistake having been SpecBox User Manual version PC 2 21a Caveats 6 13 made On the other hand there are occasions where the term error would not be strictly correct but where there is evidence that something is potentially wrong or that it has been misunderstood In such cases a warning message is given in place of an error W 1 Redeclaring local variable lt name gt potential typographical mistake A redeclaration of a local variable has been encountered This may be correct and intentional but it may indicate an error W 2 Operation name delivers results to statement At present in draft ISO VDM operations called directly from a statement should not return results i e they are operations having only pure side effects A value returning operation should be called from appropriate binding statements such as dcl or let statements 6 5 Caveats The notion of arity is an approximation to the general set theoretical notion of type used within VDM This technique can only check that the number of parameters supplied to a function or operation matches that required by its definition As an example of what it cannot yet do is to ensure that the SpecBox User Manual versi
43. blem As a matter of design policy the analyser reports each error at most once per phrase and line Where possible the analyser attempts to suppress misleading cascade errors which tend to confuse and obscure the possible cause of an error File Description lt filename gt lst 6 9 Cross reference file This file contains a cross reference listing of the global identifiers used on a module by module basis Where possible declaration sites are also noted File Description lt filename gt xrf SpecBox User Manual version PC 2 21a 6 16 The analyser SpecBox User Manual version PC 2 21a 7 1 7 IATEX GENERATOR Top level menu The BTEX generator converts the ASCII source file to ATpX macros that display the specification in draft ISO VDM mathematical syntax For details of the IATEX document preparation system refer to 2 7 1 General operation The BTEX generator is invoked by selecting Latex The IATpX output file is named by replacing the extension of the source file by tex The generation process only affects that portion of the source file that has been most recently parsed the remainder of the file is copied unchanged The BTEX generator carries out lexical conversion from the ASCII source to IA3TpX macros that print mathematical symbols as defined in 9 17 7 2 Formatting SpecBox uses formatting information in the source file to lay o
44. ccurs and recommending the appropriate change SpecBox User Manual version PC 2 21a 10 4 Illustrative examples 10 3 Telegram analysis This example is from 1 page 201 Notes e in is a keyword so is changed to inpt here e The position of the binding in the set comprehension is different from 1 module Telegram definitions types Input seq of Telegram Telegram seq of Word inv t t gt lt Word seq of char inv w w gt lt and w lt gt zzzz Output seq of Report Report tgm Telegram count int ovlen bool SpecBox User Manual version PC 2 21a Telegram analysis 10 5 functions analyse_telegram Telegram gt Report analyse_telegram wordl mk Report wordl charge_words wordl check words wordl charge_words Telegram gt int charge_words wordl card j j in set inds wordl amp wordl j gt lt STOP check_words Telegram gt bool check_words wordl exists w in set elems wordl amp len w gt 12 operations ANALYSE inpt Input out Output post len out len inpt and forall i in set inds inpt amp out i analyse_telegram inpt i end Telegram SpecBox User Manual version PC 2 21a 10 6 Illustrative examples Telgram analysis example 1 1 module Telegram 2 definitions 2 1 types 3 1 Input Telegram 41 Telegram Word 2 mtAt TE 5 1 Word char inv w A 3 w UU A w uzi
45. chy may make use of various facilities provided by other modules either by instantiating parameterized modules or by importing modules All names in draft ISO VDM specifications have a full version of the form Mod Id where Mod is the name of the module where d is defined This differs from the proposal in 4 which had a third component for an instantiation This form is valid even where Id is defined internally to the module It is only mandatory however where it is necessary to disambiguate two items with the same rootname in the same way as an Ada procedure preceded by use MOD There is no facility for introducing local nicknames of items imported Note that the use hierarchy is not recursive and so there is no mutual recursion between items defined in separate modules 1 Not currently supported by SpecBox SpecBox User Manual version PC 2 21a 11 4 Modules Of course mutual recursion is permitted between items that are defined in the same module The module scheme contains a syntactic class called a document which is composed of a sequence of modules The scope of the objects exported by a module is restricted to the document The top level module should be the only module not used by any other module contained in the document it will often be the last one in the list of modules comprising the document 11 1 3 Importing modules The simple way of using objects defined in other modules is by im
46. cter literals 8 32 comments 3 identifiers 0 9 2 text literals 8 32 operator precedence log file 1 1 8 29 terminals 5 5 5 7 mathematical symbols 8 34 help system 1 2 3 2 menu 1 highlighting bar 3 1 cancelling 3 2 hooked values 0 correction 1 3 5 4 installation 1 5 5 complete option LaTeX generator 1 1 9 6 1 4 7 1 edit option 5 6 5 9 grammar option 5 7 insert mode option 5 9 skip option 5 9 help on 3 2 items allowed 2 scrolling 3 1 toplevel 1 3 message analyser error 7 BATCH MODE 3 5 CHECK OK 1 3 5 2 SpecBox User Manual version PC 2 21a Index 13 3 continue option warning 5 9 current line number 5 2 diagnostic 1 3 5 4 End of text 5 3 FINISHED 5 9 line number 5 9 Quit 3 3 Save altered file 5 3 5 5 Microsoft Windows 2 1 2 2 modules 1 as abstract data types 10 2 exports 10 12 imports 10 4 10 12 instantiation 10 5 10 13 interface 10 5 parameterized 10 5 10 13 sharing 10 8 use of 3 mouse 2 1 Mural 2 parse tree 2 path command 2 1 quick key 1 report file 1 1 1 4 6 14 skip option 4 source file changed by editor 5 3 selecting 1 3 4 1 in batch mode 4 standard version 3 starting SpecBox 3 stylistic conventions 9 1 syntactic units 1 3 5 1 syntax checker 1 1 5 1 action on error 5 4 adding text 5 5 correcting text 5 5 insertion point 5 4 log file 5 3 options 5 1 start point 5 3 syntax error 1 3 virtual dri
47. cument vdmmodule vdmmodule defnblock defnblock 9 3 Modules 2 vdmmodule module identifier parameters modsig imports importclause importclause instantiation instclause instclause exports modsig definitions defnblock defnblock end identifier 3 importclause from identifier modsig 4 instclause identifier as instance 5 instance identifier substitute substitute modsig SpecBox User Manual version PC 2 21a Modules 9 3 6 12 13 14 15 16 17 substitute modsig modsigitem typesigmap typedescr valuesigmap idvaluesig funsigmap idfunsig opsigmap opsig defnblock identifier gt identifier identifier modsigitem typesigmap valuesigmap funsigmap opsigmap HEEM LE types typedescr typedescr identifier typedef values idvaluesig idvaluesig HEEM LE identifier identifier type HEEM functions idfunsig Jr idfunsig identifier identifier funtype 66 22 operations opsig opsig identifier identifier optype using identifier typedefns SpecBox User Manual version PC 2 21a 9 4 The SpecBox grammar stateinf
48. d 0 147 fieldmod identifier gt expr 148 lambda lambda typebind typebind amp expr 149 ifexpr f expr then expr elsifexpr else expr 150 elsifexpr elsif expr then expr 151 cases cases expr casesaltn casesaltn othersexpr end SpecBox User Manual version PC 2 21a Expressions 9 19 HEEM en E cases expr casesaltn 1 casesaltn othersexpr end H 152 casesaltn pat 4 pat gt expr pat gt expr e 0 e 14 H H D 153 othersexpr others gt expr 154 isexpr istoken expr 155 fieldselect expr fieldid fieldid 156 polyfuninst expr type type T 157 fieldid identifier ef LG 0 14 e 0 expr expr 7 4 7 YT expr 158 subsequence 159 applyexpr expr type type expr 5 expr 0 160 nameexpr oldvarname identifier identifier 161 oldvarname identifier 162 bracexpr expr 163 tupleexpr mk expr expr SpecBox User Manual version PC 2 21a 9 20 The SpecBox grammar 9 12 Bindings and Patterns 164 bind bracbind simplebind 1 DTM 1 1 6677 m H H
49. d before the highlighted token or to replace the highlighted token depending on the setting of the insertion mode Otherwise the terminal will be placed at the end of the text If the token is enclosed in angled brackets it is a variable Selecting a variable causes an edit box to be invoked into which the required token should be input The choice of nonterminal is used to restrict the choices offered by the menu item as the parse progresses The choice provided is intended as an illustration of the basic shape of the grammar at that point and usually omits some or all of the optional items The selection offered by the option can of course be overridden by entering any syntactically correct token via the editor or by returning SpecBox User Manual version PC 2 21a 5 8 The syntax checker to the correction menu and selecting a terminal from there As an example suppose you reach a point in your specification where expr is expected If you select you will be offered a list of nonterminals that includes subsequence Suppose you select this enter the editor type foo then reparse After foo is checked a new correction menu will appear giving all possible terminals which include C binary operator However if you select again the only choice presented will be as this is the shortest route to a subsequence The selection process nests so that if you selected subsequence oldvarna
50. e file has been syntactically checked this section will be converted and the remainder will be copied unchanged SpecBox can also be run in batch mode by giving it a list of files to be analysed It will check the syntax of each in turn jumping past any errors that occur and writing the results to the log file If there are no syntactic mistakes SpecBox will go on to semantic analysis and BTEX generation and if there are no semantic errors it will perform Mural translation SpecBox User Manual version PC 2 21a 1 6 Introduction SpecBox User Manual version PC 2 21a 2 1 2 INSTALLATION 2 1 General SpecBox runs under Microsoft MS DOS 3 2 and higher Installing SpecBox merely involves making a directory called specbox on your hard disk and copying the diskette supplied into it You will probably wish to use SpecBox from other directories so you should amend the path command in autoexec bat accordingly Your config sys file must contain the command files 20 or you will get system errors during startup Once you have added this line to the file you must reboot the machine so that it takes effect It may be necessary to increase the number of files in this command to 30 or 40 when running SpecBox in a multi tasking environment such as Microsoft Windows 2 2 Use of a mouse SpecBox can be used with a Microsoft compatible mouse The menu item can be used to enable or disable the use of a mouse Enabling the mou
51. e whether the correct end of the parse is reached or not The correction menu is headed Syntax error if an error is detected Insert text at an insertion point or the end of the file or End of text if the end of the parse may have been reached The correction menu contains the items Edit complete Gramer and Insert mods 0 owed by a list of possible grammar terminals The syntax check can be abandoned at this point by pressing or clicking the right mouse button If you have previously made changes to the input file another menu will appear headed Save altered file select or according to whether or not you wish to preserve the edits If you save the edits the original file is renamed with the extension bak The grammar terminals are generally listed as the terminal strings expected e g or lt identifier gt but binary e g lt gt and union and unary e g not hd operators are summarised as lt binary operator gt and lt unary operator gt SpecBox User Manual version PC 2 21a 5 6 The syntax checker Selecting a replacement token inserts it before the highlighted token or replaces the highlighted token with it according to the insertion mode selected If the token is enclosed in angled brackets it is a variable selecting a variable causes an edit box to be invoked into which the required token should be input The built in editor is then invoked as described in Sectio
52. ecause such reference implies the potential for changing the value of a read only variable which is clearly absurd D 3 Global state variable lt name gt is inaccessible The declared state variable called name was not mentioned as being accessible to the operation where external clauses have been specified D 4 Old value of lt name gt used incorrectly This error arises when use is made of the hook notation for the old value of a variable outside a VDM post condition such as within the pre condition to an operation or inside an explicitly defined operation SpecBox User Manual version PC 2 21a 6 12 The analyser Module naming errors These errors are associated with the names of modules and the items they define E 1 Module name lt name gt clashes with global declaration In VDM all objects need to have a corresponding type including the pre and post conditions of operations When these are exported from a module the type of the state component is assumed to have the same name as the module since the actual state type may not have otherwise been exported This implies that the state type of a module is always externally visible even though the state type is given a different name internally Finally it means that no other globally declared objects in a module can be given the same name as the module that contains them E 2 Terminating module identifier not equal to lt name gt The module synt
53. ect name was not declared either locally or globally The context was expecting an object described by class SpecBox User Manual version PC 2 21a 6 8 The analyser B 2 Incorrect use of lt object gt lt expectation gt This error arises when for instance a declared named value is used within a type expression usage that is inconsistent with its declaration The object indicates what has been found and when present the expectation indicates what the context required B 3 Item lt name gt is not declared as a record type no mk constructor function declared A constructor mk function has been used for an item that is not a composite object This arises when for instance a constructor function of the form mk name has been used where name is not a known record type B 4 Non record type or basic type lt name gt in is expression The is expression is name ezpr has been used where name is neither a basic type nor a known record type B 5 Item name not declared as a field selector An undeclared field called name for some composite object has been referenced B 6 Selector lt name gt used incorrectly as a value use dot notation to apply selector Fields in composite objects should be selected by the dot notation rather than by using the selector name as a function SpecBox User Manual version PC 2 21a Error messages 6 9 Definition and declaration structure errors Such errors
54. ed keywords during analysis The help provides general information on the operation in progress Leave the help system by typing or clicking the right mouse button 3 3 Displays SpecBox uses the bottom two lines of the display for informative messages during analysis Generally the input filename is displayed on the left of the upper of these with the remainder reserved for specific error help and status messages these are described fully in sections 5 to 7 A G in the upper right hand corner of the display indicates that garbage collection is in progress 3 4 Aborting the current activity Syntax checking semantic analysis ATEX generation and Mural translation can be abandoned by pressing or clicking the right mouse button A menu headed Quit will SpecBox User Manual version PC 2 21a 3 4 General features appear select to return to the main menu or to continue the activity 3 5 Batch processing SpecBox can be run in batch mode as well as the more normal interactive mode To carry out batch analysis set up a file containing a list of the files to be analysed the list should be separated by spaces and may continue over several lines The file names should obey the conventions described in Section 4 1 In order to run in batch mode SpecBox must be invoked using the command line specbox b lt filename gt where lt filename gt is the file containing the list of files for analysis When
55. ers 3 types Id Attribs Two parameters defined exports operations STOREL Id x Attribs ISINL Id 5 B LOOKUPL Id Attribs types State Nou bi 3 1 definitions 2 types 3 Ldict Id gt Attribs 4 1 state 2 State of ld Ldict 3 init mk State Ido A ldo A end SpecBox User Manual version PC 2 21a 11 14 Modules 5 1 operations 2 STOREL i Id a Attribs 3 ext wr ld Ldict 4 pre i domld 5 post ld Id U i ai 6 1 ISINL i Id r B ext rd ld Ldict 3 post r amp i dom ld 7 1 LOOKUPL i Id r Attribs 2 ext rd ld Ldict 3 pre dom ld post r ld i 8 1 end LDICT The definition of EDICT can now be used in the definition of the main operations contained in another parameterized module CDICT Note that according to 4 the state may be implicitly exported and imported but only if it has the same name as the module which is not the case here We do assume however that the pre and post conditions of the instantiated operations are imported we do not need to use their full names when referring to them since they do not clash with any names in CDICT The use of the same name for the state and the module would make it clearer that the module was an abstract data type however However from the maintenance point of view it might be better to use the full names for all imported objects SpecBox User Manual version PC 2 21a Inst
56. g for all cno1 cno2 in set dom m amp cnoi lt gt cno2 in forming compound identifiers Do not use e g upper limit the underscore _ is used instead e g upper_limit This generalizes also to quotation of pre post conditions as in post findb Tests for the type of a variable are carried out by an is expression e g is_real X Local variables do need to be introduced e g via quantifiers or as formal parameters to operations etc Undeclared variables will be picked up by the semantic analyser The specifier is not permitted to define type operators directly in draft ISO VDM So for instance types cannot be of the form Bag X However the parameterised module facility allows one to import parameterised abstract data types to achieve the same effect see Section 11 Do not use reserved keywords such as end by mistake it is worth spending a little time learning the keywords If you can t remember them while using SpecBox they are provided in the help facility SpecBox User Manual version PC 2 21a Notes on the ASCII syntax 10 3 The ASCII representations for the mathematical symbols are mainly given by compound symbols and are listed in Section 9 17 Again it is well worth spending some time familiarizing yourself with the ASCII syntax for these symbols Do not confuse is defined as with mathematical equality Fortunately the parser is good at spotting when this o
57. g the Ds Home and End keys 4 4 DOS DOS The item allows you to access the operating system without unloading SpecBox Type exit to return to SpecBox SpecBox User Manual version PC 2 21a 4 6 Utilities SpecBox User Manual version PC 2 21a 5 1 5 THE SYNTAX CHECKER The syntax checker parses the input file constructing a parse tree in the process that is then used by the analyser Section 6 to locate semantic errors The syntax checker examines the source file for conformance to the grammar given in Section 9 5 1 Syntax checker options The syntax checker allows you to check the syntax of a complete module or of smaller syntactic units It also enables you to select the position in the file where checking is to begin If you wish to return to the start of the file during the course of syntax checking reselect the file name using the item on the top level menu or select the built in editor using the item and press followed by F8 Syntactic units Top level menu Selecting one of these menu items allows you to check for conformance to the appropriate nonterminal in the grammar SpecBox User Manual version PC 2 21a 5 2 The syntax checker as follows Menu item Syntactic unit Module vdmmodule Type definition typedefn State stateinfo Constant definition valuedefn Function definition fundefn Operation definition opdefn Expression expr
58. heck reaches this point it pauses and the correction menu is displayed thus allowing you to select possible tokens from the correction menu using the grammar interrogation feature if required or insert text using the built in editor An insertion point is placed in the file from the built in editor by pressing F7 or clicking the text Insert point with the mouse A file can contain several insertion points An insertion point can be removed by deleting it by means of the editor in the same way as any other character See Section 5 7 for more information on the built in editor SpecBox treats the end of the file in exactly the same way as an insertion point 5 5 Action on error If a syntax error is encountered the erroneous token is highlighted an error banner is displayed and a beep sounds if the system is configured with beep on A diagnostic message such as Erroneous token midule is displayed at the bottom of the screen and the correction menu is displayed SpecBox User Manual version PC 2 21a Adding and correcting text 5 5 SpecBox treats the end of the file as an insertion point rather than an error and does not display the error message if it is encountered before the end of the check 5 6 Adding and correcting text Adding and correcting text is controlled by the correction menu which is displayed when the checker encounters a syntax error an insertion point the end of the file or if it is not sur
59. in style file bsivdm sty in the version dated 30th March 1989 14 38 written by Mario Wolczko of the Department of Computer Science University of Manchester Oxford Road Manchester M13 9PL United Kingdom sb sty is compatible with bsivdm sty when they are invoked together SpecBox uses the commands Forall Exists and minus instead of the normal TEX commands forall exists and SpecBox User Manual version PC 2 21a 8 1 8 MURAL TRANSLATOR The Mural translator enables syntactically and semantically correct specifications to be transmitted to the Mural VDM support tool so that proof obligations relating to the specification may be generated and discharged The specification is transmitted to Mural by Smalltalk code contained in a file named by replacing the extension of the source file by mur The user is referred to 3 for a complete description of the Mural system 8 1 Syntactic variants SpecBox will translate syntactic variants into the form recognized by Mural Thus for example a Z b Ze is translated as SpecBox User Manual version PC 2 21a 8 2 Mural translator 8 2 Unsupported classes Mural does not currently support the complete draft ISO VDM specification language A warning message is produced if any unsupported syntactic classes are encountered and generally the translated specification will not be acceptable to Mural The unsupported classes are
60. input with type intt St St B where St is the state space type 6 2 VDM quotation expressions There are various places where special VDM functions may be used or quoted In particular the pre and post conditions of functions and operations may be quoted This quotation makes use of a systematic convention from 1 SpecBox User Manual version PC 2 21a 6 4 The analyser 6 2 1 Function Quotations If a function has the following functional type f AL 4 R the associated pre and post conditions have type pre f AXX 4 B post f Ayx xA xR B 6 2 2 Operation quotations If an operation implicit or explicit has the following operation type with state space type ST Op Aq X X An gt Ri x x Rm the associated pre and post conditions have type pre Op Ans A x ST B post Op Ay X X A X ST x ST x Ry x x Ry B In each case the first occurrence of state type ST represents the state on entry and the second use is the state on exit 6 3 Scope All declarations occurring within a specification introduces a scope i e a region of the text within which the identifier declared can be correctly referred to The occurrence of an identifier without a corresponding declaration within the available context is therefore regarded as a scoping error SpecBox User Manual version PC 2 21a Scope 6 5 Each main class of declaration introduces global
61. line 1 2 end annotation 7 5 Subscripts SpecBox adopts a convention that any part of an identifier following a double underscore is a subscript Thus input 8 printed as inputg SpecBox User Manual version PC 2 21a Running ATEFX 7 5 7 6 Running IATEFX The BTEX macros generated by SpecBox are defined in a style file sb sty which is included in the distribution You should copy this file to the inputs subdirectory of your T X system This style needs to be included in the optional arguments to the documentstyle command Note that version 2 21 of sb sty is not compatible with ATpX produced by SpecBox versions before 2 21 BTEX files require a preamble that is incompatible with draft ISO VDM and it is therefore normal to use an input or include command to read the file generated by SpecBox Alternatively you can select a start point after the preamble As an example suppose you wish to write a file report tex say to print the specification generated by SpecBox from the file code vdm report tex will need to contain commands similar to the following documentstyle 1ipt sb article begin document input code end document You then run BTEX by typing latex report This produces a file report dvi which is printed by means of SpecBox User Manual version PC 2 21a 7 6 BTEX generator the particular driver for your printer 7 7 bsivdm sty sb sty incorporates extracts from the public doma
62. me after foo you would be offered only and after foo you would be offered only C The effect of a choice extends as far to the right as possible so after foo a b you will be offered only again SpecBox User Manual version PC 2 21a Editor 5 9 Skip option Correction menu The item causes the syntax checker to jump forward in the file to the start of the next major syntactic item A message giving the line number at which checking recommenced is given at the bottom of the screen or the warning Cannot resynchronise parse concluded if the end of the file is reached before such a place is found Further analysis is not allowed if syntax errors have been skipped in this way and the check ends with the message FINISHED This option is available only when checking complete modules Insert mode option Correction men The item toggles between insert mode and overwrite mode for corrections chosen from this menu The insert or overwrite mode of the editor is not affected 5 7 Editor Correction menu SpecBox s built in editor is invoked by selecting the option from the correction menu or by chosing one of the replacement tokens SpecBox User Manual version PC 2 21a 5 10 The syntax checker In order to conserve memory the editable text is limited to one screen If more text is input beyond this limit
63. mt return exit skip error handlerstmt letbestmt letstmt defstmt dclstmt 83 block dclstmt stmt stmt 2 H 84 dclstmt del identifier type exprorcallstmt SpecBox User Manual version PC 2 21a Statements 85 86 87 88 95 96 97 defstmt equalsdefn letbestmt letstmt assignment statedesignator designatoritem designatorarg exprorcallstmt callstmt usingstmt nondetstmt forloops 9 11 def equalsdefn equalsdefn in stmt patbind exprorcallstmt let simplebind stexpr in stmt let letbind letbind in stmt statedesignator exprorcallstmt identifier identifier designatoritem designatorarg fieldid 7 expr expr usingstmt identifier identifier expr 57 expr usingstmt using statedesignator I 7 stmt 57 stmt y intloop SpecBox User Manual version PC 2 21a 9 12 The SpecBox grammar sequenceloop setloop 98 sequenceloop for patbind in reverse expr do stmt 99 setloop for all pat in set expr do stmt 100 intloop for identifier expr to expr
64. n PC 2 21a 3 1 3 GENERAL FEATURES This section describes the general features of SpecBox that apply to all the functions such as the menu system and the help facility The functions themselves are covered in sections 4 to 7 Batch processing is also described 3 1 The menu system SpecBox is principally controlled by means of a system of menus with some additional information entered through edit boxes You can select items from menus in three ways 1 By pressing the appropriate quick key This is the leftmost capital letter in the item name and is the initial letter unless two or more items start with the same letter 2 If the mouse is not in use by moving the highlighting bar to the required item using the and keys then pressing Enter 3 With the mouse by pointing at the item and clicking the left button A small arrow to one side of the menu indicates that there are more menu items than currently displayed If the mouse is not in use the and keys will cause the menu window to scroll to display the other items If the mouse is in use clicking the small arrow scrolls the menu SpecBox User Manual version PC 2 21a 3 2 General features Not all menu items may be allowed at a particular stage in analysis for example IATpX generation cannot proceed until syntax checking has been carried out successfully Such items are shown in brackets and the highlighting bar
65. n 5 7 below Edit option Correction menu Selecting the menu item causes the built in editor to be invoked with the cursor at the start of the highlighted token See Section 5 7 for more information on the built in editor Complete option Correction MENU If the item is available it means that there exists only one possible token or list of tokens ignoring optionals at this point in the parse Selecting this item will cause these token or tokens to replace or be inserted before the highlighted token according to the insertion mode selected Sometimes the checker cannot decide whether the end of the parse has been reached If this is so it stops with the first token beyond the parsed text highlighted and the correction SpecBox User Manual version PC 2 21a Adding and correcting text 5 7 menu headed End of text Selecting in this case will cause the check to conclude successfully Grammar option Correction menu Selecting the item gives menus of the allowable terminals and nonterminals at each possible level in the grammar Selecting a nonterminal will cause a menu of terminals and nonterminals one level deeper in the grammar to be displayed Selecting leads to a menu one level higher in the grammar If a token in the source file is highlighted selecting a terminal will cause it to be inserte
66. n that it believes is the first one outside the section of text being checked Answering will successfully conclude the check If the file has been successfully rechecked after correction by means of the built in editor a menu headed Save altered file will appear before the main menu is displayed select or according to whether or not you wish to preserve the edits You cannot analyse the specification or generate a IATpX or Mural file from it unless the edits are preserved since otherwise the outputs would refer to an out of date file If you save the edits the original file is renamed with the extension bak In batch mode the progress of the syntax checking session is recorded in a log file named by the source filename with the extension changed to log 5 3 Selecting the start point You can use the built in editor to select a start point for the check other than the start of the file Choose the item from the top level menu position the cursor at the start of the region of text to be checked and press or click the mouse on the text Start point on the menu bar at the bottom of the screen Then select or click Quit to return SpecBox User Manual version PC 2 21a 5 4 The syntax checker to the top level menu See Section 5 7 for more information on the built in editor 5 4 Selecting an insertion point You can pause the syntax checking at any point by placing an insertion point in the file When the c
67. names of the following kind State types The state declaration introduces the identifier as a record type This identifier can then be used globally within type expressions Additional entities are e as for record type declarations e the variables declared as fields which may be referred to in operations e state initialisation predicate Type declarations The type declaration introduces the identifier as a type This identifier can then be used globally within type expressions Additional entities are e records e g construction function amp selector functions e quoted literals defined by explicit enumeration e invariant functions Value declarations The value or constant declaration introduces the identifier as a value together with its type i e arity The identifier can then be used globally within expressions Function declarations The value or constant declaration introduces the identifier as a value together with its type SpecBox User Manual version PC 2 21a 6 6 The analyser i e arity The identifier can then be used globally within expressions Additional entities are e pre amp post condition predicates Operation declarations The operation declaration introduces the identifier as an operation together with its type i e arity The identifier can then be used globally within statements i e explicit operation calls Additional entities are e pre amp post condition predic
68. nd functions maxs set of Letter gt Letter maxs 1 is not yet defined ptrans Letter Letter Pcode gt Letter ptrans kl ml code code k1 m1 operations CODE m seq of Letter t seq of Letter ext rd c 8 rd k Key post len t len m and let 1 maxs dom k 1 in forall i in set inds t amp t i ptrans k i mod 1 m i c DECODE t seq of Letter m seq of Letter ext rd c Pcode rd k Key post len m len t and let 1 maxs dom k 1 in forall i in set inds t amp SpecBox User Manual version PC 2 21a 10 10 Illustrative examples t i ptrans k i mod 1 m i c end Code SpecBox User Manual version PC 2 21a Code 10 11 Code example 1 1 module Code 2 1 definitions 3 1 types 41 Mcode Letter L Letter 2 inv m A 3 V x Letter x dom m 5 1 Pcode Letter 2 gt Mcode 2 inv m A 3 V x Letter x dom m 61 Key 4 7 Letter 2 inv m A 3 dn Z domm 0 n 7 1 Letter is not yet defined 8 1 state 2 Code of 3 c Pcode 4 k rey 5 end 9 1 functions 10 1 mars Letter set Letter 2 mazs l is not yet defined SpecBox User Manual version PC 2 21a 10 12 Illustrative examples 11 1 ptrans Letter x Letter x Pcode Letter 2 ptrans kl ml code A code kl ml 12 1 operations 13 1 CODE m Letter t Letter 2 ext rde Pcode 3 rdk Key 4 post lent len m A 5 let maxs domk 1 in 6 Vicindst 7 t 1 ptr
69. nd complex specifications may cause it to run out of workspace during this sorting if this SpecBox User Manual version PC 2 21a PC versions 2 3 occurs an unsorted listing can be selected through the menu item See Section 4 3 for details of how to carry this out SpecBox makes use of a number of working files during its operation and because the root directory can only hold a limited number of files it is desirable to place these in a subdirectory which in the 80386 version can be specified through the _configure menu item If no subdirectory is configured the setting of the TEMP environment variable will be used if it is defined Standard version The standard version has been written for 8086 and 80286 PCs This version is constrained to conventional memory and uses disk storage for parse trees too large to hold in RAM this imposes certain limits on the size of specification that can be analysed The absolute limit is that the concrete parse tree must occupy less than 1MB the number of pages this represents obviously depends on the nature of the specification and the number of comments comments are not retained by SpecBox but is very roughly fifteen pages of uncommented VDM You will find however that SpecBox slows down and the amount of disk activity increases when the concrete parse tree becomes too large to hold in actual memory and corresponds to about three pages of uncommented VDM If you
70. not available if parsing Quit without reparsing Help EH 0 e With the mouse editor functions can be selected by clicking on the description in the menu bar at the bottom of the screen Clicking the right button quits the editor without reparsing Cursor movement With the keyboard the following actions position the cursor SpecBox User Manual version PC 2 21a 5 ui N The syntax checker Function Move cursor one character to right Move cursor one character to left 2 0 E Move cursor up one line unless at top of screen Move cursor down one line Scrolls the view down one line if at bottom of screen Move cursor to end of line a Move cursor to beginning of line o 3 HE Move cursor to top left of screen Move cursor to bottom left of screen Delete character to left of cursor HE 5 a With the mouse the cursor can be positioned by pointing to a character and clicking the left button The view can be scrolled by clicking the left button on the small arrow at the bottom right of the screen Deleting and copying With the keyboard the following actions delete and copy text Key Function D Delete block or line Insert block or line Copy block or line When D is pressed a block indicated by highlighting in a different colour on a colour screen or reverse video on a monochrome screen will appear running from the cursor to the end of the edit
71. ntegers are strings of digits that do not contain a decimal point Real numbers should be written in the manner 12 3 or 123 4E 5 which will be converted to 12 3 and 123 4 x 107 in the mathematical syntax At least one digit must occur directly after the decimal point Leading zeros are allowed only in the case of the integer 0 and real numbers such as 0 123 Character and text literals charlit and textlit Character literals represent single characters and are written in single quotes e g ei Text literals represent sequences of characters and are written in double quotes e g A string SpecBox User Manual version PC 2 21a Lexical rules 9 33 Single quotes within character literals and double quotes within text literals must be preceded by a itself is represented by Thus is the mathematical syntax corresponding to r and A string with a corresponds to the source text A string with a All other characters appear unchanged in the mathematical syntax Comments Two sorts of comment are allowed by draft ISO VDM Brief comments run from a pair of dashes to the end of the line This is a comment Longer comments annotations are enclosed between the keywords annotation and the next end annotation Draft ISO VDM allows annotations to be distinguished in any convenient way in the mathematical syntax SpecBox places them in an environment named annotation which is defined in sb
72. o valuedefns fundefns opdefns 18 typedefns types typedefn typedefn 19 valuedefns values valuedefn valuedefn 20 fundefns functions fundefn fundefn 21 opdefns operations opdefn opdefn 9 4 Type definitions 22 typedefn identifier typedef 23 typedef typedefeqn typedefrcd isnotyetdefn 24 typedefeqn type invariant 25 typedefrcd 7 7 field field invariant 9 5 Type expressions 26 type simpletype SpecBox User Manual version PC 2 21a Type expressions 9 5 27 28 uniontype tupletype mappingtype maptype inmaptype funtype typety simpletype uniontype tupletype mappingtype funtype type type type PT type maptype inmaptype map type to type inmap type to type typety gt type typety gt type emptytype type quotetype typename basictype typevariable settype seqtype optionaltype recordtype bractype SpecBox User Manual version PC 2 21a 9 6 The SpecBox grammar 35 settype set of type 36 seqtype seq0type seql type 37 seq type seq of type 38 seqltype seql of type 39 optionaltype P type 40 recordtype compose identifier of field field end 4
73. on PC 2 21a 6 14 The analyser types of the actual parameters are subtypes of the types of the formal parameters 6 6 Output during checking During the checking of the specification the kind of definition encountered is output together with the name of the item that it defines Error messages are printed as errors are discovered and retained for inclusion in the listing file If errors are discovered a message giving the number of errors is printed at the end of the definition 6 7 Report file This contains a summary of the modules parsed and of the global declarations in each module These declarations are grouped together for each kind of definition in the VDM language Note that the additional VDM specific functions are also included together with the arity information computed by SpecBox for checking purposes Finally a statement of the number of errors discovered is given File Description lt filename gt rep SpecBox User Manual version PC 2 21a Listing file 6 15 6 8 Listing file This contains a line numbered listing of the specification modules parsed Error messages are included near to where the analyser understands that they were encountered Naturally enough any error actually found could possibly be symptomatic of some other more profound error located elsewhere usually earlier in the file In such cases the user should inspect the context carefully to find the true source of the pro
74. ould therefore ensure that comments are acceptable to IATpX Note that the annotation environment will give a wrongly nested environment error message if used with JATpPX versions dated earlier than 24th May 1989 This message is spurious and the printed specification is not affected 7 4 Line numbering Specifications can be printed with line numbers by preceding them by the command sbnumberson The default on startup is numbering off this can also be selected with the command sbnumbersoff Numbering begins at 1 1 and proceeds at intervals of 1 until a blank line is encountered when it is incremented to 2 1 This process continues until another sbnumberson command is encountered when numbering is reset to 1 1 IATpX cross references can be implemented by placing a label command in a short comment SpecBox adopts a convention that the at the start of a short comment is not printed if the first character of the body of the comment is also a this is intended to be used for comments containing only non printing ATpX commands This is illustrated by the following example which gives the source followed by the mathematical form SpecBox User Manual version PC 2 21a 7 4 BTEX generator Num nat A type defn inv n gt 256 label inv annotation The invariant is at line reffinv end annotation 11 Num type defn 2 inv n A n gt 6 annotation The invariant is at
75. pl 59 fundefimplnyd 60 fundefn 56 fundefns 20 funsigmap 13 funtype 32 dclstmt 84 defexpr 117 defnblock 17 defstmt 85 designatorarg 92 designatoritem 91 document 1 elsifexpr 150 guardedstmt 105 SpecBox User Manual version PC 2 21a Index to the grammar 9 25 handlerstmt 109 mapenum 8 mappingtype 29 identifier 190 maptype 30 idfunsig 14 matchval 187 idseqpat 181 matchvalue 188 idtypepair 62 mccarthystmt 102 idvaluesig 2 mkidentifier 189 ifexpr 149 mktoken 194 ifstmt 103 modsig 7 importclause 3 modsigitem 8 inittoken 9 multibind 171 inmaptype 31 instance 5 nameexpr 160 instclause 4 nametoken 192 intlit 202 nondetstmt 96 intloop 0 invariant 50 invinitdefn 1 invtoken 198 isexpr 154 isnotyetdefn 52 istoken 195 oldvarname 161 opdef 71 opdefbody 80 opdefcont 79 opdefexpl 8 opdefexplnyd 81 opdefimpl 2 lambda 8 opdefimplnyd 3 letbeexpr 119 opdefn 70 letbestmt 87 opdefns 21 letbind 121 opsig 16 letexpr 118 opsigmap 15 letfunbind 3 optionaltype 39 letstmt 88 optype 42 literal 200 othersexpr 153 othersstmt 108 mapcomp 0 pat 174 SpecBox User Manual version PC 2 21a 9 26 The SpecBox grammar patbind 167 sequenceexpr 142 patident 186 sequenceloop 98 patidorval 185 sequencepat 178 patparams 69 setbind 170 pattypebind 168 setcomp 137 pattypeparams 61 setenum 135 polyfuninst 156 setinterval 134 postcond 64 setloop 99 posttoken 7 setmultibind 172 precond 63 setormapexpr 133 pretoken 196 se
76. porting them e Importing does not create storage but provides facilities from the module for defining and manipulating objects e As a consequence a non parameterized module need never be imported into a module more than once as it only introduces facilities and services Importing it twice into the same module can always be replaced by a single import Documents are included in the SpecBox syntax but not currently accessible through the menu because semantic checking is restricted to single modules SpecBox User Manual version PC 2 21a Background 11 5 11 1 4 Parameterized modules Modules may be parameterized by formal parameters Such modules are not imported instead they are instantiated by providing actual parameters in place of the formal ones e Several uses of a parameterized module may be made within another module to enable it to be instantiated in a number of differing ways 11 1 5 General form of the interface The general pattern for defining and using modules is as follows module ModNm interface parameters Parameters that this module will need when it is used by modules that instantiate it ParmModSig imports Use of non parameterized standard modules from ImpModNm ImpModSig from ImpModNm 2 ImpModSig2 etc instantiation Use of parameterized modules SpecBox User Manual version PC 2 21a 11 6 Modules InstModNm as PModNm ParmBind ParmlmpModSig InstModNmz
77. provided in machine readable form on the distribution disks Each example is given first in the ASCII syntax and then in the mathematical Note that these examples may exceed the subset of the draft 150 VDM syntax currently supported by Mural For more details on the use of VDM readers are referred to 1 and 6 A description of draft ISO VDM module syntax is given in Section 11 10 1 General observations Our experience in converting some of our own work into SpecBox shows that the use of a tool such as SpecBox enforces certain disciplines such as the complete declaration of variables and the careful use of naming that are missing from VDM that has not been mechanically checked It is these issues relating to scoping where we found many errors in some of the VDM we have translated over the past few months Some of this detail may not be appropriate in a text book or tutorial where fragments of specifications are used to illustrate a particular point There are also stylistic conventions that are useful to adhere to that are not enforced by the language The use of capitals to denote operations the use of uppercase as the first letter of SpecBox User Manual version PC 2 21a 10 2 Illustrative examples type names and the following of the general layout of 1 are all practices to be recommended 10 2 Notes on the ASCII syntax The raised dot in quantified expressions is denoted by a amp in the ASCII syntax e
78. r specifications include modules that are much larger than this we suggest that you check them in fragments of around four or five pages while developing them selecting the appropriate SpecBox User Manual version PC 2 21a 2 4 Installation syntactic category from the main menu and then check the complete module at the end The performance of the standard version can be improved by freeing as much conventional memory as possible for SpecBox Using Microsoft MS DOS 5 0 or an alternative memory manager such as that from Quarterdeck may enable you to move some memory resident software into the upper memory area and if it is available expanded or extended memory on PCs with 80286 80386 or 80486 processors If this is not possible or not sufficient you will need to remove optional memory resident software such as mouse drivers network drivers and shells SpecBox briefly displays at the bottom of the screen the amount of heap available after the core system is loaded 385 kbytes available heap is the minimum to run SpecBox satisfactorily 420 kbytes is recommended and 435 kbytes should be achievable with full use of memory management If you have a PC with additional memory configured as a virtual disk the performance of the standard version can be improved on large files by configuring SpecBox to store the parse tree on the virtual disk See Section 4 3 for details of how to carry this out SpecBox User Manual versio
79. rom the text and stored in the insert buffer Clicking the right button cancels the operation Text is copied in the same way as it is deleted only Copy is clicked in the menu bar SpecBox User Manual version PC 2 21a 5 14 The syntax checker Clicking Insert inserts the contents of the insert buffer immediately before the cursor position and can thus be used for both copying and undeleting text SpecBox User Manual version PC 2 21a 6 1 6 THE ANALYSER Top level menu The SpecBox semantic analyser performs basic semantic checking of VDM specifications and is concerned with the scopes and arities of formulae In addition a number of VDM specific design rules are checked such as the visibility of state variables in operations specified by pre and post conditions 6 1 Arities The arity of a value is the number of input parameters that it depends upon together with the number of results that it can deliver In a sense the arity is a simplified kind of type and can be checked in a similar way In VDM various items can possess arities in addition to basic functions such as mappings and operations There are also families of functions associated with a given VDM specification such as record constructors and selector functions 6 1 1 Functions All functions in VDM have functional types fs Ai x x An 5 Ra x x Rm SpecBox User Manual version PC
80. rs digits underscores _ and primes The mathematical form replaces _ by If you wish to use a keyword as an identifier you must precede it by a e g module or pre_ types Old state values are represented by a suffix these are converted to the hooked form in the mathematical syntax For example var is converted to var Greek letters can be represented by preceding the corresponding upper or lower case letter by Not all the possible upper case Greek symbols e g A are available in standard IATEX sb sty substitutes Roman letters for these SpecBox User Manual version PC 2 21a Lexical rules 9 31 omicron is printed as o Ascii Mathematical Ascii Mathematical A A ta a B B b B G T ig y D A d E E te Z 7 itz C H H h n Q o q 0 SI I di L K K k K L A 1 M M m N N n V X x t amp 0 0 to 0 P II p T R P ir p S x is o ST T t T U Y itu U F f C X ic X Y y ty m AN Q tw w SpecBox User Manual version PC 2 21a 9 32 The SpecBox grammar Compound identifiers mktoken etc A compound identifier is formed by prefixing mk_ pre_ post_ inv_ init and is to a simple identifier The ATpX generator converts the underscore to a hyphen Quoted literals quotlit Distinguished literals are written in upper case letters and placed in pointed brackets e g TRIP The mathematical form is TRIP Numbers intlit and ratlit I
81. rsion 2 3 aborting activities 3 3 analyser 1 1 1 4 6 1 arity checking 6 1 error messages 6 7 function checking 6 1 operation checking 6 2 output 4 quotation checking 6 3 scope checking 6 4 annotated listing 1 1 1 4 6 15 audible beep 4 3 batch mode 1 5 3 4 bsivdm sty 7 6 config sys file files command in 2 1 configuration 4 2 4 3 cross reference file 1 1 4 6 15 sorting 4 4 default directory 4 1 displays 3 3 DOS accessing from SpecBox 4 5 MS DOS 5 0 2 2 version 2 1 edit boxes 1 editor built in 1 1 1 3 1 4 5 4 5 6 5 9 copying 5 12 cursor movement 5 11 deleting 5 12 miscellaneous functions 0 moving to start of file 5 10 setting insertion point 5 10 setting start of check 5 10 external 1 1 1 4 4 2 pathname 4 3 examples 9 1 bank accounts 9 13 binary trees 9 17 code 9 8 telegram analysis 4 files command in config sys 1 garbage collection 3 3 grammar 8 1 9 1 SpecBox User Manual version PC 2 21a 13 2 Index access from correction compound 8 32 menu 5 7 keywords as 8 30 EBNF description integers 8 32 8 1 mathematical symbols keywords 8 28 8 34 old state values 8 30 quoted literals 8 32 real numbers 8 32 lexical rules 8 30 nonterminals 5 7 notes on ASCII syntax handling of comments 7 2 line numbering 7 3 output file 1 output format 1 style file 7 5 subscripts 7 4 viewing output 7 5 lexical rules 5 2 8 30 chara
82. se takes effect straight away disabling takes effect from the next time SpecBox is loaded See Section 4 3 for details of how to carry this out SpecBox assumes that the mouse uses interrupt 51 if this is not the SpecBox User Manual version PC 2 21a 2 2 Installation case the system may crash if the mouse is enabled SpecBox does not incorporate a mouse driver and a suitable one must be installed before running SpecBox 2 3 PC versions Two PC versions of SpecBox are available the standard and the 80386 versions 80386 version The 80386 version uses a DOS extender that is compatible with both Microsoft MS DOS 5 0 and Microsoft Windows 3 This version stores the concrete parse tree entirely in RAM and its performance will therefore depend on the amount of RAM in the particular configuration The 80386 version is normally shipped configured so that SpecBox occupies extended memory this leaves the standard 640kB for other DOS applications and in particular the external editor see Section 4 2 This configuration may run out of heap space when analysing specifications over about 10 pages unless the PC contains at least 2MB of RAM Configurations with less RAM than this will probably perform better with the standard 8086 version 80386 PCs with 4MB or over of memory should be able to analyse any realistically sized specification SpecBox sorts the cross reference information produced by the analyser Unusually large a
83. ser Manual version PC 2 21a Instantiation and parameterization 11 17 20 1 end CDICT 11 4 2 Mailing list This example shows how a sorting module can be instantiated for a particular type and relation in the definition of a mailing list it is based on 5 The natural way of writing the instantiation in mailing list would be something like item Z are ordered gt However as already mentioned in Section 11 1 5 the grammar requires identifiers for Z and gt This is achieved below by the local definitions of Integer and ge however a neater solution would be to define another parameterized module giving general expressions for orderings module sort parameters types item functions 1 exports 1 2 3 A 5 are ordered item x item B 6 7 functions 8 do sort item item 2 1 definitions 2 functions A do sort item item A do sort input list A SpecBox User Manual version PC 2 21a 11 18 Modules 5 if input list 6 then else insert sorted hd input list do sort tl input list 3 1 insert sorted item x item item 2 insert sorted elem list A 3 if list i A then elem list 5 else hd list insert sorted elem tl list 41 end sort 5 1 module mailing list 2 instantiation 3 integer sort as sort item Integer are ordered ge A functions 5 do sort Integer Integer 6 1 definitions types 3 Integer Z
84. ters 11 2 2 Sharing of storage VDM in common with Hoare logic and much else eschews sharing and insists that parameters are passed by value it is SpecBox User Manual version PC 2 21a 11 10 Modules normally said that sharing destroys the assignment axiom but actually it damages much else as well However sharing can be modelled by the explicit use of keys as shown in the following simple example which defines an abstract data type STACK used to set up a collection of stacks in a second module 1 1 module STACK 2 exports 3 operations 4 PUSH 5 5 POP N 6 types T Stack 2 1 definitions 2 state Stack of s N 3 init mk Stack so A so 4 end 7 3 1 operations PUSH 5 3 PUSH i is not yet defined 4 1 POP Q N 2 POP is not yet defined 5 1 end STACK 6 1 module COLLECTION 2 imports from STACK 3 operations 4 PUSH 5 5 POP N SpecBox User Manual version PC 2 21a Sharing 11 11 6 types 7 Stack 7 1 definitions 2 types 3 Key is not yet defined 8 1 state Colln of c Key STACK Stack 2 init mk Colln co A 60 3 end 9 1 operations 2 KPUSH k Key i N 3 ext wr c Colin 4 pre k dome 5 post post PUSH i c k c k 6 V Key 7 KE domcAk k gt 8 e k c Kk 10 1 end COLLECTION We could have an operation with two keys but notice that KTWO k1 Key ka Key ext wr c Colln pre ky dome A ko domc post dtN
85. tion notation in draft ISO VDM The modularization facility does not form part of the core language when the standard is published the syntax and semantics of the modules will be in an informative annex All the examples are syntactically correct and indeed have been typeset in the mathematical notation using SpecBox however most give some spurious semantic errors as a result of going outside the currently supported area 11 1 Background The module scheme for draft ISO VDM was first proposed by Stephen Bear 4 The standardization meetings have concentrated on the flat language although a few papers on modules have been tabled e g 5 1 contains some simple examples one of which is taken up in Section 11 4 1 below Modules provide the following facilities e A hierarchical design approach e Name space control by permitting certain objects to be exported Those not exported are not visible from an external point of view and may only be referenced internally to the module that defines them e Reuse of commonly used services SpecBox User Manual version PC 2 21a 11 2 Modules e Partitioning of services provided two modules should not provide identical functionality The specification of concurrent or distributed systems is explicitly not catered for The reason is that the semantics of operations assume that the complete system state is known when any state change occurs this is known as the frame
86. tpat 175 settype 35 quantifier 128 setunionpat 7 quotetype 45 simplebind 6 quotlit 193 simplesetpat 176 simpletype 34 statedesignator 90 stateinfo 49 stexpr 120 stmt 82 subsequence 158 substitute 6 ratlit 203 readwritemode 76 recordconstr 145 recordmodifier 146 recordpat 182 recordtype 40 rectrapstmt 112 return 114 textlit 205 tokenitem 191 trapbind 3 trapstmt 111 tupleexpr 163 tuplepat 184 tupletype 28 seq type 37 seqltype 38 seqlitpat 183 seqpatid 179 seqpatidpat 180 seqtype 36 type 26 sequencecomp 144 typebind 169 sequenceenum 143 typedef 23 SpecBox User Manual version PC 2 21a Index to the grammar 9 27 typedefeqn 24 typedefn 2 typedefns 18 typedefrcd 25 typedescr 10 typemultibind 173 typename 6 typesigmap 9 typety 33 typevardecl 57 typevariable 47 unaryexpr 124 unaryop 125 uniontype 7 uniqueexpr 132 usingstmt 95 valbind 122 valuedef 55 valuedefn 53 valuedefncont 54 valuedefns 19 valuesigmap 11 vdmmodule 2 whileloop 1 SpecBox User Manual version PC 2 21a 9 28 The SpecBox grammar 9 15 Keywords The draft ISO VDM keywords are as follows Alphanumeric keywords abs all always and annotation as be bool by card cases char comp compose conc dcl def defined definitions dinter div do dom dunion elems else end error errs exists existsi exit exports ext false floor for forall from functions hd if imports
87. tted the exported objects are taken as being not yet defined 11 2 Sharing Two types of sharing are of interest sharing in the sense of mathematical equality and sharing in the sense of sharing storage Not currently supported by SpecBox SpecBox User Manual version PC 2 21a Sharing 11 9 11 2 1 Sharing by equality Because VDM objects are mathematical abstractions and therefore satisfy the usual properties of equality it may happen that some of the values and types exported by modules may in fact be equal The sharing rules are as follows imported modules These are shared That is if objects from a module A are imported into two separate modules X and Y and then objects from the modules A X and Y are imported into a fourth module Z all the exported constructs from A are the same no matter which module they occur in parameterized modules In order to be used parameterized modules must first be instantiated and given a particular name This name is then used within the instantiating module to refer to the services that the parameterized module exports If a module is instantiated twice within another module the constructs must be given distinct names In general parameterized modules will be instantiated differently and will not therefore be equal However identical instantiations will be equal a simple example of this may be constructed by exporting a value that is not dependent upon any of the parame
88. tule Such an assumption is invalidated when treating concurrent or distributed systems of any realistic complexity This area is the subject of much recent research by Ketil Stolen and Cliff Jones Other ISO standard notations such as LOTOS are available for formally describing such systems 11 1 1 Modules as abstract data types An module may be viewed as something that provides a collection of related facilities and services These are presented in terms of VDM types and functions as well as operations over a distinguished type known as the state type Thus a module represents a collection of abstract data types in terms of types functions and operations It may be the case that a module does not export any operations or a distinguished state type providing only types and functions externally Such a module is said to be pure otherwise the module is said to be state based A module does not correspond to a task process or agent It has no dynamic extent in that modules merely provide services in terms of functions and relations In short a module is not executed in any operational mechanistic sense instead it just represents a container from which users SpecBox User Manual version PC 2 21a Background 11 3 of the module can select from the services provided 11 1 2 Use of modules In general a system will consist of a hierarchy of modules with a single top level module at the root Modules in the hierar
89. ut the BTEX output In particular e It obeys line breaks SpecBox User Manual version PC 2 21a 7 2 BTEX generator e Single spaces are interpreted as normal interword spaces e Two or more spaces tab the output to the corresponding column in the source This enables items on adjacent lines of the specification to be aligned if required Normally items in the specification will be separated by single spaces giving the result on the left from the source on the right u indicates a space character Pcode character Pcode key Key key Key However if you wish to align the types in this example align them in the source making sure there are two or more spaces before each character Pcode character Pcode key Key key The tab separations are defined by the length sbtab defined in sb sty This is set up to give good results on a range of specifications but if you find it is giving too much or too little space in your case you can reduce or increase it appropriately See 2 for details of setting length dimensions 7 3 Comments Both short comments which run from to the end of the line and annotations which run from the keyword annotation to end annotation are allowed by draft SpecBox User Manual version PC 2 21a Line numbering 7 3 ISO VDM The contents of both types of comment are copied unchanged to the IATpX file and you sh
90. ve 4 4 SpecBox User Manual version PC 2 21a
Download Pdf Manuals
Related Search