Home

Overture VDM-10 Tool Support: User Guide

1. 61 Tc 63 15 4 Generated GUI of VDM Models 64 16 A Command Line Interface to Overture 69 ie ceci ote De ce Be eie Lo 69 ee ee 70 rco cse DNO 71 DuC NAP ee RA PA RAD ee GI SIME a E 81 oo n A Templates in Overture S CONTENTS B Internal Errors 87 C Lexical Errors 89 D Syntax Errors 91 E Type Errors and Warnings 105 F Run Time Errors 121 G Categories of Proof Obligations 129 H Mapping Rules between VDM VDM RT and UML Models 133 I Using VDM Values in Java 137 LI The Value Class Hierarchy x euo om RR ha ges d s ak d dre s 137 L2 Primitive Valugsl uu dou he eh n e a i desert e E ete re er oin 6 137 L3 Sets Sequences and Maps e sem sos ns ps sea Crack Bae Grace Gee GB 4 139 Lf Other Types x uoa ow A SEE Ge BEER ROS Gees 141 1 4 1 _Functon values Les ss has ss dk pere ee lg amp S ec 141 4 2 Object Valles Los mad sega oed e ed rg Sree Brg dee A fo RC 141 LAS Recor Vales sore Tor asore Eoi a 344 OE EE 322 142 1 4 4 _ Token Values 4 24 uk om mk dno ode ace da aa ns RO EXT OUR A 142 ESE ie 3d cT 143 LAO Invariant Values 4 4 4 mad oe 4 bis bh eh his x hea a d 143 1 4 7 Void Values sus vus cR x 0v x x XR x Um Sw o e 143 144 Overture VDM 10 Tool Support User Guide ABSTRACT This document is the user manual for the Overture Integrated Development Environment IDE for the Vienna Development Method VDM It serves a
2. Architecture overview Execution overview vCpu CPUL cruz crus CPUS CPU CPU vCpu vBus NW BUS Fd tH al RH 1 1 1 1 1 L 1 1 1 oOo Tm e o e eo o eo c eo eo eo eo eo Lo e eo Lo ex eo e eo eo e o Lo m Lo Lo e eo eo eo e Lo Lo 74 eo eo eo o m e N N oD c eo eo e e e oo eo eo e e e m m o o o Co oo o e m m e o o Liens N N EN N o gt eo e m Figure 14 5 Violations of validation conjectures shown in the model execution overview 22 Chapter 15 Expanding VDM Models Scope and Functionality by Linking Java and VDM In some cases the impact and value of VDM models can be immensely improved by expanding them with functionality which is not delivered directly by VDM Examples of such functionality could be a to associate the model with existing legacy systems for which no model or speci fication exists b to add a graphical representation of the model or c to enable network com munication for instance in a client server setup In order to achieve this functionality Overture enables the possibility of linking a VDM model directly with the underlying Java based Overture interpreter In addition it is possible to link a Java implementation with a VDM model Overture supplies two different techniques for linking between VDM and Java 1 the func tionality which allow VDM to interact with an External Java Library
3. Tnstance invariant violated lt inv_op gt State invariant violated lt inv_op gt Using undefined value Map range is not a subset of its domain T Infinite or NaN trouble Cannot instantiate a system class Cannot deploy to CPU Cannot set operation priority on CPU Cannot set CPU priority for operation Multiple BUS routes between CPUs lt name gt No BUS between CPUs name and lt name gt CPU policy does not allow priorities Value already updated by thread n No such test number lt n gt key T and name State init expression cannot be executed 126 APPENDIX F RUN TIME ERRORS EB 4145 Time n is not a natl 4146 Measure failure f args measure lt name gt current value previous value 4147 Polymorphic function missing QT 4148 Measure function is called recursively lt name gt 4149 CPU frequency to slow speed Hz 4150 CPU frequency to fast speed Hz 4151 Cannot take dinter of empty set 4152 Wrong number of elements for map pattern 4153 Values do not match map pattern 4154 Cannot match map pattern 4155 Map union pattern does not match expression 4156 Cannot match map pattern 4157 Expecting tive integer in periodic sporadic argument lt n gt 4158 Period argument must be non zero 4159 Delay argument must be less than the period
4. 2309 Expecting stoplist 2310 Expecting stoplist 2311 Expecting after stoplist objects 2312 Expecting after sporadic 2313 Expecting after sporadic arguments 2314 Expecting after sporadic 2315 Expecting name after sporadic 103 Overture VDM 10 Tool Support User Guide 104 Appendix E Type Errors and Warnings If the syntax rules are satisfied it is still possible to get errors from the type checker The errors can be as follows 3000 Expression does not match declared type 3001 Class inherits thread definition from multiple supertypes 3002 Circular class hierarchy detected lt name gt 3003 Undefined superclass lt supername gt 3004 Superclass name is not a class lt supername gt 3005 Overriding a superclass member of a different kind lt member gt 3006 Overriding definition reduces visibility Thiserror message typically are caused by using a more restrictive access modifier or none which is interpreted as pri vate at this place compared to for example an inherited definition 3007 Overriding member incompatible type lt member gt 3008 Overloaded members indistinguishable lt member gt 3009 Circular class hierarchy detected lt class gt 3010 Name lt name gt is ambiguous 3011 Name lt name gt is multiply defined in class 3012 Type lt name gt is multiply defined in c
5. 2106 2107 2108 2109 2110 2111 2112 2113 2114 2115 Expecting Expecting Missing colon Missing col Y Expectin Expectin Expectin Expectin Expectin Expectin Expectin g lt pattern gt g g g g g g after after function parameters after parameters pattern type parameter on FOL end after rs Missing colon after Missing col Y Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin g g g g after after after in identifier type return value Implicit function must have post condition lt type gt lt exp gt state name pattern in invariant initializer pattern in after state definition operation parameters after parameters pattern type parameter on in identifier type return value E at dd lt pattern gt Implicit operation must define a post condition after name in errs clause in errs clause lt exp gt T type bind gt lt exp gt pattern pattern after E d after ro in set set exp gt in set set exp gt periodic period arguments after a d name perrodrce s after periodic 95 Overture VDM 10 Tool Support User Guide 2116 2117 2118 2119 2120 2121 2122 212
6. 4160 Object 4n is not running a thread to stop 4161 Cannot stop object 4n on CPU name from CPU name 4162 The RHS range is not a subset of the LHS domain 4163 Cannot inherit private constructor 4164 Compose function cannot be restricted to type 4165 Cannot convert type to type 127 Overture VDM 10 Tool Support User Guide 128 Appendix G Categories of Proof Obligations This appendix provides a list of the different proof obligation categories generated by Overture and an explanantion of the circumstances under which each category can be expected cases exhaustive If a cases expression does not have an others clause it is necessary to ensure that the different case alternatives catch all values of the type of the expression used in the case choice finite map If a type binding to a type that potentially has infinitely many elements is used inside a map comprehension this proof obligation will be generated because all mappings in VDM must be finite finite set If a type binding to a type that potentially has infinitely many elements is used inside a set comprehension this proof obligation will be generated because all sets in VDM must be finite function apply Whenever a function application is used you need to be certain that the list of ar guments to the function satisfies the pre condition of the function assuming such a predicate is present function compose
7. pog lt fn op gt This command generates a list of all proof obligations for the VDM model that is loaded There is an optional argument to indicate one function or operation name 12 CHAPTER 16 ACOMMAND LINE INTERFACE TO OVERTURE E break lt file gt lt line gt lt condition gt This command creates a breakpoint at a specific file and line and optionally makes it a conditional breakpoint break lt function operation gt lt condition gt This command creates a breakpoint at the start of the body of a named function or operation and optionally makes it a conditional breakpoint trace lt file gt lt line gt lt exp gt This command creates a tracepoint for a specific file and line A tracepoint prints the value of the expression given whenever the tracepoint is reached and then continues trace lt function operation gt lt exp gt This command create a tracepoint at the start of a function or operation body See trace above for an explanation of tracepoints remove lt breakpoint gt This command removes a trace breakpoint by referring to its num ber given by the 1ist command list This command provides a list of all current trace breakpoints by number coverage clear write lt dir gt merge lt dir gt lt filenames gt This command man ages test coverage information The coverage command displays the source code of the loaded VDM model by default all source files are listed with
8. state functions types or values 2014 Recursive type declaration This is reported in type definitions such as T T 2015 Expecting lt type gt or lt field list gt 91 Overture VDM 10 Tool Support User Guide 2016 2017 2018 2019 2020 2021 2022 2023 2024 2025 2026 2027 2028 2029 2030 2031 2032 2033 2034 2035 2036 2037 2038 2039 2040 Function Expectin Function Expectin name cannot start with mk g or after name in function definition type is not a gt or gt function g identifier name after type in definition Expectin Expectin Expectin Expectin Expectin Expectin Expectin g after function name or after name in operation definition q yr g name lt name gt after type in definition g after operation name g external declarations after ext name exp gt exp in errs clause g rd or wr after ext m ww Expectin Expectin g per or mutex set bind lt expression gt g Expectin Expectin Expectin Expected is not specified g simple field identifier ge g field number after g field name or is subclass responsibility Unexpected token in expression Tuple must have 1 argument Expecting mk type Malformed Expecting Expecting Expecting mk type name l
9. 0 9999 rseed 87654321 Memory mk_Memory 87654321 mk_M lt FREE gt 0 9999 mk_M lt FREE gt 0 9999 74 CHAPTER 16 ACOMMAND LINE INTERFACE TO OVERTURE E 03 mk_M lt FREE gt 0 9999 gt env fragments M Quadrant gt nat combine M Quadrant M Quadrant tryBest nat nat seed natl gt reset gt bestfit natl x M Quadrant gt natl add natl natl x M Quadrant gt M Quadrant firstFit natl gt bool rand natl gt natl tryFirst nat gt nat main natl natl gt seq of lt SAME gt BEST lt FIRST gt MAXMEM 10000 delete M M x M Quadrant gt M Quadrant inv M M M gt bool CHUNK 100 bestFit natl gt bool least natl natl gt natl fits natl x M Quadrant gt natl init Memory M Memory gt bool pre add natl natl x M Quadrant gt bool This example shows a VDM SL specification called shmem vdms1 being loaded The help command lists the interpreter commands available Note that several of them regard the setting of breakpoints which is covered in the next section The state command lists the content of the default module s state This can be changed by operations as can be seen by the two calls to rand which change the rseed value in the state a pseudo random number generator The init command will re initialize the state to its
10. 4025 4026 4027 4028 4029 4030 4031 4032 4033 4034 4035 4036 4037 4038 4039 4040 4041 Duplicate map keys have different values lt domain gt Maplet cannot be evaluated Sequence cannot extend to key lt index gt State value is neither a lt type gt nor a lt type gt Duplicate map keys have different values lt key gt mk type argument is not lt type gt Mu type conflict No field tag lt tag gt not yet specified expression reached Map key not within sequence index range lt key gt Cannot create post op environment Cannot create pre_op environment Sequence comprehension pattern has multiple variables Sequence comprehension bindings must be numeric Duplicate map keys have different values key First arg of must be a map function or number Tis subclass responsibility expression reached Tail sequence is empty Name name not in scope Object has no field lt name gt ERROR statement reached No such field lt name gt Loop from lt value gt to lt value gt by lt value gt will never terminate Set bind does not contain value lt value gt Let be st found no applicable bindings Tis not yet specified statement reached 122 APPENDIX F RUN TIME ERRORS EB 4042 4043 4045 4046 4047 4048 4049 4050 4051 4052 4053 4055 4056 4057
11. E lvo ES VOM Explorer 53 Demo vdmpp 52 D Outline 53 4 RW e Wt E v class Demo B 4 Demo 4 Demo O f set of bool bool functions 2 generated E Demo vdmpp public f gt set of bool bool 13 f O b b bool bool a end Demo m 4 h Ta E Console 5 Ql terprete REl ta my Code Generator Console Starting VDM to Java code generation No user specified classes to skip Copied the Java code generator runtime library to C Users peter Desktop Overture workspace Demo generated java lib codegen runtime jar Copied the Java code generator runtime library sources to C Users peter Desktop Overture workspace Demo generated java lib codegen runtime sources jar m Generated Eclipse project with Java generated code Could not code generate class Demo Following VDM constructs are not supported by the code generator b bool bool ATypeMultipleBind at 6 14 Reason Type binds are not supported finished Java code generation generated 1 class 4 Figure 11 4 Reporting of unsupported constructs in the console org overture codegen runtime x and in order to compile the generated Java code the runtime library must be visible to the Java compiler Similar to VDMTools the runtime library also provides implementation for subset of the func tionality available in the standard libraries The runtime library provides a full implementation of the MATH library support for conversion o
12. Fitzgerald8z08a J S Fitzgerald and P G Larsen and M Verhoef Vienna Development Method Wiley Encyclopedia of Computer Science and Engineering 2008 11 pages edited by Benjamin Wah John Wiley amp Sons Inc Fitzgerald amp 08b John Fitzgerald and Peter Gorm Larsen and Shin Sahara VDMTools Ad vances in Support for Formal Modeling in VDM ACM Sigplan Notices 43 2 3 11 February 2008 8 pages Fitzgerald amp 09 John Fitzgerald and Peter Gorm Larsen Modelling Systems Practical Tools and Techniques in Software Development Cambridge University Press The Edinburgh Building Cambridge CB2 2RU UK Second edition 2009 ISBN 0 521 62348 0 Fitzgerald amp 14 John Fitzgerald and Peter Gorm Larsen and Marcel Verhoef editors Col laborative Design for Embedded Systems Co modelling and Co simulation Springer 2014 78 CHAPTER 16 ACOMMAND LINE INTERFACE TO OVERTURE E Fitzgerald amp 98 Henhapl amp 78 ISOVDM96 Java2VDMMan Johnson96 Jones78a Jones78b Jones90 Kurita amp 09 John Fitzgerald and Peter Gorm Larsen Modelling Systems Practical Tools and Techniques in Software Development Cambridge University Press The Edinburgh Building Cambridge CB2 2RU UK 1998 ISBN 0 521 62348 0 W Henhapl C B Jones A Formal Definition of ALGOL 60 as described in the 1975 modified Report In The Vienna Development Method The Meta Language pages 305 336 Springer Verlag 1
13. Overture VDM 10 Tool Support User Guide 48 Chapter 14 Analysing Logs from VDM RT Executions Whenever a VDM RT model is executed a binary logfile with rtbin extension is created in the generated 1ogs subfolder In order to distinguish between multiple runs the name of the logfile indicates the time at which the model was executed Logfiles can be viewed with the built in RealTime Log Viewer by double clicking the rt bin file in the Explorer view In addition Overture provides a textual version of the log file with rt extension which can be inspected using any text editor The RealTime Log Viewer enables you to explore the simulated system execution in various ways In Figure 14 I the architectural overview of a system is shown describing the CPU and BUS topology of the model 4x VDM RT Realtime Log View Architecture overview Exec vcpu cruz cruz cruz CPUI CPU CPUS BUSI Figure 14 1 Architectural overview The RealTime Log Viewer also enables you to get an overview of the model execution at a system level see Figure This view shows how the different CPUs communicate via the BUSes of the system Since the complete execution of a model cannot generally be shown in a normal sized window you have the option of jumping to a certain time index using the button or moving to the next time index using the Movenext button Also Overture enables you to move to the p
14. This is an implementation detail and allows Overture to permute set orderings in certain circumstances These three classes have obvious constructors and allow Values or collections of them to be added to the collection subsequently using standard Java collection methods public ValueSet public ValueSet public ValueSet public ValueSet int size ValueSet from Value v p 139 E Overture VDM 10 Tool Support User Guide ValueList from Value v int size public ValueList public ValueList public ValueList public ValueList public ValueMap public ValueMap ValueMap from public ValueMap Value k Value v Using these three helper classes it is now possible to create VDM set sequence and map values using constructors of the Set Value SeqValue and MapValue classes public SetValue public SetValue ValueSet values public SeqValue public SeqValue ValueList values public SeqValue String s public MapValue public MapValue ValueMap values Note that there is a special constructor for SeqValue that takes a Java string This creates a VDM seg of char but without the need to create a ValueList with CharacterValues If the ValueList or another collection passed to these constructors contains a mixture of VDM types i e a mixture of VDM Value subclasses such as a BooleanValue and a NaturalOneValue
15. When using a function composition f comp g this ensures that the precon dition of g implies the precondition of f applied to the result of g function iteration When using a function iteration for the function we are iterating with this ensures that the precondition on an argument implies the precondition on the result function parameter patterns When using a pattern as a function parameter this ensures that all values in the parameter type for the function can match the pattern function satisfiability For all implicit function definitions this proof obligation will be generated to ensure that it is possible to find an implementation satisfying the post conditions for all arguments satisfying the pre conditions 129 E Overture VDM 10 Tool Support User Guide let be st existence Whenever a let be such that expression statement is used you need to be cer tain that at least one value will match the such that expression map apply Whenever a map application is made you need to be certain that the argument is in the domain of the map map compose When composing 2 maps ensures that the range of map2 is a subset of the domain of mapl map compatible Mappings in VDM represent a unique relationship between the domain values and the corresponding range values Proof obligations in this category are meant to ensure that such a unique relationship is guranteed map iteration When performing a map iteration ensures the itera
16. at end of block g atomic g after atomic g after atomic assignments g after call operation name g after new class name g while g do after while expression g for g in set after for all g in set after for all g do after for all expression g in after pattern bind g do before loop statement 99 Overture VDM 10 Tool Support User Guide 2216 2217 2218 2219 2220 2221 2222 2223 2224 2225 2226 2227 2228 2229 2230 2231 2232 2233 2234 2235 2236 2237 2238 2239 2240 Expecting Expecting to Expecting do Missing then Missing then Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin g g g g g g g g g g g g g F xim F xm db Ed statement block Tr after for variable after els after from expression before loop statement if xpression in object assignment statement in state assignment statement after map seq reference after statement rj Ter at end of statement block A after declarations name type in declaration return leur rin after local defin
17. id Options Compatibility Extension E Paste Cv V Adding Modelio annotations cum X Delete f i BR mo Rename inks Editor 28 Macros By Desd T Ba Desq a Check model E Copy Compatibility EMF UML30 0 uml li Create Update automatic diagrams gt Model Components tun M BE Import XMI Litems selected 28 Export XMI Figure 12 1 Exporting UML definitions from Modelio Importing and exporting a UML model is an option in the Overture Explorer view Exporting Right click a VDM or VDM RT project to access a submenu for UML Transfor mation From here it is possible to Convert to UML The resulting um1 file will be saved to the generated folder of your project 45 E Overture VDM 10 Tool Support User Guide Importing To perform a UML import you must have the um1 file in the relevant project folder You can either copy it manually or use the Eclipse Import File System feature Afterwards it is possible to right click the uml file and choose the submenu for UML Transformation and then select Convert to VDM The mapping rules between VDM VDM RT and UML models are further explained in Ap pendix H Note that the mapping depends on the settings selected in the Preferences menu see Figure 4 7 above The general explanation of these options are Prefer associations during translation If this option is chosen ticked references to instances of other classes will be modelled a
18. 16 3 Your new launch configuration can be started immediately by clicking the Run button at the bottom of the dialog Alternatively the configuration can simply be saved by clicking Apply Once a launch configuration has been defined it can be re run at any time by using the small downward arrow next to the run or debug icons in the IDE toolbar You will see type checking errors at the top of the dialog if you do not do this such as Error 3063 Too few arguments in 2Those familiar with VDMTools will recognise this functionaility as initialising a specific VDM model and then having a prompt where different expressions can be evaluated making use of the definitions from the model 23 E Overture VDM 10 Tool Support User Guide A launch configuration can either be started normally which will simply evaluate the expres sion given and stop or it can be started in debug mode which will stop the evaluation at any break points you may have set The same launch configuration can be used for either purpose though by default those created through the Run Configurations dialog will appear in the favourites list under the Run toolbar icon Similarly a launch configuration created under the Debug Configu rations dialog will appear under the favourites of the debug toolbar icon You can control which icons display the launch configuration in the Common tab on the dialog This is standard Eclipse behaviour VDM
19. 4058 4059 4060 4061 4062 4063 4064 4065 4066 4067 Sequence does not contain key lt key gt Object designator is not a map sequence operation or function Object does not contain value for field lt name gt No such field lt name gt Cannot execute specification statement ris subclass responsibility statement reached Value lt value gt is not in set bind Value lt value gt is not in set bind Cannot apply implicit function lt name gt Wrong number of arguments passed to lt name gt Parameter patterns do not match arguments Precondition failure lt pre_name gt This error occurs if a pre condition to a function or operation is violated Postcondition failure lt post_name gt This error occurs if a post condition to a function or operation is violated Curried function return type is not a function Value lt value gt is not a nati Value lt value gt is not a nat Type invariant violated for lt type gt No such key value in map lt key gt Cannot convert non injective map to an inmap Duplicate map keys have different values lt domain gt Value value is not a nati number Value value is not a nat Cannot call implicit operation name Deadlock detected 123 Overture VDM 10 Tool Support User Guide 4068 4069 4071 4072 4073 4074 4075 4076 4077 4078 4079 408
20. Cea Figure 4 3 Adding New Libraries DM Unit are available for all VDM dialects also when a flat VDM All these libraries except V SL specification is used VDM SL Unit use object orientation and thus it cannot be used with VDM 4 5 Setting Project Options There are various VDM specifi c settings for an Overture project You can change these by selecting a project in the Explorer view and then right clicking and selecting Properties See Figure 4 4 The options that can be set for each VDM project are Language version Here the default is to use the classic version which is similar to that used in VDMTools Alternatively you can select VDM 10 which is a new improved but not 16 CHAPTER 4 MANAGING OVERTURE PROJECTS E e Properties for Hotel gj pa type filter text VDM Settings er Ma Resource Builders Language options Project References Language version classic Refactoring History Run Debug Settings Type checking VDM Build Path Suppress warnings VDM Settings Restore Defaults Apply Ro Goes Figure 4 4 Overture Project Settings necessarily backwards compatible version of the VDM dialects developed by the Overture VDM Language Board Suppress type checking warnings Warnings are enabled by default but you can change it here Overture allows VDM specifications to be embedded in TEX files that form part of the docu mentation o
21. Eclipse platform The project is managed on GitHul The best way to run Overture is to download a special version of Eclipse with the Overture functionality already pre installed If you go to http overturetool org download you will find pre installed versions of Overture for Windows Linux and Mad Modelio In order to take advantage of the UML VDM mapping a tool for UML modelling is needed We recommend Modelio This is a tool that is both available in a commercial version as well as in an open source setting from a company called Softeam Just like Overture this tool is built on top of the Eclipse platform The product can be obtained from http www modelio org Note that in order to be able to execute Overture you need to have Java Runtime Environment minimum version 1 6 installed on your computer When you start Overture for the first time it will request a workspace location We recommend that you choose the default location proposed by Overture and tick the box for Use this as the default and do not ask again A welcome screen will introduce you to the overall mission of the Overture open source initiative the first time that you run the tool and provide you with a number of interesting pointers of additional material see Figure 2 1 You can always get back to this page using Help Welcome Finally in order to make use of the test coverage feature described in Section 7 it is necessary to have the text processing sys
22. Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin g g g g g g g g Faf E end FoU in last in after map enumeration after list comprehension after list enumeration after elseif after cases expression after others after case after cases pattern list after local definitions after be in let expression after bind in let expression after bind list in forall after bind list in exists after single bind in existsl after single bind in iota after bind list in lambda after equals definitions after new c after after after after after after isofbase isofclass isofclass samebaseclass samebaseclass lass name isofbase args rw args rw args 97 Overture VDM 10 Tool Support User Guide 2166 2167 2168 2169 2170 2171 2172 2173 2174 2175 2176 2177 2178 2179 2180 2181 2182 2183 2184 2185 2186 2187 2188 2189 2190 Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin g g g g g g g g Malformed after sameclass after sameclass args top name s top name s module at module start end after module definitions dlmodule
23. PP Launch Configurations p mx Create manage and run configurations No Module specified FEB XIE Name AlarmSL type filter text B Main Runtime E Source E Common Debugger Develop 4 amp VDM PP Model Project AlarmPP i T ye Project AlarmSL Browse ArchitectureStateMa de m CMRT Launch Mode 4 Mi VOM ET Mode Entry Point Remote Control Console i CMRT Run a VDM SL Model Entry Point Ki AlarmsL Module Search Function Operation Remote Control Fully qualified remote control class Other V Generate coverage Filter matched 8 of 8 items IAN SSS Q Debug Close Figure 6 1 The launch configuration dialog Whenever a launch configuration is started up it is also possible to decide upon which additional run time checks to carry out By default all possible run time checks are swiched on but if desired some of these can be swiched off using the Runtime pane see Figure 6 2 Note that for VDM RT debugging it is also possible to switch off the logging of all events appearing during the debugging The different run time checks that can be performed are Dynamic type checks This is an option for the interpreter default on to continuously type check values during interpretation of a VDM model It is possible to switch off the check herd However a consequence of doing that is that you may get internal Java errors null pointer or class cast exceptions typi
24. a certain timeframe from the trigger event seperate The separation properties are used to describe a minimum separation between events 1f the second event occur at all In Overture validation conjectures are evaluated over the execution trace at run time and in case violations occur they will be written to a violations file with txt extension The violations file is located in the log file directory and named by the time of execution When this file is loaded using the 4 button Overture will list the violations as shown in Figure 14 4 In particular this figure shows two violations of the validation conjecture in listing 14 1 In addition the RealTime Log viewer will show the violations graphically by marking the trigger and corresponding response in the model execution overview Figure 14 5 shows the two violations from Figure 14 4 Note that the trigger for the second violation occurs at the same time as the response for the first one Therefore they are both marked by the same red circle the middle one 51 E Overture VDM 10 Tool Support User Guide status name expression src time srcthread desttime dest thread ANR C1 separate fin MMTUpdateScreen fin MMTUpdateScreen 500000000 118254267 14 209165360 15 Cl separate fin MMTUpdateScreen fin MMTUpdateScreen 500000000 209165360 15 300076453 16 Figure 14 4 Violations of validation conjectures will be listed in a table VDM RT Realtime Log Viewer 23 E m
25. adding new empty files it is possible to add existing standard libraries This can be done by right clicking on the project where the library is to be added and then selecting New Add VDM Library That will make a new window as shown in Figure Here the different standard libraries provide different standard functionalities In the body of many of these function s operations are declared as is not yet specified but the actual functionality for all of these are hard coded into Overture so the user can get access to this when the respective standard libraries are included This can be summarised as IO This library provides functionality for input and output from to files and the standard console Math This library provides functionality for standard mathematical functions such as sine and cosine Util This library provides functionality for converting different kind of VDM values mainly to and from files and strings 15 Overture VDM 10 Tool Support User Guide CSV This library is an extension of the IO library which provides additional functionality for saving and reading VDM values to from comma separate format used by excel spreadsheets VDM Unit This library provides functionality for unit testing of VDM models similar to the well known JUnit library Add Library Wizard Add Library Select libraries to include 10 Math Util E csv VDM Unit a Select the libraries to include
26. as the Remote Controller technique is utilized This is done to enable the VDM model to display data directly to the Java GUI and to allow the VDM model to be controlled from the Java GUI The example is based on a VDM model of the smokers concurrency problem Patil71 Consider a scenario where three chain smokers and an agent who does not smoke are sitting at a table infinitely going through the following lifecycle 1 Each chain smoker continuously seeks to roll a cigarette and smoke it 2 a smoker needs three ingredients tobacco paper and matches 3 each smoker has an infinite supply of only one of the ingredients One of the smokers has tobacco the second has paper and the third has matches 4 the agent has an infinite supply of all three materials and randomly places two different ingredients on the table at a time 5 the smoker who has the remaining ingredient then empties the table rolls a cigarette and smokes it The smokers never accumulate the ingredients and never grab an ingredient from the table which they are already in possession of 6 when the table becomes empty the agent puts another two random ingredients on the table and the cycle repeats In this example a GUI has been created for the model in which the user of the GUI is considered to be the agent providing the smoker with ingredients as illustrated in Figure 15 1 By clicking one of three buttons one of the respective ingredients will be placed
27. at module start end after dlmodule definitions imports Expecting exports section Expectin Expectin Expectin Expectin Expectin g g g g g after export name after export name after export name imports from in import definition Mismatched brackets in pattern Mismatched braces in pattern Mismatched square brackets in pattern Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin g after mk tuple after mk tuple after type record after type record is not yet specified is not yet specified is subclass responsibility exit 98 APPENDIX D SYNTAX ERRORS 2191 2192 2193 2194 2195 2196 2197 2198 2199 2200 2201 2202 2203 2204 2205 2206 2207 2208 2209 2210 2211 2212 2213 2214 2215 Expectin Expectin Expectin Expectin Expectin Expectin Expectin q trxet a PTT after eat g after pattern bind g in after tixe traps g trap g with in trap statement g in in trap statement Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin g always g in after always statement go tp g after g
28. by Overture Since VDM modelling languages have a formal mathematical semantics a wide range of ana lyses can be performed on models both to check internal consistency and to confirm that models have emergent properties Analyses may be performed by inspection static analysis testing or Formerly called VDM In a Constrained Environment VICE See E Overture VDM 10 Tool Support User Guide mathematical proof To assist in this process Overture offers tool support for building models in collaboration with other modelling tools to execute and test models and to carry out different forms of static analysis Larsen amp 13 It can be seen as an open source version of the closed but now freely available tool called VDMTools Elmstr m amp 94 LarsenO Fitzgerald amp O8b This guide explains how to use the Overture IDE for developing models for different VDM dialects It starts with an explanation of how to get hold of the software in Chapter 2 This is followed in Chapter 3 with an introduction to the Eclipse workspace terminology Chapter 4 ex plains how projects are managed in the Overture IDE Chapter 5 covers the features for creating and editing VDM models This is followed in Chapter 6 with an explanation of the interpreta tion and debugging capabilities in Overture Chapter 7 illustrates how test coverage information can be gathered when models are interpreted Chapter 8 shows how models with test coverage informa
29. exp This command is only available for the VDM and VDM RT dialects It creates a global variable that can be used subsequently in the interpreter It is mostly used for creating global instances of classes 71 E Overture VDM 10 Tool Support User Guide log lt file gt off This command can only be used with VDM RT models It starts to log real time events to the file indicated By default event logging is turned off Log ging can be directed to the console by using log with no arguments or to a file using log lt filename gt Logging can subsequently be turned off again by using log off The events logged include requests activations and completions of all functions and operations as well as all object creations creation of CPUs and BUSses deployment of objects to spe cific CPUs and the swapping in out of threads state This command can only be used for the VDM SL dialect and shows the default module state The value of the state can be changed by operations called p rint lt expression gt This command evaluates the expression provided in the current context runtrace lt name gt test number This command runs the trace called lt name gt This will expand the combinatorial test and execute the resulting operation sequences If a specific test number is provided only that one test from the expansion will be executed debugtrace lt name gt test number This command is the same as runt race except that i
30. fis an exception to this rule VDM concept Property isReadOnly Instance variables false Values true Table H 1 The meta attribute isReadOnly distinguishes instance variables and values Transformation Rule 7 The initial value of instance variables and values definitions are mapped as the property default of the UML meta class Property Transformation Rule 8 The VDM optional type is mapped to the properties Lower Qandupper 1 of the UML meta class Transformation Rule 9 The VDM constructs set seq and seq1 is mapped as the UML meta class Association which may be deco rated with a textual constraint defined by the meta attribute isOrde red lin addition to a multiplicity at both ends Ta ble shows how the above mentioned VDM constructs are mapped VDM construct Ordered Target class Multiplicity set false O seq true 0 x seq true lux Table H 2 Transformation rules for VDM constructs mod eling collections 134 APPENDIX H MAPPING RULES BETWEEN VDM VDM RT AND UML MODELS E Transformation Rule 10 The VDM constructs map and inmap are mapped as the UML meta class Association with a qualifier The do main is specified by the qualifier which is located at the source class The range is specified by the target class No tice that if the range is specified by a basic type it is mapped as a separate class This is an exception to ru
31. init command is given or when the command coverage clear is executed otherwise coverage is cumulative If several files are loaded the coverage for just one source file can be listed with coverage lt file gt orlatex lt file gt files This command lists the names of all source files loaded 73 E Overture VDM 10 Tool Support User Guide reload This command will reload parse and type check the VDM model files currently loaded Note that 1f there are any errors in the parse or type check of the files the interpreter will exit after the reload load lt files gt This command replaces the current loaded VDM model files Note that 1f there are any errors in the parse or type check of the files the interpreter will exit after the load q uit This command leaves the interpreter gt modules M default gt state O4 mk M FREE 0 9999 rseed 87654321 Memory mk Memory 87654321 mk_M lt FREE gt 0 9999 mk_M lt FREE gt 0 9999 Q3 mk_M lt FREE gt 0 9999 gt print rand 100 EU Executed in 0 063 secs print rand 100 44 Executed in 0 0 secs gt state O4 mk M FREE 0 9999 rseed 566044643 Memory mk_Memory 566044643 mk_M lt FREE gt 0 9999 mk_M lt FREE gt 0 9999 Q3 mk_M lt FREE gt 0 9999 gt init Global context initialized gt state O4 mk_M lt FREE gt
32. intValue null set smoker ctrl DisableButtons prevent new GUI input model finishedSmoking wait for smoker to finish ctrl EnableButtons enable GUI input Listing 15 5 Java implementation of the VDM interface for the external Java library In order to use the VDM Types the Java implementation must have the Overture java library in its build path The library can be found in Overture installation directories under lt Overturedir gt Plugins e org overture ide core _x x jars Ast jar Contains the Abstract Syntax Tree with all the static language definitions Parser jar Contains the VDM parser e org overture ide debug x xMjarsN Interpreter jar Contains the interpreter and the values which is what external Java implementations mainly will use e org overture ide builder vdmj x xMjarsN 39 E Overture VDM 10 Tool Support User Guide TypeChecker jar Contains the type checker this is used when e g comparing types These can then be added to the Java build path as shown in Figure The alternative is to use the command line Overture x x x Jar file as described in chapter 16 and add that to the Java build path since this contains all of the above Jars in a single file CA type filter text Java Build Path PN D Resource Builders 8 Source L gt Projects BA Libraries amp Order and Export Java Build Path
33. model all text outside vdm a1 will be ignored Properties for RTTest type filter text Latex Resource Latex options Builders Main document RT Test tex Project References Refactoring History Browse V Generate main document Run Debug Settings V Insert coverage tables Y Mark coverage VDM Build Path Y Model only 4 VDM Settings Restore Defaults Apply m Figure 8 1 The BIEX project properties window 33 Overture VDM 10 Tool Support User Guide 34 Chapter 9 Managing Proof Obligations In all VDM dialects Overture can identify places where run time errors could potentially occur if the model was to be executed The analysis of these areas can be considered as a complement to the static type checking that is performed automatically Type checking accepts specifications that are possibly correct but we also want to know the places where the specification could possibly fail Unfortunately it is not always possible to statically check if such potential problems will actu ally occur at run time error or not So Overture creates Proof Obligations for all the places where run time errors could occur Each proof obligation PO is formulated as a predicate that must hold at a particular place in the VDM model if it is error free and so it may have particular context information associated with it POs can be considered as constraints that will guarantee the internal integrity of a VDM m
34. passing the Value required public TokenValue Value exp 14 5 Tuple Values A TupleValue in Overture is a wrapper for a ValueList The following method and con structor can be used like one would expect public TupleValue ValueList argvals public ValueList tupleValue Context ctxt 1 4 6 Invariant Values A VDM type can be given a name and an invariant e g when wrapping a primitive type without an invariant Overture has a separate Value subclass for values of such types that simply combine the primitive Value with a FunctionValue for the invariant However as with RecordValues which can also have invariants it is not currently possible to create InvariantValues in Java for types that have an invariant For types without an invariant the constructor is as follows public InvariantValue NamedType type Value value Context ctxt The NamedType is obtained in a similar way to the RecordType above using the Remote Interpreter Note that the caller is responsible for passing a Value that matches the expected type If they do not match Overture will throw a dynamic type exception for subsequent evalua tions L4 7 Void Values Operations which do not return a value in VDM i e gt return an instance of VoidValue in Java The constructor has no arguments 143 Index architecture overview assert break BUS classes code generation
35. state variable lt name gt in assignment Cannot assign to ext rd state lt name gt Object designator is not a map sequence function or operation Map application must have one argument Map application argument is incompatible type Sequence application must have one argument Sequence argument is not numeric Too many arguments Too few arguments Inappropriate type for argument lt n gt Too many arguments Too few arguments Inappropriate type for argument lt n gt Unknown class member name lt name gt 115 Overture VDM 10 Tool Support User Guide 3261 3262 3263 3264 3265 3266 3267 3268 3269 3270 3271 3272 3273 3274 3275 3276 3277 3278 3279 3280 3281 3282 3283 3284 3285 Unknown field name lt name gt Field assignment is not of a class or record type Cannot reference self from here At least one bind cannot match set At least one bind cannot match this type Argument is not an object Empty map cannot be applied Empty sequence cannot be applied Ambiguous function operation name name Measure name is not in scope Measure name is not an explicit function Measure result type is not a nat or a nat tuple Measure not allowed for an implicit function External variable is not in scope name Error clause must be a boolean Ambiguous names inh
36. step through the evaluation to the place where it is failing You can inspect the exact circumstances of the failure including the values of the different variables in scope Note that this is only available for VDM SL and VDM RT models if the VDM 10 language version has been selected 37 Overture VDM 10 Tool Support User Guide Project Run Window Help 3 Combinatorial testi vdmpp 23 expert vdmpp 16 tracker vdmpp Era 43 operations public Run gt set of Plant Period Expert Run let periods plant ExpertIsOnDuty ex1 expert plant ExpertToPage al p1 in return mk periods expert traces AddingandDeleting let myex in set exs in let myex2 in set exs myex in let p in set ps in plant AddExpertToSchedule p myex plant AddExpertToSchedule p myex2 plant RemoveExpertFromSchedule p myex MP Test 000001 Test 000002 6 Test 000004 4 Test 000005 Test 000006 Test 000007 Test 000008 Test 000009 SP Test 000010 PE Test 000011 XX Test 000012 f Test 000013 f Test 000014 f Test 000015 plant RemoveExpertFromSchedule p myex2 H lt Test 000016 45 9 Test 000017 im o 2 Problems E Console E cr Test Case resul 33 ILI Trace Test case Result ES plant AddExpertToSchedule mk_token Tuesday day myex i plant AddExpertToSchedule mk token Tuesday day myex2 0 plant RemoveExpertFromSchedule mk_token Tuesda
37. that will ensure termination of the recursion 5014 Uninitialized BUS ignored This warning appears if one has defined a BUS that is not used 5015 LaTeX source should start with comment or Nsubsection 5016 Some statements will not be reached 119 document section Overture VDM 10 Tool Support User Guide 120 Appendix F Run Time Errors When using the interpreter debugger it is possible to get run time errors even if there are no type checking errors The possible errors are as follows 4000 4002 4003 4004 4005 4006 4007 4008 4009 4010 4011 4012 4013 4014 4015 4016 Cannot instantiate abstract class class Expression value is not in set bind Value value cannot be applied No cases apply for lt value gt Duplicate map keys have different values Type type has no field field No such field in tuple lt n gt No such type parameter lt name gt in scope Type parameter local variable name clash lt name gt Cannot take head of empty sequence Illegal history operator lt op gt Cannot invert non injective map Iota selects more than one result Iota does not select a result Let be st found no applicable bindings Duplicate map keys have different values lt domain gt 121 Overture VDM 10 Tool Support User Guide 4017 4018 4019 4020 4021 4022 4023 4024
38. witha cov extension will be created for each file in the project These files are written into a project subfolder named generated coverage lt date and time gt Double clicking the cov files will open a special editor window that displays the source with coverage coloured in red green red is executable but not covered Alternatively a PDF file containing the entire model with coloured test coverage summarised for all runs can be generated by right clicking on the project name and selecting Latex Latex Coverage 3l Overture VDM 10 Tool Support User Guide 32 Chapter 8 Pretty Printing to IATEX It is possible to use literate programming specification with Overture just as you can with VDMTools To take advantage of this you need to use the TEX text processing system with plain VDM models mixed with textual documentation The VDM model parts must be enclosed within begin vdm_al and end vdm_al The text parts outside these specifica tion blocks are ignored by the VDM parser though note that each source file must start with a recognizable IATEX construct a documentclass section subsection ora BIEX comment When using this functionality it is possible to configure additional options for the PdfLatex generation in the project properties see Figure 8 1 For example you can choose whether to use an auto generated main tex file or a user provided one It is also possible to generate a pdf containing only the
39. x x x jar file contains a MANIFEST that identifies the main class to start the tool so the minimum command line invocation is as follows java jar Overture x x x jar Overture You must specify either vdmsl vdmpp or vdmrt Usage Overture vdmsl vdmpp vdmrt gt lt options gt lt files gt The first parameter indicates the VDM dialect to use and then various extra options can be used These are r This indicates the VDM release number classic or vdm10 w This will suppress all warning messages q This will suppress all information messages such as the number of source files processed etc i This will start the command line interpreter if the VDM model is successfully parsed and type checked otherwise the errors discovered will be listed p This will generate all proof obligations for the VDM model if it is syntax and type correct and then stop 0 exp This will evaluate the exp print the result and stop 69 E Overture VDM 10 Tool Support User Guide c lt charset gt This will select a file character set to allow a specification written in languages other than the default for your system t charset This will select a console character set The output terminal can use a different character set to the specification files o filename This will save the internal representation of a parsed and type checked spe cification Such files are effectivel
40. 0 4081 4082 4083 4084 4085 4086 4087 4088 4089 4090 4091 4092 4093 Wrong number of arguments passed to lt name gt Parameter patterns do not match arguments Precondition failure pre name Postcondition failure post name gt Cannot convert type parameter value to lt type gt Cannot convert value to type Value value is not an integer Value value is not a nati Value value is not a nat Wrong number of fields for lt type gt Type invariant violated by mk arguments Wrong number of fields for lt type gt Field not defined lt tag gt Type invariant violated by mk arguments Sequence index out of range lt index gt Cannot convert empty sequence to seql Cannot convert tuple to type Value of type parameter is not a type Cannot convert value kind to type Set not permitted for kind Can t get real value of kind Can t get rat value of lt kind gt Can t get int value of lt kind gt Can t get nat value of lt kind gt Can t get natl value of lt kind gt 124 APPENDIX F RUN TIME ERRORS 4094 4095 4096 4097 4098 4099 4100 4101 4102 4103 4104 4105 4106 4107 4108 4109 4110 4111 4112 4113 4114 4115 4116 4117 4118 Can t get bool value of kind Can t get char value of kind Can t get tuple value of lt kind g
41. 1 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 Malformed quoted character Invalid char ch in base n number Expecting Expecting Expecting Expecting Expecting p gt close double quote close quote after character Unexpected tag after Malformed module name Unexpected character c Expecting lt digits gt lt digits gt e lt gt lt digits gt Unterminated block comment 89 Overture VDM 10 Tool Support User Guide 90 Appendix D Syntax Errors If the syntax of the file you have provided does not meet the syntax rules for the VDM dialect you wish to use syntax errors will be reported These can be as follows 2000 Expectin 2001 Expecting in set in set bind 2002 Expecting in type bind 2003 Expectin g in set after pattern in set binding g in set after pattern in binding 2004 Expecting in set or after patterns 2005 Expecting list of class or system definitions 2006 Found tokens after cl 2007 Expecting end class lass definitions 2008 Class does not start with class 2009 Can t h 2010 Can t h 2011 Only on 2012 Can t h ave instance variables in VDM SL ave a thread clause in V DM SL e thread clause permitted per class ave a sync clause in VDM SL 2013 Expected operations
42. 278 2279 2280 2290 2291 2292 2293 2294 2295 2296 2297 2298 2299 Expecting n or nl n2 after trace definition Expecting obj op args or op args Expecting id id args Expecting trace definitions Only value definitions allowed in traces Expecting duration Expecting duration Expecting after duration Expecting cycles Expecting cycles Expecting after cycles Can t have state in VDM Async only permitted for operations T Invalid breakpoint hit condition System class cannot be a subclass System class can only define instance variables and a constructor M reverse not available in VDM classic Expecting amp 2 Expecting a D Expecting ending clause Can t use old name here Block cannot be empty Expecting 5 in map pattern Map patterns not available in VDM classic Expecting gt empty map pattern 102 APPENDIX D SYNTAX ERRORS 2300 mk type must have a single argument 2301 Expecting narrow expression type 2302 Expecting after narrow expression 2303 Narrow not available in VDM classic 2304 stop not available in VDM classic 2305 stoplist not available in VDM classic 2306 Expecting stop 2307 Expecting stop 2308 Expecting after stop object
43. 3 2124 2125 2126 2127 2128 2129 2130 2131 2132 2133 2134 2135 2136 2137 2138 2139 2140 Expecting lt name gt gt lt exp gt Expecting after mutex Expecting after all Expecting Expecting el e2 in subsequence Expecting after subsequence Expecting after function args Expecting after function instantiation Expecting Expecting is not yet specified Expecting is not yet specified Expecting is subclass responsibility Expecting comma separated record modifiers Expecting identifier lt expression gt Expecting after mu maplets Expecting after mk tuple Expecting is expression type Expecting after is expression Expecting pre function args Expecting in empty map Expecting after set comprehension Expecting el e2 in set range Expecting after set range Expecting after set enumeration Expecting after map comprehension 96 APPENDIX D SYNTAX ERRORS 2141 2142 2143 2144 2145 2146 2147 2148 2149 2150 2151 2152 2153 2154 2155 2156 2157 2158 2159 2160 2161 2162 2163 2164 2165 Expecting Expecting Expecting Missing then Missing then Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin Expectin
44. 39 combinatorial testing command assert break classes continue coverage create default down env files init latex latexdoc list load log modules next out pog print quit reload remove source stack state step stop threads trace up continue Convert to UML Convert to VDM 46 coverage CPU create create real time project creating VDM class VDM RT class VDM SL module debug configuration debug perspective 26 default down examples import explorer export image button file extension files Go to time icon fail verdict inconclusive verdict 37 144 INDEX not yet executed pass verdict 37 resume debugging 26 skipped test case step into step over step return suspend debugging terminate debugging use step filters 26 init latex latexdoc launch configuration mode line number line numbers list load log model execution overview Modelio modules next out outline perspective combinatorial testing 37 debug proof obligation VDM pog print problems project close 9 create open 9 options proof obligation perspective proof obligation categories quick interpreter quit RealTime Log viewer reload remove single CPU overview source stack state step stop Test Coverage Test suite threads trace trac
45. 978 One of several examples of ALGOL 60 descriptions Information technology Programming languages their environments and system software interfaces Vienna Development Method Specification Language Part 1 Base language December 1996 The VDM Tool Group The Java to VDM User Manual Technical Report CSK Systems January 2008 C W Johnson Literate Specifications Software Engineering Journal 225 237 July 1996 C B Jones The Meta Language A Reference Manual In The Vienna De velopment Method The Meta Language pages 218 277 Springer Verlag 1978 C B Jones The Vienna Development Method Examples of Compiler De velopment In Amirchachy and Neel editors Le Point sur la Compilation INRIA Publ Paris 1979 Cliff B Jones Systematic Software Development Using VDM Prentice Hall International Englewood Cliffs New Jersey second edition 1990 333 pages ISBN 0 13 880733 7 This book deals with the Vienna Development Method The approach ex plains formal functional specifications and verified design with an emphasis on the study of proofs in the development process T Kurita and Y Nakatsugawa The Application of VDM to the Develop ment of Firmware for a Smart Card IC Chip Intl Journal of Software and Informatics 3 2 3 343 355 October 2009 13 pages 79 Overture VDM 10 Tool Support User Guide Larsen01 Larsen amp 09 Larsen amp 10 Larsen amp 13 Larsen am
46. COPE AND FUNCTIONALITY BY Q LINKING JAVA AND VDM 15 2 Enabling Remote Control of the Overture Interpreter In some situations it may be valuable to establish a front end for example a GUI or a test har ness for calling a VDM model This feature corresponds roughly to the CORBA based API from VDMTools APIMan A VDM model can be remotely controlled by implementing the Java interface Remot eCont rol Remote control should be understood as a delegation of control of the interpreter which means that the remote controller is in charge of the execution or debug session and is responsible for taking action and executing parts of the VDM model when needed When finished it should return and the session will stop When a Remote controller is used the Overture debugger continues working normally so for example breakpoints can be used in debug mode A debugging session with the use of a remote controller can be started by placing the jar with the RemoteControl implementation in a project subfolder called 1ib The fully qualified name of the RemoteControl class must then be specified in the launch configuration in the Remote Control box 15 2 1 Example of a Remote Control Class In this example we have a VDM class A which defines an operation that just returns its argument As seen in listing it is possible to call execute on the Overture interpreter via the Re motelnterpreter object which is passed to the RemoteControl implementation via the run m
47. JARs and class folders on the build path p Java Code Style b fm Overture xxxjar Smoking Add JARs b Java Compiler gt BA JRE System Library JavaSE 1 7 O uu uiu LL gt Java Editor Add External JARs Javadoc Location nt Project References Add Variable Run Debug Settings E Task Tags Add Library Validation Add Class Folder Add External Class Folder Edit Remove Migrate JAR File Figure 15 3 Adding VDMJ library to the build path in Eclipse 60 CHAPTER 15 EXPANDING VDM MODELS SCOPE AND FUNCTIONALITY BY Oo LINKING JAVA AND VDM 15 3 3 Remote Control To enable the GUI to interact with the model the Remote Control technique is utilized by imple menting the RemoteControl interface as shown in Listing 15 6 The RemoteControl interface also requires the Overture Java library to be included in the Java build path as explained above From listing I5 6 it can be seen that the RemoteControl interface supplies protected access to the VDM interpreter that is passed to the SmokingControl object which functions as the bridge between the GUI and the running VDM model The SmokingControl class is specific for this example and its implementation could essentially be implemented directly in the RemoteControl realization It is important the finish method is called on the interpreter when the GUI is disposed this will allow Overture to do a controlled
48. Left hand of operator is not a set Right hand of operator is not a set Left and right of intersect are different types Set range type must be an number Set range type must be an number Left hand of operator is not a set Right hand of operator is not a set Map iterator expects nat as right hand arg Function iterator expects nat as right hand arg xx expects number as right hand arg First arg of must be a map function or number Subsequence is not of a sequence type Subsequence range start is not a number Subsequence range end is not a number Left hand of operator is not a set Right hand of operator is not a set Argument to tl is not a sequence Inaccessible member name of class name Cannot access name from a static context Name name is not in scope Exported function name not defined in module 112 APPENDIX E TYPE ERRORS AND WARNINGS EB 3184 3185 3186 3187 3188 3189 3190 3191 3192 3193 3194 3195 3196 3197 3198 3199 3200 3201 3202 3203 3204 3205 3206 3207 3208 Exported lt name gt function type incorrect Exported operation lt name gt not defined in module Exported operation type does not match actual type Exported type lt type gt not defined in module Exported value lt name gt not defined in module Exported type does not match actual type Import al
49. Meanwhile the Graphics object is created deep inside the VDM model and the SmokingControl object cannot be passed to it through the interpreters execute method Instead the bridge between the Controller and the SmokingControl object is kept in Java and the insider knowledge that the Controller object will eventually be created from inside the model is used to justify the static reference This is a special case when combining the Remote Control technique with the External Java Library method Example of how to shut down a JFrame when using the remote controller interface It is important that the execution of a remote GUI is stopped in a controlled manner e g not just by calling System exit 0 One way to allow the finish method to be called from a JFrame is shown in listing 15 9 The in the constructor of the JF rame a the default close operation is changed to be DISPOSE_ON_CLOSE this will change the closing of the window so that the dispose method is called where call to the interpreter finish can be placed public MyJFrame Allow Overture to do a controlled shutdown 62 CHAPTER 15 EXPANDING VDM MODELS SCOPE AND FUNCTIONALITY BY Q LINKING JAVA AND VDM setDefaultCloseOperation WindowConstants DISPOSE_ON_CLOSE GOverride public void dispose interpreter finish Listing 15 9 Java implementation of a finish method for a JFrame 15 3 4 Deployment of the Jav
50. Overture Technical Report Series No TR 002 September 2015 Overture VDM 10 Tool Support User Guide Version 2 3 0 by Peter Gorm Larsen Kenneth Lausdahl Peter Tran J rgensen Joey Coleman Sune Wolff and Luis Diogo Couto Aarhus University Department of Engineering Finlandsgade 22 DK 8000 Arhus C Denmark Nick Battle Fujitsu UK Lovelace Road Bracknell Berkshire RG12 8SN UK Overture Open source Tools for Formal Modelling Overture VDM 10 Tool Support User Guide Document history Month Year Version Version of Overture January 2010 0 1 5 March 2010 0 2 May 2010 1 0 2 February 2011 2 1 0 0 June 2011 3 1 0 1 August 2013 4 2 0 0 January 2015 5 2 1 6 April 2015 5 2 2 4 September 2015 6 2 3 0 Contents 1 Introduction 2 Getting Hold of the Software 3 Using the VDM Perspective 3 1 Understanding Eclipse Terminology HR nn 3 2 1 Opening and Closing Projects poa NEED paa e D De oo Bea du 3 2 4 Including line numbers in the Editor 4 Managing Overture Projects 4 1 Importing Overture Projects 4 2 Creating a New Overture Project 43 Creating FUES na a Sd dd ne ue Die Que Dr no 4 4 Adding Standard Libraries 4 5 Setting Project Options 444 cor eee ete ete
51. Support User Guide interpreter valueExecute w agent AddPaper public void finish interpreter finish A Listing 15 7 Java implementation of the bridge between the GUI and the interpreter executing the VDM model addPaperButton addActionListener new ActionListener public void actionPerformed ActionEvent e smoke AddPaper Listing 15 8 Java implementation of the Button click action invoking the remote intepreter The last thing to note in Listing 15 7 is the constructor which adds itself to a public static field in the Controller class This step is necessary to brigde the objects created by the Remote Control technique with the objects created in connection with the External Java Library technique To understand why this construct is needed some insight into the initialization steps is necessary Firstly the entire VDM model and thereby the Graphics object is created via the RemoteControl interface by SmokingControl Now recall from Listing 15 5 that the Controller class of the MVC pattern is created when the init method of the Graphics class is invoked from the VDM model meaning that the actual graphical Java components are also created when init is called Now in order to connect a click on the GUI buttons with the commands that can be executed in the model the Controller needs to have access to the interpreter i e the SmokingControl object
52. The next step enables inclusion of VDM libraries and 8 Click the Finish button see Figure 4 2 4 3 Creating Files Switching to the VDM perspective will change the layout of the user interface to focus on VDM development To change perspective go to the menu Window Open perspective Other and choose the VDM perspective From this perspective you can create files using one of the following methods 1 Choose File New gt VDM SL Module or VDM PP Class or VDM RT Class or 2 Right click on the Overture project where you would like to add a new file and then choose New VDM SL Module or VDM PP Class or VDM RT Class In both cases you need to choose a file name and optionally choose a directory if you do not want to place the file in the home directory of the chosen Overture project Then a new file with the appropriate file extension according to the chosen dialect vdmsl vdmpp or vdmrt will be created in the directory This file will use the appropriate module class template to get you started Naturally keywords that are not required can be deleted from the template 14 CHAPTER 4 MANAGING OVERTURE PROJECTS EB New Project gt B VDM Project Chose location for VDM project Project name Tour Y Use default location C TEMP Overturelde 0 3 0 workspace Tour Working sets Add project to working sets Figure 4 2 Create Project Wizard 4 4 Adding Standard Libraries In addition to
53. Value Context ctxt throws ValueException public String quoteValue Context ctxt throws ValueException Note that all of these conversion functions take a Context parameter as argument and po tentially throw a ValueException The Context parameter is used internally by Overture and represents the call stack during the evaluation of an expression This parameter can be set to null when using these methods in Java code outside Overture A ValueException is thrown if the VDM value cannot be converted into the Java type requested For example calling booleanValue ona RealValue object will raise a ValueExcept ion with the message text Can t get bool value of real L3 Sets Sequences and Maps VDM allows primitive types to be built into more complex aggregations and collections and these can also be converted to and from Java types though the process is a little more involved Three classes are provided to assist with this conversion ValueSet ValueList and ValueMap all within the same org overture interpreter values package These classes represent respectively a Java Set List and Map of VDM values public class ValueSet extends Vector lt Value gt public class ValueList extends Vector lt Value gt public class ValueMap extends LinkedHashMap lt Value Value Note that the ValueSet class is actually based on a Java Vector not a Java Set type though the class does have set semantics no duplicates
54. a Program to Overture Once the Java program has been implemented it must be exported to a Jar file and placed in the lib directory in the Overture VDM projects directory in order for Overture to find it In Eclipse a Jar file can be created through the Export function as illustrated on Figures and 3 Export RE Select A Export resources into a JAR file on the local file system l 5 Select an export destination Ant Buildfiles Archive File 2 File System E Preferences gt Java O JAR file 2 Javadoc I Runnable JAR file E Run Debug Po Breakpoints Eb Launch Configurations gt Tasks Team XML Q Next gt F Cancel Figure 15 4 Exporting in Eclipse Note that it can be very beneficial to check Save the description of this JAR illustrated on Figure 15 6 as this saves the export configuration and makes it a lot faster to redeploy the JAR file to VDM project during development Before running the model in Overture the debug configuration needs to be changed to use the Remote Control The Launch Mode must be change to Remote Control and the fully qualified name of the class implementing the remote control interface must be supplied The debug configuration for the current example is supplied in Figure 15 7 63 E Overture VDM 10 Tool Support User Guide S JAR Export BE JAR File Specification Define which resources should be exported in
55. and signs in the left hand column indicating lines which have been executed or not The percentage coverage of each source file is displayed Typically the testing of a specification will be incremen tal and so it is convenient to be able to save the coverage achieved in each test session and subsequently merge the results together This can be achieved with the write lt dir gt and merge lt dir gt options to the coverage command The write option saves the current coverage information in lt dir gt for each specification file loaded the merge option reads this information back and merges it with the current coverage information For example each day s test coverage could be written to a separate day directory and then all the days merged together for review of the overall coverage at the end latex latexdoc lt files gt This command generates TEX coverage files These are IATEX versions of the source files with parts of the specification highlighted where they have not been executed The IATEX output also contains a table of percentage cover by module class and the number of times functions and operations were hit during the execution The latexdoc command is the same except that output files are wrapped in BIEX document headers The output files are written to the same directory as the source files one per source file with the extension tex Coverage information is reset when a specification is loaded when an
56. ar as Java is concerned these values are opaque there is no equivalent Java construct and the only way to evaluate a VDM function is to let Overture perform that evaluation Similarly Java cannot construct aFunctionValue The only operation that Java can reasonably perform with a FunctionValue is to create a composite function eg f1 comp f2 in VDM or a function iteration e g E xx 3 in VDM using existing FunctionValues In order to do this there are two subclasses of FunctionValue called CompFunctionValue and IterFunctionValue the construc tors for which are as follows public CompFunctionValue FunctionValue f1 FunctionValue f2 public IterFunctionValue FunctionValue function long count These both create new FunctionValues which when evaluated by Overture act as the com position and iteration of the arguments respectively There is a method for obtaining a FunctionValue from a Value but note that this is not an internal Java value unlike other Value methods like realValue It is used as a more convenient way of casting the Value to a FunctionValue public FunctionValue functionValue Context ctxt 1 4 2 Object Values When VDM and VDM RT create new objects using the new operator the resulting values are held as ObjectValues in Overture These are complex types that involve function and opera tion definitions for the object as well as any type value sync threa
57. argument y 2 ath Hy gt alue org overturetool vdmj values M C Object X95 Value O BooleanValue O CharacterValue gt FunctionValue O MapValue O Nilvalue y 95 NumericValue O RealValue RationalValue Integervalue NaturalValue O NaturalOneValue gt O ObjectValue O OperationValue O ParameterValue O QuoteValue O RecordValue gt Of ReferenceValue O Seqvalue 9 SetValue O TokenValue O TupleValue O UndefinedValue gt O VoidValue Figure I 1 Java Value Hierarchy Note that a QuoteValue is constructed with a string This is simply the string value that would appear between angle brackets in VDM for example FAIL would be constructed with the Java string FAI L 138 APPENDIX I USING VDM VALUES IN JAVA EB To convert a VDM value into a Java value the Value class provides a number of conversion methods each of which returns the corresponding Java primitive value or throws an exception if the conversion cannot be made for the VDM type concerned public boolean boolValue Context ctxt throws ValueException public char charValue Context ctxt throws ValueException public double realValue Context ctxt throws ValueException public double ratValue Context ctxt throws ValueException public long intValue Context ctxt throws ValueException public long natValue Context ctxt throws ValueException public long nati
58. ble in VDMTools Java2VDMMan CGManPP The sections below focus solely on the Java code generator available in Overture 11 1 Use of the Java Code Generator The Java code generator can be launched via the context menu as shown in Figure Alter natively this can be done by highlighting the project in the VDM explorer and typing one of the shortcuts associated to this plugin The Java code generator operates in two different modes e Regular mode In this mode the Java code generator produces an Eclipse project with all the generated code Java code generation in this mode can also be initiated using the Ctrl Alt C shortcut e Launch Configuration mode Is currently limited to VDM This mode is like regular code generation except that the Java code generator also prompts the user for a launch con figuration as input for the code generation process Based on this launch configuration the Java code generator constructs an entry point a main method really that serves as an entry point for the generated code Launch configuration based code generation can be initiated using the Ctr1 A1t B shortcut Upon completion of the code generation process the status is output to the console as shown in Figure In particular this figure shows the status of code generating the AlarmPP model available in the Overture standard examples As indicated by the console output the generated 39 E Overture VDM 10 Tool Support User Guide E VDM Ex
59. cally rather than nice clean VDM type errors about mismatched types 24 CHAPTER 6 INTERPRETATION AND DEBUGGING IN OVERTURE EB Invariant checks This is an option for the interpreter default on to continuously check both state and type invariants It is possible to switch off this check here but note that option requires dynamic type checking also to be switched off Pre condition checks This is an option for the interpreter default on to continuously check pre conditions for all functions and operations during interpretation of a VDM model It is possible to switch off this check here Post condition checks This is an option for the interpreter default on to continuously check post conditions for all functions and operations during interpretation of a VDM model It is possible to switch off this check here Measure checks This is an option for the interpreter default on to continuously check recursive functions for which a measure function has been defined It is possible to switch off this check herd In the launch configuration the Debugger pane shown in Figure 6 3 can also be useful in rare cases where one has particularly deep recursion for example This is an advanced setting where one can decide the arguments given to the Java virtual machine for allocation of maximum amounts of space per thread in a VDM model However this option is rarely needed ed VDM PP Launch Configurations 38 Create manage an
60. d lt member gt Cannot write to IO file lt name gt Too many syntax errors This error typically occurs if one have included a file that is in a non VDM format and by mistake have given it a vdm file extension vdms1 vdmpp or vdmrt Too many type checking errors CPU or BUS creation failure Cannot set default name at breakpoint Unknown trace reduction type 87 Overture VDM 10 Tool Support User Guide 0054 0055 0056 0057 0058 0059 0060 0061 0062 0063 0064 0065 0066 0067 0068 Cannot instantiate native object lt reason gt Cannot access native object lt reason gt Native method cannot use pattern arguments lt sig gt Native member not found lt name gt Native method does not return Value Failed in native method lt reason gt Cannot access native method lt reason gt Cannot find native method lt reason gt Cannot invoke native method lt reason gt No delegate class found lt name gt Native method should be static lt name gt T Illegal Lock state Thread is not running on a CPU Exported type name not structured Periodic threads overlapping 88 Appendix C Lexical Errors When a VDM model is parsed the first phase is to gather the single characters into tokens that can be used in the further processing This is called a lexical analysis and errors in this area can be as follows 1000 100
61. d to set of Expert legal map application 3 Plant Plantinv set of Alarm map Period to set of Expert legal map application functions 4 PlantExpertToPage Alarm Period let be st existence 5 Plant ExpertToPage Alarm Period legal map application PlantInv set of Alarm map Period to set of Expert gt 6 Plant ExpertToPage Alarm Period legal map application bool 7 Plant ExpertToPage Alarm Period operation establishes postcondition PlantInv as sch 8 Plant NumberOfExperts Period legal map application Cforall p in set dom sch amp schkp lt gt and 9 Plant ExpertisOnDuty Expert legal map application forall a in set as amp 10 Plant Plant set of Alarm map Period to set of Expert state invariant holds forall p in set dom sch amp exists expert in set sch p amp a a GetReqQuali in set expert GetQuali V Problems E Console PO Proof Obligation View 93 H Cforall as set of Alarm sch map Period to set of Expert amp forall p in set dom sch amp p in set dom sch Figure 9 1 The Proof Obligation perspective 36 Chapter 10 Combinatorial Testing In order to better automate the testing process a notion of test traces has been introduced into VDM and subsequently VDM SL and VDM RT Traces are effectively regular expressions that can be expanded to a collection of test cases Each test case comprises a sequence of operation calls If a user defines a trace it is possible to make
62. d or traces sections defined Therefore Ob jectValues are really opaque to Java and cannot be used directly Like for FunctionValue the ObjectValue class has a method for converting a Value into an ObjectValue public ObjectValue objectValue Context ctxt 141 E Overture VDM 10 Tool Support User Guide 1 4 3 Record Values A VDM record is just a collection of typed field values ARecordValue can be obtained from a Value using the following method which returns a RecordVa lue rather than some other Java representation public RecordValue recordValue Context ctxt To get individual field values from a RecordVa lue two more Java helper types have to be in troduced called FieldMap and FieldValue A FieldValue has the following constructor and represents a record field public FieldValue String name Value value boolean comparable The comparable argument indicates whether this field is used in the value comparison be tween record values A field declared with in VDM would have a false argument but normally this argument would be true and the value must match the record type being used FieldValues are added to a FieldMap which is just a Java List of FieldValues So given a RecordValue its FieldMap can be obtained from a public final field in the object called fie 1dMadl and from there individual FieldValues can be accessed e g fieldMap get 0 name and fi
63. d over the execution trace Later this work has been ex tended in to include run time validation Predefined standard forms of validation 50 CHAPTER 14 ANALYSING LOGS FROM VDM RT EXECUTIONS EB conjectures have been defined directly supporting the validation of a deadline or separation be tween two events called the trigger and the response The trigger event could be the press of a button and the corresponding response may be the update of a display From the standard forms more specific validation conjectures can be constructed In Overture it is possible to specify validation conjectures as comments in the system class Listing provides an example of a validation conjecture requiring the separation of 500 ms between two subsequent screen updates system Distribution Class content omitted timing invariants separate fin MMI UpdateScreen Yfin MMI UpdateScreen 500 ms end Distribution Listing 14 1 Validation conjecture example The concrete syntax for the timing invariants in VDM RT is defined as property trigger ending interval The different kinds of properties that can be used are called deadlineMet A deadline by definition is a time by which something must be finished In real time embedded systems there is typically deadlines that must be respected from when an event happens to its response In our terminology it means that the ending event must happen within
64. d run configurations Debug Ca Xx Bi Name CMRT Run type filter text Main Runtime Ey Source Common Debugger Develop Java Applet Interpreting Java Application Y Dynamic type checks V Invariants checks V Pre condition checks Remote Java Applic VDM PP Model E VDM RT Model VDM Real Time options ls CMRT Run Log Real Time Events E VDM SL Model Y Post condition checks V Measure Run Time checks 4 m Filter matched 13 of 13 item Debug Close Figure 6 2 The launch configuration dialog Note that this feature may not work correctly with the presence of mutually recursive function definitions 25 Overture VDM 10 Tool Support User Guide r VDM PP Launch Configurations pS Eq Create manage and run configurations Debug FE XIE 7 Name AlarmSL type filter text VDM PP Model E VDM RT Model VDM SL Model lo AlarmSL Main Runtime E Source ES Common Debugger gt Develop Java Virtual Machine custom arguments e g Xmx1024M Xss20M Arguments Filter matched 8 of 8 items Apply Revert NE Close Figure 6 3 The launch configuration dialog Table 6 1 Overture debugging buttons Button Explanation Resume debugging Suspend debugging Terminate debugging Step into Step over Step return Use step filters 6 2 The Debug Perspective The Debug Perspective contains all the views com
65. dow like Figure 6 5 will occur Using this it is possible to watch the value of such a variable easily whenever a new stop is reached in the debugging process 24 E Overture VDM 10 Tool Support User Guide Name Value XY pz mapl4 Maplet1 lt D gt gt 4 Maplet 2 lt E gt gt 1 Maplet 3 lt A gt gt 1 Maplet 4 lt C gt gt 5 ep Add new expression Figure 6 5 Example of a watchpoint 6 2 3 The Breakpoints View Breakpoints can be added in any perspective from the Editor view The debug perspective also has a Breakpoints view that lists all current breakpoints allowing you to navigate easily to the location of a given breakpoint disable it or delete it The view is located in the same panel as the Variables view in the upper right hand corner 6 2 4 Conditional Breakpoints Breakpoints can be conditional This is a powerful feature for the developer since it allows you to specify a conditional expression which has to be true for the debugger to stop at the given breakpoint As well as using an expression a conditional breakpoint may specify a hit count and whether the breakpoint should stop when the hit count is equal to greater than or a multiple of the given value or a general expression using the variables in scope at the breakpoint A normal breakpoint can be made conditional by right clicking on the breakpoint mark in the Editor view and selecting Breakpoint Properties This opens a dialo
66. e which is interpreted as private at this place compared to for example an inherited definition 3031 Unknown state variable lt name gt 3032 State variable lt name gt is not this type 3033 Polymorphic function has not been instantiated lt name gt 3034 Function is already instantiated 3035 Operation returns unexpected type 106 APPENDIX E TYPE ERRORS AND WARNINGS EB 3036 Operation parameter visibility less than operation definition This error message typically are caused by using a more restrictive access modifier or none which is interpreted as private at this place compared to for example an inherited definition 3037 Static instance variable is not initialized lt name gt 3038 lt name gt is not an explicit operation 3039 lt name gt is not in scope 3040 Cannot put mutex on a constructor 3041 Duplicate mutex name 3042 lt name gt is not an explicit operation 3043 lt name gt is not in scope 3044 Duplicate permission guard found for lt name gt 3045 Cannot put guard on a constructor 3046 Guard is not a boolean expression 3047 Only one state definition allowed per module 3048 Expression does not return a value 3049 Thread statement operation must not return a value 3050 Type lt name gt is infinite 3051 Expression does not match declared type 3052 Value type visibility less than value definition This error mes sag
67. e precondition of the function implies the post condition recursive function This proof obligation makes use of the measure construct to ensure that a recursive function will terminate sequence apply Whenever a sequence application is used you need to be certain that the argu ment is within the indices of the sequence 130 APPENDIX G CATEGORIES OF PROOF OBLIGATIONS EB sequence modification Whenever a sequence modification is used this ebsures the domain of the modification map is a subset of the indices of the sequence state invariant If a state including instance variables in VDM has an invariant this proof obligation will be generated whenever an assignment is made to a part of the state subtype This proof obligation category is used whenever it is not possible to statically detect that the given value falls into the subtype required tuple selection This proof obligation category is used whenever a tuple selection expression is used to gurantee that the length of the tuple is at least as long as the selector used type invariant Proof obligations from this category are used to ensure that invariants for elements of a particular type are satisfied unique existence binding The iota expression requires one unique binding to be present and that is guranteed by proof obligations from this category value binding When binding a value to a pattern ensures that the resulting value matches the pattern while lo
68. e to update the GUI and it would rely on the 57 E Overture VDM 10 Tool Support User Guide Java implementation to request data on any state changes in the model A VDM model interface has been created which allows the model to interact with the Java GUI the interface is shown in Listing The hierarchical naming pattern of Java packages which normally are separated by periods are denoted with underscores in the VDM model Meaning that with this interface the External Java library must contain a Graphics class which is organized in the gui package class gui_Graphics operations public init gt init is not yet specified public tobaccoAdded gt tobaccoAdded is not yet specified public paperAdded gt paperAdded is not yet specified public matchAdded gt matchAdded is not yet specified public tableCleared gt tableCleared is not yet specified public nowSmoking nat gt nowSmoking smokerNumber is not yet specified end gui_Graphics Listing 15 4 VDM interface for external Java library The Java class implementing the VDM interface is shown in Listing This example will not go into detail with regards to actual GUI implementation however it should be mentioned that the example utilizes the Model View Controller MVC design pattern and that the Java im plementation of the VDM interface interacts with the graphical
69. e typically are caused by using a more restrictive access modifier or none which is inter preted as private at this place compared to for example an inherited definition 3053 Argument of abs is not numeric 3054 Type name cannot be applied 3055 Sequence selector must have one argument 3056 Sequence application argument must be numeric 3057 Map application must have one argument 3058 Map application argument is incompatible type 107 Overture VDM 10 Tool Support User Guide 3059 3060 3061 3062 3063 3064 3065 3066 3067 3068 3069 3070 3071 3072 3073 3074 3075 3076 3077 3078 3079 3080 3081 3082 3083 Too many arguments Too few arguments Y Inappropriate type for argument lt n gt Too many arguments Too few arguments T Inappropriate type for argument lt n gt Left hand of lt operator gt is not lt type gt Right hand of lt operator gt is not lt type gt Argument of card is not a set Right hand of map comp is not a map Domain of left should equal range of right in map comp Right hand of function comp is not a function Left hand function must have a single parameter Right hand function must have a single parameter Parameter of left should equal result of right in function comp Left hand of comp is neither a map nor a function Argument of conc is not a seq
70. eakpoint stop This command terminates the execution immediately threads This command can only be used for the VDM and VDM RT dialects It lists the active threads with status information for each thread 76 References APIMan Battle 10 Bjgrner amp 78a Bj rner78b Bj rner78c Burdy amp 05 CGMan The VDM Tool Group VDM Toolbox API Technical Report CSK Systems January 2008 Nick Battle VDMJ Design Specification Available from the Overture Source Forge repository September 2010 59 pages D Bj rner and C B Jones editors The Vienna Development Method The Meta Language Volume 61 of Lecture Notes in Computer Science Springer Verlag 1978 This was the first monograph on Meta IV See also entries Bj rner78bl Bjorner78c Lucas78 Jones78a Jones78b Henhapl amp 78 D Bjgrner Programming in the Meta Language A Tutorial The Vienna Development Method The Meta Language 24 217 1978 An informal introduction to Meta IV D Bjgrner Software Abstraction Principles Tutorial Examples of an Operat ing System Command Language Specification and a PL I like On Condition Language Definition The Vienna Development Method The Meta Language 337 374 1978 Exemplifies so called exit semantics uses of Meta IV to slightly non trivial examples Lilian Burdy and Yoonsik Cheon and DavidR Cok and Michael D Ernst and Joseph R Kiniry and Gary T Leavens and K Rustan M Lein
71. ect type name is not a matchable field of class class Subset will only be true if the LHS set is empty 118 APPENDIX E TYPE ERRORS AND WARNINGS 3336 Illegal use of RESULT reserved identifier 3337 Cannot call a constructor from here Warnings from the type checker include 5000 5001 Definition name not used Instance variable is not initialized name 5002 Mutex of overloaded operation This warning is provided if one defined a mutex for an operation that is defined using overloading The users needs to be aware that all of the overloaded operations will now by synchronisation controlled by this constraint 5003 Permission guard of overloaded operation 5004 History expression of overloaded operation 5005 Should access member member from a static 5006 Statement will not be reached 5007 Duplicate definition name 5008 lt name location gt hides lt name location gt 5009 Empty set used in bind 5010 State init expression cannot be executed context 5012 Recursive function has no measure Whenever a recursive function is de fined the user have the possibility defining a measure i e a function that takes the same parameters as the recursive function and returns a natural number that should decrease at ev ery recursive call If such measures are included the proof obligation generator can provide proof obligations
72. ed instance or operation called will be sent to the model allowing to interact with it Any responses from the model are also shown in the GUI This feature is currently only available for VDM models 64 CHAPTER 15 EXPANDING VDM MODELS SCOPE AND FUNCTIONALITY BY Q LINKING JAVA AND VDM JAR Packaging Options PS Define the options for the JAR export Select options for handling problems Export class files with compile errors Export class fles with compile warnings Create source folder structure Bydd projects d not buit automatically Y Saye the description cf tha JAR in the workspace Description fe Smoking export jaedesc Browse O Bk Net Gran comcel E Debug Configurations CA E Create manage and run configurations Debug Sex ery Name SmokingEx Main Runtime 4 Source ES Common Debugger Develop ES vom PP Model Project TE Project SmokingEx Browse VDM RT Model ESTES Mouse Entry Point Remote Control Console Entry Point Class World nat simtime Search Function Operation Run Remote Control Fully qualified remote control class gui SmokerRemote Other 7 Generate coverage Apply Revert Filter matched 5 of 5 items O gt Figure 15 7 Changing the Overture debug configuration into using the remote controller 65 Overture VDM 10 Tool Support User Guide C
73. eldmap get 0 value To create a RecordValue the record type is obtained from the RemoteInterpreter type remotelnterpreter getlInterpreter findType typename The type is then passed to the RecordValue constructor along with a FieldMap or a ValueList of the fields in order public RecordValue RecordType type ValueList values Context ctxt public RecordValue RecordType type FieldMap mapvalues Context ctxt The Context parameter is needed to allow records with invariants to check the invariant before the value is constructed Note that currently record types with an invariant cannot be constructed in Java The Context parameter can be passed as null from Java The caller is responsible for passing field values that match their expected type If they do not match Overture throws a dynamic type exception for subsequent evaluations 14 4 Token Values Token values are simply wrappers for normal VDM values reflecting the way they are created in VDM like mk token hello which would be a wrapper for a seq of char There is no Really this ought to have a get method 142 APPENDIX I USING VDM VALUES IN JAVA EB special way of getting a TokenValue from a Value other than casting it Having casted the Value the wrapped value can be obtained from the public final Value field called value Constructing a TokenValue is just a matter of
74. erited by name Trace repeat illegal values Cannot inherit from system class name Cannot instantiate system class name Argument to deploy must be an object Arguments to duration must be nat Arguments to cycles must be nat System class constructor cannot be implicit System class can only define instance variables and a constructor System class can only define a default constructor 116 APPENDIX E TYPE ERRORS AND WARNINGS 3286 3287 3288 3289 3290 3291 3292 3293 3294 3295 3296 3297 3298 3299 3300 3301 3302 3303 3304 3305 3306 3307 3308 3309 3310 Constructor cannot be async Periodic sporadic thread must have n argument s Argument to setPriority must be an operation Argument to setPriority cannot be a constructor Constructor is not accessible Asynchronous operation name cannot return a value Only one system class permitted Argument to reverse is not a sequence Cannot use typename outside system class Cannot use default constructor for this class Cannot inherit from CPU Cannot inherit from BUS Operation type cannot be called from a function Variable name in scope is not updatable Variable name cannot be accessed from this context Measure parameters different to function Recursive function cannot be its own measure CPU frequency to s
75. erture Overture Examples You can then select which VDM dialect you wish to import examples for Finally a selection screen with all examples will be showrl Simply pick the ones you wish to import See Figure 4 1 for more details EI Import Projects Import ess Select a directory to search for existing Eclipse projects Select N E m 149 lect root direc Select Dialect tie 7 gt ES Projects Select dialect V ACSSL ACSSL 2 Select an EV 7 ADTSL ADTSL VDM PP AlarmErrSL AlarmErrSU Deselect Al AlarmSL AlarmSL Overture Examples VDM RT Bi ATES AES Refresh Run Debug Team Opti cts O Ge ms a 2 Next gt Cancel Working sets 4 Add project to working sets Figure 4 1 Import VDM Examples Note that any previously imported examples will be greyed out 13 E Overture VDM 10 Tool Support User Guide 4 2 Creating a New Overture Project Follow these steps to create a new Overture project Create a new project by choosing File New Project Overture 2 Select the VDM dialect you wish to use VDM SL VDM PP or VDM RT 3 Click Next 4 Type in a project name 5 Choose whether you would like the contents of the new project to be in your workspace or outside browse to the appropriate directory 6 The next step enables references to other projects but this is not used at the moment 7
76. erture workspace AlarmPP generated java src AlarmPP quotes finished Java code generation generated 4 classes Figure 11 2 The status of code generating the AlarmPP example type filter text Java Code Generation M Y General Help F Disable cloning Install Update V Generate character sequences as strings Run Debug Generate concurrency mechanisms VDM only E Generate JML Java Modeling Language annotations VDM SL only m Team 4 VDM Combinatorial Testi Debugger Dot Editor Les Classes modules that should not be code generated Separate by e g World Env Output package of the generated Java code e g my pack Java Code Generatio Latex COEK ADM Tonle Restore Defaults Apply o Figure 11 3 Configuration of the Java code generator as an argument or returned as a result However Java does not support composite value types like structs and records and as a consequence record types must be represented using classes which use reference semantics This means that an object reference which is used to represent a com posite value type in the generated Java code must be deep copied when it appears in the right hand side of an assignment it is passed as an argument or returned as a result For arbitrarily complex value types such as records composed of record or sets of composed of sets deep copying may introduce a significant overhead in the generated code If t
77. es UML transformation up 76 VDM dialect vdm file extension view welcome screen 5 workbench XMI 145
78. et dom schedule 15 ADT a o stl nat hedul p Period to set of Expert BP Aat 53 public ExpertIsOnDuty Expert gt set of Period T idee doa i pas et of Eg E AlarmPP 54 ExpertisOnDuty ex a m s of Alarm map Period to set of amp generated 955 return p p in set dom schedule amp A Penod toker alarm vdmpp 5 ex in set schedule p ExpertToPage Alarm Period Expert ES expertvdmpp NumberOfExperts Period nat ES plantvdmpp 58 public Plant set of Alarm ExpertisOnDuty Expert set of Period E README bt 59 map Period to set of Expert Plant Plant set of Alarm map Period to set of Expert estl vdmpp 60 Plant als seu 1 AlarmSL m VDM Model files 9 Error Log HE 3 Srvorreuick Interpreter 3 errors 606 warnings 0 others Filter matched 103 of 609 items Description a Location Type O Errors 3 items Problem view amp Warnings 100 of 606 items f Writable Insert 52 1 CENE Figure 3 1 The VDM Perspective Dra a Select a wizard gt Wizards type filter text E VOM PP Project E VOM RT Project Es VDM SL Project gt General Overture Back Next gt Finish Cancel Figure 3 2 Creating a New VDM Project Figure 3 3 illustrates the different outline icons At the top of the view there are buttons to filter what is displayed for instance it is possible to hide non public members Clicki
79. ete REA A 5 Editing VDM Models 5 1 VDM Dialect Editors 5 2 Using Templates 5 sis ss 6 2 AA TRE d Rok d 6 Interpretation and Debugging in Overture 6 1 Run and Debug Launch Configurations ee ere oP ae Be eie A OA AOA d 6 2 1 The Debug View a eek era XU eU AAA O loud 45d q e qs eS hse d ud IS a Crece AA E E Ne SD a S 7 Collecting Test Coverage Information 13 13 14 14 15 16 21 21 21 23 23 26 21 27 28 28 28 31 Overture VDM 10 Tool Support User Guide 8 Pretty Printing to DTEX 33 10 Combinatorial Testing 37 10 1 Using the Combinatorial Testing GUI 37 11 Automatic Generation of Code 39 11 1 Use of the Java Code Generator 4s o mo EE AAA 39 UU de WERE Ge ne Ge A e a 40 11 2 1 Disable cloning cs ess caspa edad a ee ee eRe Gas 40 dpe Buty bane bee ban 42 Toc Ge E Ge oe Se a ae ae 42 cT 42 Cv 42 TROMPE 43 11 3 Limitations of the Java Code Generator 43 11 4 The Code Generation Runtime Library 43 45 47 14 Analysing Logs from VDM RT Executions 49 15 Expanding VDM Models Scope and Functionality by Linking Java and VDM 53 rsen 53 AAA au Seay GE OV d 54 sheen een ener 55 Eno Seo Gee SA 55 LEX had RT Ded Og alot 56 ERE ARA IAN ee ee 56 15 3 2 External Java Library 4 ace cs ra RS RR S RES 57 15 3 8 Remote Control
80. ethod The method returns a string with the result A more advanced valueExecute method is also available which returns the internal Value type of the interpreter which is useful for more com plex results The values exchanged between the Overture IDE and the controller are the internal Values used in Overture Documentation about these can be found in the Overture Design Specifi cation Battle10 import org overture interpreter debug RemoteControl import org overture interpreter debug RemoteInterpreter public class RemoteController implements RemoteControl public void run RemoteInterpreter interpreter throws Exception System out println Remote controller run System out println The answer is interpreter execute 1 1 System out println The answer is interpreter execute new A op 123 System out println The answer is interpreter execute new A op 1 3 Listing 15 3 Remote Controller Java class 55 E Overture VDM 10 Tool Support User Guide 15 3 Using a GUI in a VDM model Linking Example This example describes how the linking functionality can be used to create a graphical representa tion of a VDM model 15 3 1 The Modelled System A GUI has been developed in Java Swing which will be used to both control and present the system which is described in the VDM model In this example both the External Java Library technique as well
81. f a project as seen in Figure 4 5 The project settings allow you to define a main TEX file for the project and define the order in which the different VDM source files shall be included Note that if the Insert coverage tables and Mark coverage options are selected the TEX pretty printing will include test coverage information as well as provide test coverage tables for each class module in the VDM model It is also possible to define your own main doc ument instead of making use of the standard one suggested by Overture which is the name of the project followed by tex Finally the Model only option is used to select if you wish to include only the VDM model or also the text that can be written outside begin vdm_al and Nend vdm al environments see Chapter 8 for more details It is also possible to set various preferences that apply to all projects This is done in the general VDM preferences dialog under Window Preferences VDM Here for example it is possible to link projects to VDM Tools if you have the appropriate SCSK VDMTools executables installed on the computer Figure 4 6 shows how it is possible to set up paths to the corresponding VDMr Tools executables If these paths have been set it is possible to right click on a project in the VDM Explorer view and select VDM Tools Open project in VDMTools Then a project file for VDMTools will automatically be generated with all the files from the Overture pro
82. f a runtime exception is encountered during the execution of a test control will enter the debugger With runt race runtime exceptions are recorded as the result of a failed test rather than trapping into the debugger filter Sage reduction type This command reduces the size of expanded CT traces to a given percentage eg 10 There are various options for making the actual selection of tests to remove RANDOM SHAPES NOVARS SHAPES VARNAMES or SHAPES VARVALUES the names are not case sensitive assert file This command runs assertions from the file provided The assertions in the file must be Boolean expressions one per line The command evaluates every assertion in the file raising an error for any which is false init This command re initializes the global environment Thus all state components will be initialised to their initial value again created variables are lost and code coverage information is reset env This command lists the value of all global symbols in the default environment This will show the signatures for all functions and operations as well as the values assigned to iden tifiers from value definitions and global state definitions in VDM terminology public static instance variables Note that this includes invariant initialization and pre postcon dition functions In the VDM and VDM RT dialects the identifiers created using the create command will also be included
83. f values into character sequences as provided by the VDMUt il and finally functionality to write to the console as available in the TO library Chapter 12 Mapping VDM To and From UML VDM and VDM RT projects can be converted automatically back and forth between VDM and the corresponding UML model Essentially VDM and UML can be considered as different views of the same model A UML model is typically used to give a graphical overview of the model using class diagrams The VDM model is typically used to define the implementation and constraints for each class and is therefore used for detailed semantic analysis Note that state charts activity diagrams sequence diagrams objects charts package charts are not used in the UML mapping It is essentially only the information used statically inside classes and their usage in class diagrams that is used To convert a UML class diagram model to a VDM model you first need to export the UML model from Modelio to the Eclipse XMI format called UML using the EMF UML3 0 0 format At the moment Modelio is the only UML tool supported Export from Modelio is done as illustrated in Figure 2 Model 3 al o Operation E e 2 Raised Exception ud ES Alarminityiiar E Plant IM Create a diagram Q XM Export E a B Alam Create an element E pel XMI Export IB Alar f Add stereotype J Close project C Users pgl modelio workspace Alarm XMI AlarminitUML uml of Cut
84. g like the one shown in Figure 6 2 5 The Expressions View The Expressions view allows you to define expressions that are evaluated whenever the debugger stops Watched expressions can be added to the view directly or created by selecting Watch when right clicking a variable in the Variables view It is also possible to edit existing expressions The view sits in the same panel as the Breakpoints view and the Variables view 5Note that breakpoints can only be set on lines that contain executable code Note this is not possible from the Breakpoint view 28 CHAPTER 6 INTERPRETATION AND DEBUGGING IN OVERTURE Breakpoint properties Line Breakpoint Filename flarecontroller vdmrt Line 45 Y Enable TJ Hit Counter Y Enable Condition evid 4 E Suspend when condition is true 9 value of condition changes Figure 6 6 Conditional breakpoint options 29 Overture VDM 10 Tool Support User Guide 30 Chapter 7 Collecting Test Coverage Information When a VDM model is being interpreted it is possible to automatically collect test coverage in formation Test coverage measurements help you to see how well a given test suite exercises your VDM model In order to enable the collection of test coverage data go to the debug launch configuration and select the Generate coverage option After running this configuration a new file
85. gt is not in scope Cannot use history of a constructor If expression is not a boolean 109 Overture VDM 10 Tool Support User Guide 3109 3110 3111 3112 3113 3114 3115 3116 3117 3118 3119 3120 3121 3122 3123 3124 3125 3126 3127 3128 3129 3130 3131 3132 3133 Argument to inds is not a sequence ra 1 Argument of in set is not a set Argument to inverse is not a map Iota set bind is not a set Unknown type name lt name gt Undefined base class type lt class gt Undefined class type lt class gt Argument to len is not a sequence Such that clause is not boolean Predicate is not boolean Map composition is not a maplet Argument to dom is not a map Element is not of maplet type Argument to rng is not a map Left hand of munion is not a map Right hand of munion is not a map Argument of mk type is the wrong type Unknown type type in constructor Type type is not a record type Record and constructor do not have same number of fields Constructor field n is of wrong type Modifier for tag should be type Modifier tag not found in record mu operation on non record type Class name name not in scope 110 APPENDIX E TYPE ERRORS AND WARNINGS EB 3134 Class has no constructor with these parameter types 3135 Class has no constructor with these para
86. h easier for users to create models even if they are not deeply familiar with the VDM syntax It is possible to adjust or add to the templates defined in Overture This can be done in the general VDM preferences under Window Preferences VDM gt Templates Figure 5 2 shows where to adjust templates in Overture Note that new templates can be added and the existing ones can be edited or removed A full list of the standard Overture templates is available in Appendix A 21 Overture VDM 10 Tool Support User Guide 30 functions NumberOfExperts NumberOfExperts peri plant Period Plant gt nat 34 card plant schedule peri 5 pre peri in set dom plant schedule 36 37 ExpertIsOnDuty Expert Plant gt set of Period 38 ExpertIsOnDuty ex mk Plant sch 39 peri peri in set dom sch amp ex in set sch peri 40 41 ExpertToPage a Alarm peri Period plant Plant r Expert 2 pre peri in set dom plant schedule and 43 a in set plant alarms 44 post r in set plant schedule peri and 45 a quali in set r quali 47 QualificationOK set of Expert Qualification gt bool 48 QualificationOK exs reqquali 49 exists ex in set exs amp reqquali in set ex quali 50 51 functionk parameterTypes gt resultType 52 functionName parameterNames expression 53 pre preCondition 54 post postCondition 55 Figure 5 1 Explicit function template Mg Preferences w type filter te
87. he specification subject to code gener ation does not truly rely on value semantics the user may wish to disable deep copying of value 41 e Overture VDM 10 Tool Support User Guide types in the generated code in order to remove this overhead The user should however be aware that disabling of cloning may lead to code being generated that does not preserve the semantics of the input specification and in general disabling of cloning is discouraged By default cloning is enabled 11 2 2 Generate character sequences as strings In VDM a string is a sequence of characters and there is no notion of a string type Java in particular works differently since it uses a separate type to represent a string The default behaviour of the Java code generator is to code generate sequences of characters as strings and subsequently do the necessary conversion between between strings and sequences in the generated code Another possibility is to treat a string literal for what it truly is namely a sequence of characters and thereby avoid any conversion between strings and sequences In order to do that i e not generating character sequences as strings the corresponding option must be unchecked 11 2 3 Generate concurrency mechanisms If the user does not rely on the concurrency mechanisms of VDM and does not want to include support for them in the generated code the corresponding option in the preference page must be unchecked By default the behaviou
88. ing arrow at the top right most corner of the view See Figure The Filters option allows various files or directories to be hidden including directories that have no source files 3 2 4 Including line numbers in the Editor If line numbers are required in the dialect editors right click in the left hand margin of the editor and select show line numbers as shown in Figure B 6 Note that the current line number and cursor position are displayed in the eclipse status bar at the bottom of the workspace when an editor has focus 10 CHAPTER 3 USING THE VDM PERSPECTIVE Top Level Elements Select Working Set Deselect Working Set Edit Active Working Set 531 Window Working Set Package Presentation E Link With Editor Figure 3 5 Filtering Directories without source files Toggle Breakpoint Enable Disable breakpoint wv Show Quick Diff Ctri Shift 0 w Show Line Numbers Preferences Breakpoint properties Figure 3 6 Adding Line Numbers in Editor 11 Overture VDM 10 Tool Support User Guide 12 Chapter 4 Managing Overture Projects 4 1 Importing Overture Projects It is possible to import Overture projects by right clicking in the Explorer view and selecting Import followed by General Existing Projects into Workspace It is possible to automatically import a large collection of existing examples To do this right click the Explorer view and select Import Ov
89. ion fin functionExplicit functionImplicit instancevariables isnotyetspecified isofbaseclass Is subclass responsibility Mutex operation Explicit Operation Implicit operation Permission predicate for an operation history coun ters can be used fin act active req waiting The number of requests that has been issued for the operation name operation Test if two objects are of the same type Get a reference to the current object Synchronization block Values block The number of outstanding requests for the operation name operation The number of times that operation name operation has been activated The number of operation name operations that are currently active BUS Priority lt CSMACD gt capacity set of con nected CPUs Class Definition Class Definition full skeleton CPU Priority lt FP FCFS gt capacity Cycles number of cycles statement Duration time in nanoseconds statement The number of times that the operation name opera tion has been completed Explicit function Implicit function Instance Variables block is not yet specified Test if an object is of a specific base class 84 APPENDIX A TEMPLATES IN OVERTURE Key Description isofclass Test if an object is of class issubclassof Is subclass of issubclassresponsibility mutex operationExplicit operationImplicit per periodic req samebaseclass self sync system time values waiting Is subc
90. is described in Section 15 1 and 2 the method used to allow a Java implementation to Remote Control a VDM model is explained in Section 15 2 An example of how these methods can be used to create a GUI for a model is supplied in Section 15 3 These methods are also used to enable control of models with a generic GUI as explained in 15 1 Defining Your Own Java Libraries to be used from Over ture VDM models are not appropriate for describing everything It is common to have existing legacy code that you may not wish to spend time modelling in VDM but would like to make use of from a VDM model Overture has a feature to link a VDM model with external Java libraries contained in astandard jar file Using this feature it is possible to call functionality provided by jar files from a VDM model This functionality corresponds to DL modules classes in VDMTools DLMan External jar libraries are linked to VDM via is not yet specified statements and expressions Operations or functions of modules or classes can be delegated to an external jar calling out to a Java class The Java delegate if present has the same name as the VDM module class name ln fact the TO MATH Util CSV and VDM Unit libraries are implemented as such external jar files 53 E Overture VDM 10 Tool Support User Guide 66 with underscores replaced with package naming dots For example the VDM class remote lib sensor becomes the class remo
91. itions st after be in let statement rin after bind in let statement cases ri after cases expression gt after case pattern list gt after others end after cases der in after equals definitions 100 APPENDIX D SYNTAX ERRORS 2241 2242 2243 2244 2245 2246 2247 2248 2249 2250 2251 2252 2253 2254 2255 2256 2257 2258 2259 2260 2261 2262 2263 2264 2265 Expecting Expecting after specification statement Expecting start Expecting start Expecting after start object Expecting startlist Expecting startlist Expecting after startlist objects Missing of in compose type Missing end in compose type Expecting to in map type Expecting to in inmap type Expecting of after set Expecting of after seq Expecting of after seql Bracket mismatch Missing close bracket after optional type Expecting gt in explicit operation type Operations cannot have QT type parameters Module starts with class instead of module Missing comma between return types Can t have traces in VDM SL Missing after named trace definition Expecting after trace name Expecting nl n2 after trace definition 101 Overture VDM 10 Tool Support User Guide 2266 2267 2268 2269 2270 2271 2272 2273 2274 2275 2276 2277 2
92. itors Proceedings of the Second VDM Workshop September 2000 Available at www vdmportal org Nunes Carlos and Paiva Ana Automatic Generation of Graphical User Inter faces From VDM Specifications In ICSEA 2011 The Sixth International Conference on Software Engineering Advances pages 399 404 2011 S S Patil Limitations and Capabilities of Dijkstra s Semaphore Primitives for Coordination among Processes Cambridge Mass MIT Project MAC Computation Structures Group Memo 57 February 1971 80 CHAPTER 16 ACOMMAND LINE INTERFACE TO OVERTURE E Ribeiro amp 11 Augusto Ribeiro and Kenneth Lausdahl and Peter Gorm Larsen Run Time Validation of Timing Constraints for VDM RT Models In Sune Wolff and John Fitzgerald editors Proceedings of the 9th Overture Workshop pages 4 16 June 2011 Verhoef amp 06 Marcel Verhoef and Peter Gorm Larsen and Jozef Hooman Modeling and Validating Distributed Embedded Real Time Systems with VDM In Jayadev Misra and Tobias Nipkow and Emil Sekerinski editors FM 2006 Formal Methods pages 147 162 Springer Verlag 2006 81 Overture VDM 10 Tool Support User Guide 82 Appendix A Templates in Overture Overture defines a number of standard Eclipse templates You can add your own as well The keys and descriptions of the pre defined templates are Key Description caseExpression Case Expression dclStatement Declare defExpression def pattern expressi
93. ject and VDMTools will be opened The Preferences dialog also allows you to switch off continuous syntax checking while editing and to set the path to pdflatex if this 1s not automatically visible from the Overture application 2This does not work for VDM RT models since that dialect is no longer supported by VDMTools 17 E Overture VDM 10 Tool Support User Guide gt Resource Builders Project References Latex options Main document Smoking tex Run Debug Settings Generate main document VDM Build Path Insert coverage tables Mark coverage 4 VDM Settings Y Model only Latex o Figure 4 5 Overture Project Settings for IEX It is also possible to set a few other areas debugger and dot but these are mostly used by the developers Finally it is possible to manage VDM templates but that is described in Section 5 2 type filter text SCSK VDM Tools gt General gt Help Path to VDM Tools for VDM SL vdmgde C Program Files The VDM SL Toolbox v9 0 2 bin vdmgde exe a Path to VDM Tools for VDM PP vppgde C Program Files The VDM Toolbox v9 0 2 bin vppgde exe gt Run Debug gt Team 4 VDM Combinatorial Testing UML Translation Figure 4 6 Overture Preferences for connections to VDM Tools In the same fashion it is possible to set preferences for the way VDM and VDM RT models are mapped to UML This can be seen in Figure More information about these prefe
94. jects To de clutter the workspace and reduce the risk of accidental changes it may be helpful to close projects that are not used being worked on This can be done by right clicking such projects and then selecting the Close Project entry in the menu Projects can similarly be re opened using the same menu E Overture VDM 10 Tool Support User Guide 3 2 2 Adding Additional VDM File Extensions It is possible to associate additional or different filename extensions with a particular VDM dialect editor instead of the standard vdms1 vdmpp and vdmrt This is done using the Window Preferences menu Click the Add button for the appropriate content type oix cont Content Types oe X General STR dep h Fl See File Associations for associating editors with file types Content Types Java Content types E Appearance Text Type Filters JAR Manifest File E Code Style Java Properties File Formatter Java Source File E Editor Refactoring History File E Content Assist Refactoring History Index Advanced Runtime log files Favorites VDM PP Content type E Run Debug VDM RT Content type zi Launching File associations E Team File Content vdmpp locked Default encoding Update o cms Figure 3 4 Adding Additional Contents Types 3 2 3 Filtering Project Contents It is possible to filter out certain file types from the VDM Explorer view This is done by clicking the small downward point
95. l from module with no exports No export declared for import of type lt type gt from lt module gt Type import of lt name gt does not match export from lt module gt No export declared for import of value lt name gt from lt module gt Type of value import lt name gt does not match export from lt module gt Cannot import from self No such module as lt module gt Expression matching set bind is not a set Type bind not compatible with expression Set bind not compatible with expression Mk expression is not a record type Matching expression is not a compatible record type Record pattern argument field count mismatch Sequence pattern is matched against type Set pattern is not matched against set type Matching expression is not a product of cardinality n Matching expression is not a set type Object designator is not an object type Object designator is not an object type 113 Overture VDM 10 Tool Support User Guide 3209 3210 3211 3212 3213 3214 3215 3216 3217 3218 3219 3220 3221 3222 3223 3224 3225 3226 3228 3229 3230 3231 3232 3233 3234 Member lt field gt is not in scope Object member is neither a function nor an operation Expecting lt n gt arguments Unexpected type for argument lt n gt Operation lt name gt is not in scope Cannot call lt name gt from static context lt name gt is not an ope
96. lass 3013 Class invariant is not a boolean expression 3014 Expression is not compatible with type bind 105 Overture VDM 10 Tool Support User Guide 3015 Set 3016 Expression is not compatible with set bind bind is not a set type 3017 Duplicate definitions for lt name gt 3018 Function returns unexpected type 3019 Function parameter visibility less than function definition This error message typically are caused by using a more restrictive access modifier or none which is interpreted as private at this place compared to for example an inherited definition 3020 Too 3021 Too 3022 Too 3023 Too 3024 Too many parameter patterns few parameter patterns many curried parameters many parameter patterns few parameter patterns 3025 Constructor operation must have return type lt class gt 3026 Constructor operation must have return type lt class gt 3027 Operation returns unexpected type 3028 Operation parameter visibility less than operation definition This error message typically are caused by using a more restrictive access modifier or none which is interpreted as private at this place compared to for example an inherited definition 3029 Function returns unexpected type 3030 Function parameter visibility less than function definition This error message typically are caused by using a more restrictive access modifier or non
97. lass responsibility Mutex operation Explicit Operation Implicit operation Permission predicate for an operation history coun ters can be used fin act active req waiting periodic periode jitter delay offset operation name The number of requests that has been issued for the operation name operation Test if two objects are of the same type Get a reference to the current object Synchronization block System skeleton Get the current time Values block The number of outstanding requests for the operation name operation 85 Overture VDM 10 Tool Support User Guide 86 Appendix B Internal Errors This appendix gives a list of the internal errors in Overture and the circumstances under which each internal error can be expected Most of these errors should never be seen so if they appear please report the occurrence via the Overture bug reporting utility https github com overturetool overture issues new 0000 0001 0002 0003 0004 0005 0006 0007 0009 0010 0011 0052 0053 File IO errors eg File not found This typically occurs if a specifica tion file is no longer present Mark reset not supported use push pop Cannot change type qualifier lt name gt lt qualifiers gt to lt qualifiers gt PatternBind passed class name Cannot get bind values for type type Y Illegal clone Constructor for lt class gt can t fin
98. le 6 ualifier end Target class end VDM construct Q E isUnique isUnique map false true inmap true true Table H 3 Transformation rules for VDM constructs mod eling relationships between two sets Transformation Rule 11 A VDM class with a thread compartment is mapped as the UML meta class Class with the meta attribute isActive setto true Transformation Rule 12 A VDM class with the keyword is subclass of fol lowed by class names is mapped as the UML meta class Generalization with the attributes general and specific referencing the superclass and subclass re spectively More than one subclass results in more than one instance of Generalization Transformation Rule 13 A VDM class with the keyword is subclass responsibility as a function or operation body is mapped as the UML meta class Class with the meta attribute isAbstract set to true Transformation Rule 14 A VDM generic class maps to the UML meta class Class with the attribute templateSignature referencing a set of TemplateParameter having the name property set to the name of the parameter 135 Overture VDM 10 Tool Support User Guide Transformation Rule 15 A VDM operation and function are mapped to the UML meta class Operation where the property isQuery de termine whether the Operation represents a VDM func tion or operation true e for a function false e for a operation The retu
99. lication in many cases has been used by practitioners who were not specialists in the underlying formalism or logic Larsen amp 96 Clement amp 99 Kurita amp 09 Experience with the method suggests that the effort spend on formal modelling and analysis can be recovered in reduced rework costs arising from design errors VDM models can be expressed in a Specification Language VDM SL which supports the de scription of data and functionality ISOVDM96 Fitzgerald amp 98 Fitzgerald amp 09 Data are defined by means of types built using constructors that define structured data and collections such as sets sequences and mappings from basic values such as Booleans and natural numbers These types are very abstract allowing you to add any relevant constraints using data type invariants Functional ity is defined in terms of operations over these data types Operations can be defined implicitly by preconditions and postconditions that characterize their behavior or explicitly by means of spe cific algorithms An extension of VDM SL called VDM supports object oriented structuring of models and permits direct modelling of concurrency Fitzgerald amp 05 A further extension to VDM called VDM Real Time VDM RI includes support for discrete time models jee amp 00 Verhoef amp 06 The VDM RT dialect is also used inside the Crescendo toof supporting collaborative modelling and co simulation Fitzgerald amp 14 All three VDM dialects are supported
100. low speed Hz CPU frequency to fast speed Hz Errs clause is not bool gt bool Cannot mix modules and flat specifications Measure must not be polymorphic Measure must also be polymorphic 117 Overture VDM 10 Tool Support User Guide 3311 3312 3313 3314 3315 3316 3317 3318 3319 3320 3321 3322 3323 3324 3325 3326 3327 3328 3329 3330 3331 3332 3333 3334 3335 Pattern cannot match Void operation returns non void value Operation returns void value Map pattern is not matched against map type Matching expression is not a map type Expecting number in periodic sporadic argument Expression can never match narrow type Measure s type parameters must match function s Tin set expression is always false not in set expression is always true Type component visibility less than type s definition Duplicate patterns bind to different types Overloaded operation cannot mix static and non static Operation name is not static Mismatched compose definitions for type Constructor can only return self Value is not of the right type Statement may return void value Abstract function operation must be public or protected Cannot instantiate abstract class name obj expression is not an object type Object pattern cannot be used from a function Matching expression is not a compatible obj
101. meter types 3136 Left and right of different types 3137 Not expression is not a boolean 3138 Argument of not in set is not a set 3139 Left hand of operator is not numeric 3140 Right hand of operator is not numeric 3141 Right hand of is not a map 3142 Right hand of is not a map 3143 Domain of right hand of must be nati 3144 Left of is neither a map nor a sequence 3145 Argument to power is not a set 3146 Left hand of operator is not a set 3147 Right hand of operator is not a set 3148 Left of is not a map 3149 Right of is not a set 3150 Restriction of map should be set of type 3151 Left of is not a map 3152 Right of is not a set 3153 Restriction of map should be set of type 3154 name not in scope 3155 List comprehension must define one numeric bind variable 3156 Predicate is not boolean 3157 Left hand of is not a sequence 3158 Right hand of is not a sequence 111 Overture VDM 10 Tool Support User Guide 3159 3160 3161 3162 3163 3164 3165 3166 3167 3168 3169 3170 3171 3172 3173 3174 3175 3176 3177 3178 3179 3180 3181 3182 3183 Predicate is not boolean Left hand of is not a set Right hand of is not a set Left and right of are different types
102. minology Eclipse is an open source platform based around a workbench that provides a common look and feel to a large collection of extension products If you are familiar with one Eclipse product you will generally find it easy to start using other products that use the same workbench The Eclipse workbench consists of several panels known as views such as those shown in Figure 3 1 A particular arrangement of views is called a perspective for example Figure 3 1 shows the standard VDM perspective This consists of a set of views for managing Overture projects and viewing and editing files in a project Different perspectives are available in Overture as will be described later but for the moment think of a perspective as a useful composition of views for conducting a particular task The VDM Explorer view lets you create select and delete Overture projects and navigate between the files in these projects as well as adding new files to existing projects A new VDM project is created choosing the File New Project option which results in the dialog shown in Figure Select the desired VDM dialect and press Next Finally the project needs to be given a name Click Finish to create the project Depending upon the dialect of VDM used in a given project a corresponding Overture Editor view will be available to edit the files of your new project Dialect editors are sensitive to the keywords used in each particular dialect and simplify the task of
103. monly needed for debugging in VDM Break points can easily be set in the model by double clicking in the left margin of the Editor view at the chosen line When the debugger reaches the location of a breakpoint and stops you can inspect the values of different identifiers and step through the VDM model line by line The Debug Perspective is illustrated in Figure 6 4 26 CHAPTER 6 INTERPRETATION AND DEBUGGING IN OVERTURE E EEB Debug POP3 messagechannel vdmpp Overture Tools File Edit Navigate Search Project Run Window Help 0 Q AP rr 3 Debug _ _ ki Variables 2 Breakpoints E POP3 Testi VOM PP Model Name lt P VOMA all traces in debu 2 p ga 8 Global Variables lain Wi IG 9 Instance Variables gt tThread 6 on vCPU RUNNABLE s a la ject on v 6 name mi innel vdmpp lin ebu o fi PU WAITING on vCPU RUNNABLE C E UN Lo 0 x ES PO Proof Obliga EN Combinatori 55 Debug E3 VOM vel Inspecting variables POP3Types USER paul true 10 66 1 0 E plentvdmpp E testalarmavdmst E alarmavdmst G pop3test vdmpp pop3messagevdmpp messagechannelvdmpp O 3E Outline ER Nox O MessageChannel o data syne per ServerListen gt fin ClientSend 1 jebug t ServerListen Send ClientCommand ServerResponse 15 Listen Che and ServerResponse a e 1 fin ClientListen T nes s o erListen t ma i PEN gt fin ClientSendClient c say
104. must first create a launch configuration To do this go to the main Run menu and select Run Run Configurations Select the type of project you want to launch click the New icon to create a new launch specification of that type and give it a name The launch dialog requires you to identify the VDM project name the class module name and the initial operation function to call in that class module Figure 6 1 shows a launch dialog The standard Eclipse strategy is the launch mode called an Entry point and then you simply click the Browse button and it will let you select a project from those available in the workspace Clicking the Search button will search the chosen project for classes and modules to select a public operation or function from If the chosen operation or function has parameters the types and names of those parameters will be copied into the Operation box these must be replaced with valid argument values However there are other launch mode possibilities here as well The Remote Control launch mode is advanced but it is explained in more detail in Section 15 2 The Console launch mode enables you to get a special debug console where you can enter multiple entry points one after another instead of deciding upon the single entry point at launch time The commands that can be used in the Console view correspond to the commands you can give at command line when it has been started in interpreter mode see Section
105. ng lt object gt name args or name args 93 Overture VDM 10 Tool Support User Guide 2066 2067 2068 2069 2070 2071 2072 2073 2074 2075 2076 2077 2078 2079 2080 2081 2082 2083 2084 2085 2086 2087 2088 2089 2090 Expecting object field name Expecting self new or name in object designator Expecting field identifier Expecting lt identifier gt lt type gt lt expression gt Function type cannot return void type Expecting field identifier before Expecting field name before Duplicate field names in record type Unexpected token in type expression Expecting is subclass of Expecting is subclass of Expecting end after class members Missing after type definition Missing after function definition Missing after state definition Missing after value definition Missing after operation definition Expecting instance variables Missing after instance variable definition Missing after thread definition Missing after sync definition Expecting after pattern in invariant Expecting before type parameter Expecting before type parameter Expecting after type parameters 94 APPENDIX D SYNTAX ERRORS 2091 2092 2093 2094 2095 2096 2097 2098 2099 2100 2101 2102 2103 2104 2105
106. ng on the name of a definition in the outline will navigate to the definition and highlight the name in the Editor view The Problems view at the bottom of Figure 3 I displays information messages about the projects you are working on such as warnings and syntax or type checking errors The VDM Quick Interpreter view has a small command line at the bottom where a plan VDM expression not depending upon the definitions in the VDM model you are working with but for that you can use the Console launch mode explained in Section 6 1 can be entered When return 8 CHAPTER 3 USING THE VDM PERSPECTIVE E B Outline 22 m LR We x 4 O Test H FunPriv nat nat FunPro nat nat O FunPub nat nat o instPriv nat instPro nat instPub nat o instStat nat g OpPriv nat nat OpPro nat nat OpPub nat nat e OpStat nat nat amp per OpStat sync predicate 4 RecordType record type A TypePriv nat TypePro nat TypePub nat o valPriv Test nat f valpro Test nat o valPub Test nat Figure 3 3 Icons in the Outline View is pressed the expression will be evaluated and the result shown above the command line Most of the other features of the workbench such as the menus and toolbars are similar to other Eclipse applications with the exception of a special menu with Overture specific functionality 3 2 Additional Eclipse Features Applicable in Overture 3 2 1 Opening and Closing Pro
107. o and Erik Poll An overview of JML Tools and Applications Intl Journal of Software Tools for Technology Transfer 7 212 232 2005 The VDM Tool Group The VDM SL to C Code Generator Technical Report CSK Systems January 2008 TT E Overture VDM 10 Tool Support User Guide CGManPP The VDM Tool Group The VDM to C Code Generator Technical Report CSK Systems January 2008 Clement amp 99 Tim Clement and Ian Cottam and Peter Froome and Claire Jones The Devel opment of a Commercial Shrink Wrapped Application to Safety Integrity Level 2 the DUST EXPERT Story In Safecomp 99 Springer Verlag Toulouse France September 1999 LNCS 1698 ISBN 3 540 66488 2 DLMan The VDM Tool Group The Dynamic Link Facility Technical Report CSK Systems January 2008 Elmstrom amp 94 Ren Elmstr m and Peter Gorm Larsen and Poul B gh Lassen The IFAD VDM SL Toolbox A Practical Approach to Formal Specifications ACM Sigplan Notices 29 9 77 80 September 1994 4 pages Fitzgerald amp 05 John Fitzgerald and Peter Gorm Larsen and Paul Mukherjee and Nico Plat and Marcel Verhoef Validated Designs for Object oriented Systems Springer New York 2005 Fitzgerald amp 07 John Fitzgerald and Peter Gorm Larsen and Simon Tjell and Marcel Verhoef Validation Support for Distributed Real Time Embedded Systems in VDM Technical Report CS TR 1017 School of Computing Science Newcastle Uni versity April 2007 18 pages
108. odel if they are all met In the long term it will be possible to prove these constraints with a proof component in Overture but this is not yet available POs can be divided into different categories depending upon their nature The full list of categories can be found in Appendix G along with a short description for each of them The proof obligation generator is invoked either on a VDM project and then POs for all the VDM model files will be generated or for one selected VDM file Right click the project or file in the Explorer view and then select Proof Obligations Generate Proof Obligations Overture will change into a special Proof Obligations perspective as shown in Figure 9 1 Once you have gen erated POs for a VDM project for the first time they will automatically be re generated whenever the project is rebuilt as long as you stay in the Proof Obligations perspective Note that in the Proof Obligation Explorer view each proof obligation has three components e A unique number in the list shown e The name of the definition in which the proof obligation is located and e The proof obligation category type 35 E Overture VDM 10 Tool Support User Guide plant vdmpp Ej README txt g Ll Po Proof Obligation Explorer 23 g alarms set of Alarm No PO Name Type schedule map Period to set of Expert 1 Testt plant enumeration map injectivity inv PlantInvCalarms schedule 2 Plant Plantinv set of Alarm map Perio
109. of seq Argument of dinter is not a set of sets Merge argument is not a set of maps dunion argument is not a set of sets Left of is not a set Right of is not a map Restriction of map should be set of type Left of is not a set Right of is not a map 108 APPENDIX E TYPE ERRORS AND WARNINGS 3084 3085 3086 3087 3088 3089 3090 3091 3092 3093 3094 3095 3096 3097 3098 3099 3100 3101 3102 3103 3104 3105 3106 3107 3108 Restriction of map should be set of lt type gt Argument of elems is not a sequence Else clause is not a boolean Left and right of are incompatible types Predicate is not boolean Predicate is not boolean Unknown field name in record type Unknown member member of class class Inaccessible member member of class class Field name applied to non aggregate type Field lt n gt applied to non tuple type Field number does not match tuple size Argument to floor is not numeric Predicate is not boolean Function value is not polymorphic Polymorphic function is not in scope Function has no type parameters Expecting n type parameters Parameter name name not defined Function instantiation does not yield a function Argument to hd is not a sequence lt operation gt is not an explicit operation lt operation
110. on in expression2 exists exists bindList amp predicate forall forall bind list amp predicate forallLoop for identifier expression to expression2 do state ment forallinset forall in set functions Function block ifthen if predicate then expressionl else expression2 let let pattern expression in expression2 operations Operation block while while predicate do statement functionExplicit Explicit function functionImplicit Implicit function module Module moduleSkeleton Module Full skeleton of a module operationExplicit Explicit Operation operationImplicit Implicit operation act The number of times that operation name operation has been activated active The number of operation name operations that are currently active class Class Definition classSkeleton Class Definition full skeleton 83 Overture VDM 10 Tool Support User Guide Key Description fin The number of times that the operation name opera tion has been completed functionExplicit Explicit function functionImplicit Implicit function instancevariables Instance Variables block isnotyetspecified is not yet specified isofbaseclass Test if an object is of a specific base class isofclass Test if an object is of class issubclassof Is subclass of issubclassresponsibility mutex operationExplicit operationImplicit per req samebaseclass self sync values waiting act active bus class classSkeleton cpu cycle durat
111. on the table Once the necessary ingredients are on the table one smoker will grab them and start smoking The architecture of the example is illustrated on Figure 15 2 with a focus on the linking func tionality The diagram shows central classes and relations and it places the different classes into a GUI a Java and a VDM Overture block In the given context the World class represents the entire VDM model In the diagram color highlights are used to distinguish the two linking techniques 56 CHAPTER 15 EXPANDING VDM MODELS SCOPE AND FUNCTIONALITY BY Q LINKING JAVA AND VDM E peo abs A Smoker 1 A Smoker 2 A Smoker 3 ones asa ass amp Smoker 1 A Smoker 2 Q Smoker 3 P Add Tobacco Add Paper Add Match Figure 15 1 GUI of Smokers Example implements the TS ME Run method creates Controller forwards user inputs EE gt invokes entire model instantiated by state change ap Moe Loo implements the VDM class Java VDM Overture External Java Library Remote Control Figure 15 2 Class diagram of the Smokers example architecture 15 3 2 External Java Library To allow the GUI to be a true graphical representation of the model the model itself will be able to update the GUI whenever it needs to by using the External Java Library technique If only the remote controller was used the model would be unabl
112. ontain any parse or type checking errors the interpreter can be started by using the i command line option The interpreter is an interactive command line tool that allows expressions to be evaluated in the context of the specification loaded For example to load and interpret a VDM SL specification from a single file called shmem vdms1 the following options would be used java jar Overture x x x jar vdmsl i shmem vdmsl Parsed 1 module in 0 14 secs No syntax errors Warning 5000 Definition i not used in M shmem vdms1 at line 129 7 Type checked in 0 078 secs No type errors Initialized 1 module in 0 046 secs Interpreter started The interpreter prompt is gt The interactive interpreter commands are as follows abbreviated forms are permitted for some shown in square brackets modules This command lists the loaded module names in a VDM SL specification For a flat VDM SL model the single name DEFAULT is used The default module will be indicated in the list displayed classes This command lists the loaded class names in VDM and VDM RT specifications The default class will be indicated in the list displayed default module class This command sets the default module class name as the prime scope for which the lookup of identifiers appear i e names in the default module do not need to be qualified so you can say print xyz rather than print M xyz create id
113. op termination This kind of proof obligation is a reminder to ensure that a while loop will terminate 131 Overture VDM 10 Tool Support User Guide 132 Appendix H Mapping Rules between VDM VDM RT and UML Models Transformation Rule 1 VDM classes are mapped as the UML meta class Class Transformation Rule 2 The visibility of VDM instance variables values functions and operations are mapped as a subset of the UML enumer ation VisibilityKind comprising public private and protected Transformation Rule 3 VDM static is mapped as the isSt atic property of the UML meta class Class Property or Operation re spectively Transformation Rule 4 Data type definitions are mapped as the UML meta class Class and are referenced and thus nested through the meta attribute nestedClassifier of the owning class Notice that this rule is not specified or implemented Transformation Rule 5 Instance variable and value definitions are mapped as the UML meta class Association if Bla The type is an object reference type or b The type is not a basic data type Fitzgerald amp 05 p64 71 133 Overture VDM 10 Tool Support User Guide Transformation Rule 6 Instance variable and value definitions are mapped as the UML meta class Property if the type is a basic data type p71 Instance variables and values are distinguished by the meta attribute isReadOnly No tice rule T
114. original value illustrated by the fact that two subsequent calls to rand return the same results as the first two did The print command can be used to evaluate any expression The env command lists all the values in the global environment of the default module This shows the functions operations and constant values defined in the module Note that it includes invariant initialization and pre postcondition functions The pog command proof obligation generator generates a list of proof obligations for the specification When the execution of a VDM model is stopped at a breakpoint there are additional commands that can be used These are s tep This command steps forward until the current expression statement is on a new line The command will step into function and operation calls 73 E Overture VDM 10 Tool Support User Guide n ext This command is similar to step except function and operation calls are stepped over o ut This command runs to the return of the current function or operation c ontinue This command resumes execution and continues until the next breakpoint or com pletion of the thread that is being debugged stack This command displays the current stack frame context i e the call stack up This command moves the stack frame context up one frame to allow variables to be seen down This command moves the stack frame context down one frame source This command lists VDM source around the current br
115. ot supported The user will get similar messages and markers for other unsupported VDM constructs To summarise the Java code generator currently does not support code generation of multiple inher itance and neither does it support traces type binds invariant checks and pre and post conditions Furthermore let expressions appearing on the right hand side of an assignment will also be re ported as unsupported The Java code generator also does not support every pattern The patterns that are currently not supported are object map union map union set sequence concatenation and match value 11 4 The Code Generation Runtime Library The generated code relies on a runtime library used to represent some of the types available in VDM tokens tuples etc as well as collections and support for some of the complex operators such as sequence modifications For simplicity every Eclipse project generated by the Java code generator contains the runtime library More specifically there is a copy of the runtime library containing only the binaries 1ib codegen runtime jar as well as a version of the runtime library that has the source code attached lib codegen runtime sources jar The runtime library is imported by every code generated class using the Java import statement import 43 E Overture VDM 10 Tool Support User Guide ri a 3 4 0 Q S 5 9 9o 2 Quick Access
116. p 96 Lucas78 Mukherjee amp 00 Nunes amp 2011 Patil71 Peter Gorm Larsen Ten Years of Historical Development Bootstrapping VDMTools Journal of Universal Computer Science 7 8 692 709 2001 http www jucs org jucs_7 8 ten years of historical Peter Gorm Larsen and John Fitzgerald and Sune Wolff Methods for the Development of Distributed Real Time Embedded Systems using VDM Intl Journal of Software and Informatics 3 2 3 October 2009 Peter Gorm Larsen and Kenneth Lausdahl and Nick Battle The VDM 10 Language Manual Technical Report TR 2010 06 The Overture Open Source Initiative April 2010 Peter Gorm Larsen and Kenneth Lausdahl and Nick Battle and John Fitzger ald and Sune Wolff and Shin Sahara VDM 10 Language Manual Technical Report TR 001 The Overture Initiative www overturetool org April 2013 208 pages Peter Gorm Larsen and Bo Stig Hansen Semantics for Underdetermined Ex pressions Formal Aspects of Computing 8 1 47 66 January 1996 P Lucas On the Formalization of Programming Languages Early History and Main Approaches In The Systematic Development of Compiling Algo rithm INRIA Publ Paris 1978 An historic overview of the VDL and other background for VDM Paul Mukherjee and Fabien Bousquet and J r me Delabre and Stephen Payn ter and Peter Gorm Larsen Exploring Timing Properties Using VDM on an Industrial Application In J C Bicarregui and J S Fitzgerald ed
117. plorer 53 ml fg Alaren a N Go Into ij Copy Ctrl C Paste Ctrl V X Delete Delete Move Rename F2 gig Import r Export 9j Error Loc E Refresh F5 Quick Interpreter Code Genera Close Project Close Unrelated Projects Debug As Run As Team Compare With Restore from Local History Code Generation Generate Java Ctri Alt C i VDMTools Generate Java Launch Configuration Based Ctrl Alt B Overture Developer Utils gt Configuration ME Latex About PO Proof Obligations T UML Transformation Build Path Clone as VDM RT Properties Alt Enter E AlarmPP Figure 11 1 Launching the Java code generator code is available as an Eclipse project in the lt workspace gt lt project gt generated java folder 11 2 Configuration of the Java Code Generator The Java code generator can be configured via a preference page as shown in Figure The preference page can be accessed in the way you would normally access an Eclipse preference page or via the context menu shown above in Figure The Java code generator provides a few options that allows the user to configure the code generation process see Figure 11 3 The sub sections below treat each of these configuration parameters individually in the order they appear in the preference page 11 2 1 Disable cloning In order to respect the value semantics of VDM the Java code generator sometime needs to per form deep copying of objects that represent com
118. posite value types records tuples tokens sets sequences and maps For example in VDM a record is a value type which means that occurrences of the record must be copied when it appears in the right hand side of an assignment it is passed 40 CHAPTER 11 AUTOMATIC GENERATION OF CODE EB EEE E E 9 Error Log EX Problems Tasks amp Console 23 Ql VDM Quick Interpreter Code Generator Console Starting VDM to Java code generation gt No user specified classes to skip Copied the Java code generator runtime library to C Users pvj Downloads Overture workspace AlarmPP generated java lib codegen runtime jar Copied the Java code generator runtime library sources to C Users pvj Downloads Overture workspace AlarmPP generated java lib codegen runtime sources jar Generated Eclipse project with Java generated code Generated class Alarm Java source file C Users pvj Downloads Overture workspace AlarmPP generated java src AlarmPP Alarm java m Generated class Expert Java source file C Users pvj Downloads Overture workspace AlarmPP generated java src AlarmPP Expert java Generated class Plant Java source file C Users pvj Downloads Overture workspace AlarmPP generated java src AlarmPP Plant java Generated class Testi Java source file C Users pvj Downloads Overture workspace AlarmPP generated java src AlarmPP Test1 java Quotes generated to folder C Users pvj Downloads Ov
119. r module in a VDM project A class or module can often be skipped if it acts as an execution entry point or it is used to load input for the specification Classes or modules that the user wants to skip can be specified in the text box in the Java code generator preference page by separating the class module names by a semicolon As an example World Env makes the code generator skip code generation of World and Env while generating code for any other module or class For convenience the output of the Java code generator will also inform the user about what classes or modules are being skipped 11 3 Limitations of the Java Code Generator If the Java code generator encounters a construct that it cannot code generate it will report it as unsupported to the user and the user can then try to rewrite that part of the specification using other supported constructs Reporting of unsupported constructs is done via the console output and us ing editor markers In order to demonstrate this Figure 11 4 shows the console output of the Java code generator when it encounters a type bind which is an example of an unsupported language construct Note the small marker appearing in the editor in order to point out where use of the construct appears For the type bind example in Figure 11 4 the following message is reported Following VDM constructs are not supported by the code generator b bool bool ATypeMultipleBind at 6 14 Reason Type binds are n
120. r of the Java code generator is to not include support for the concurrency mechanisms of VDM in the generated code 11 2 4 Generate Java Modeling Language JML annotations When a VDM model is code generated to Java all the contract based elements of the model i e the pre conditions post conditions and invariants are ignored by default This feature does however provide limited support for translation of the contract based elements of a VDM SL model When the corresponding option is checked the contract based elements are translated to JML annotations which are added on top of the generated Java code as source code comments This al lows the system properties expressed in terms of pre conditions post conditions and invariants to be checked against the generated code Please note that this feature is still experimental and only has limited support for checking of named type invariants 11 2 5 Choose output package The Java code generator allows the output package of the generated code to be specified If the user does not specify a package the code generator outputs the generated Java code to a package with the same name as the VDM project If the name of the project is not a valid java package then the generated code is output to the default Java package 42 CHAPTER 11 AUTOMATIC GENERATION OF CODE EB 11 2 6 Skip classes modules during the code generation process It may not always make sense to code generate every class o
121. ration Expecting lt n gt arguments Unexpected type for argument lt n gt Expression is not boolean For all statement does not contain a set type From type is not numeric To type is not numeric By type is not numeric Expecting sequence type after in If expression is not boolean Such that clause is not boolean Incompatible types in object assignment lt name gt is not in scope lt name gt should have no parameters or return type lt name gt is implicit lt name gt should have no parameters or return type name is not an operation name Precondition is not a boolean expression Postcondition is not a boolean expression 114 APPENDIX E TYPE ERRORS AND WARNINGS 3235 3236 3237 3238 3239 3241 3242 3243 3244 3245 3246 3247 3248 3249 3250 3251 3252 3253 3254 3255 3256 3257 3258 3259 3260 Expression is not a set of object references Class does not define a thread Class does not define a thread Expression is not an object reference or set of object references T Incompatible types in assignment Body of trap statement does not throw exceptions Map element assignment of wrong type Seq element assignment is not numeric Expecting a map or a sequence Field assignment is not of a record type Unknown field name lt name gt Unknown
122. reate manage and run configurations localVdmPpApplicationTabGroupDescription run carlos type filter text 4 ES vomprcu ES CashDispenserPP gt ES vom PP Model E VDM RT GUI VDM RT Model gt E VDM SL Model Gn 7 Name CashDispenserPP 1 GUlBuilder Runtime Debugger Develop 5 Source Common Project Project CashDispenserPP Other Generate coverage Filter matched 73 of 73 items Figure 15 8 VDM GUI Launch configuration 66 CHAPTER 15 EXPANDING VDM MODELS SCOPE AND FUNCTIONALITY BY Q LINKING JAVA AND VDM instance_1_Acco Account 15 tra transaction ValidTransaction cs b Create __ amount date Figure 15 10 Instance viewer showing the Account class 67 Overture VDM 10 Tool Support User Guide 68 Chapter 16 A Command Line Interface to Overture At the centre of the Overture tool there is a Java implementation of VDM forming a core This pro vides a command line interface that may be valuable as it can be used independently of the Eclipse interface of Overture The command line Jar is both bundled with the Overture tool located in the commandline folder and available as a standalone download 16 1 Starting Overture at the Command Line The Overture
123. rences can be found in Chapter 12 18 CHAPTER 4 MANAGING OVERTURE PROJECTS EB type filter text Editor Latex Templates V Prefer associations during translation Y Disable nested artifacts in Deployment Diagrams UML Translation uj Restore Defaults o jJ cms Figure 4 7 Overture Preferences for mapping to UML 19 Overture VDM 10 Tool Support User Guide 20 Chapter 5 Editing VDM Models 5 1 VDM Dialect Editors VDM model files are always ment to be changed in the dialect Editor view Syntax checking is carried out continuously as source files are changed even before the files are saved Whenever files are saved assuming there are no syntax errors a full type check of the entire VDM model is performed Problems and warnings will be listed in the Problems view as well as being highlighted directly in the Editor view where the problems have been identified 5 2 Using Templates Eclipse templates can be particularly useful when you are new to writing VDM models If you press CTRL space after typing the first few characters of a template name Overture will offer a proposal For example if you type fun followed by CTRL space the IDE will propose the use of an implicit or explicit function template as shown in Figure 5 1 The IDE includes several templates cases quantifications functions explicit implicit operations explicit implicit and many more The use of templates makes it muc
124. representation through the model object this is the model in the MVC pattern and not a representation of the VDM model It should be noted that the names of the package and class can be directly related to VDM interface i e gui and Graphics Furthermore the imports should be noted firstly the class must be marked as Serializable secondly multiple packages from the Overture interpreter are imported as well These are needed for the conversion between VDM values and Java values as it can be seen in the nowSmoking method in Listing 15 5 Please be aware that it is extremely important that there are no unused imports in the Java implementation as this will result in an error when the Java library is loaded by Overture 58 CHAPTER 15 EXPANDING VDM MODELS SCOPE AND FUNCTIONALITY BY Q LINKING JAVA AND VDM package gui import java io Serializable import org overture interpreter runtime ValueException import org overture interpreter values Value import org overture interpreter values VoidValue public class Graphics implements Serializable Controller ctrl Model model public Value init ctrl new Controller init the Controller of the MVC pattern model ctrl getModel return new VoidValue public Value tobaccoAdded model tobaccoAdded return new VoidValue public Value nowSmoking Value smokeid throws ValueException model nowSmoking smokeid
125. reter values Value The Value class itself is abstract but subclasses can be instantiated to represent any VDM value such as a seq of char nat1 or a value of an arbitrarily complex type The hierarchy is shown in Figure Generally the name of the Value subclass for a VDM type is on the form name Value for example BooleanValue or SeqValue The following sections describe how to obtain Java values from a Value object and how to create Value objects from basic Java values or iteratively from other values L2 Primitive Values Most primitive VDM types have subclasses with simple constructors that take a Java primitive type as an argument public BooleanValue boolean value public CharacterValue char value 137 Overture VDM 10 Tool Support User Guide public public public public public public public RealValue double value throws Exception RationalValue double value throws Exception Natural IntegerVal Val lue long value ue long value throws Exception NaturalOneValue long value throws Exception QuoteValue String value NilValue The constructors that throw exceptions are the ones for which some Java value does not match the VDM type concerned For example aRealValue or RationalValue cannot take the Java values Double NaN or Double POSITIVE INFINITY as aconstructor argument Similarly NaturalValue and NaturalOneValue cannot take a negative long as an
126. revious time index using the MovePrevious button Finally it is also possible to export all the generated views to JPEG formatted files using the amp button All the generated images will be placed in the logfile directory where each image holds a name indicating the time of execution and the specific view Execution overview CPU1 CPU2 etc The RealTime Log Viewer also provides an overview of all executions on a single CPU Each CPU shows a detailed description of all operations and functions invoked on the particular CPU as 49 E Overture VDM 10 Tool Support User Guide VDM RT Realtime Log Viewer 23 im Architecture overview Execution overview vCpu cruz cruz crua CPUS CPU2 CPUI gy E EEO EE Pee vBus BUST 4 278 Figure 14 2 Execution overview well as the scheduling of concurrent processes see Figure 4 VDM RT Realtime Log Viewer 23 Architecture overview Execution overview vCpu CPU cpu2 cpus BUSI MMI 1 I gt P a 4546043 fa dido resta nat des T C 95459966 lis 100085249 fi aterert nat I 118187876 HA lt IR ta 1 Figure 14 3 Execution on a single CPU Analyzing timing properties at the system level The work of presents an extension to VDM RT enabling the validation of system level timing properties Validation conjectures are descriptions of temporal relations between sys tem level events which can be evaluate
127. rn type of a function and operation is mapped col lectively as the property type and the multiplicity pf the Operation meta class The parameters of the operation or function is mapped to the UML meta class Parameter represented as the property ownedParameters of the Operation meta class The name and type of a VDM parameter are mapped to the property name type and the multiplicity of the Parameter meta class 136 Appendix I Using VDM Values in Java As described in Chapter 15 integration between Overture and Java code can be established either by writing native libraries in Java that can be called from VDM or by giving a Java program overall control of a VDM model by making calls to that model as a user interacts with a GUI In both cases internal VDM values have to be handled by Java either because they are passed as arguments to a Java library and returned as results to VDM or because they are returned from a VDM model evalution to a controlling Java program This appendix describes the internal class hierarchy used by Overture to represent internal VDM model values and describes how a Java program can convert these to Java values int long String etc as well as creating internal values for returning to the VDM model e g as the return value of library methods L1 The Value Class Hierarchy All internal VDM values in Overture are held by instances of the Value class with the fully qualified name org overture interp
128. s gt mk_POP3Types USER paul Debug console Figure 6 4 Debugging perspective 6 2 1 The Debug View The Debug view is located in the upper left corner in the Debug perspective see Figure 6 4 The view shows all running models and whether a given model is stopped suspended or running It shows the call stack of models that are suspended and for VDM and VDM RT stacks for all threads are shown At the top of the view there are buttons for debugging such as stop step into step over resume etc see Table 6 1 Note that in case a multi threaded VDM model is debugged it is possible in this view to change to another thread to inspect where it is currently and inspect the local variables at that thread since they are all stopped when a breakpoint is reached 6 2 2 The Variables View The Variables view shows all the variables in a thread context allowing them to be examined after a breakpoint or an error has been reached The variables and their values are automatically updated when stepping through a model The view is located in the upper right hand corner in the Debug perspective It is possible to inspect compound variables expand nested structures and so on Note that when you stop at a permission predicate it is also possible to see the value of the relevant history counters in Figure 6 4 fin ClientSend and fin ServerListen By right clicking on a variable it is possible to select a watch point As a result a win
129. s a reference for anybody wishing to make use of the tool with one of the VDM dialects VDM SL VDM or VDM RT The different dialects are controlled by a VDM language Board that evaluates possible Requests for Modifica tions Overture tool support is built on top of the Eclipse platform The objective of the Overture initiative is to create and support an open source platform that can be used for both experimenta tion with new VDM dialects as well as new features for analysing VDM models in different ways The tool is entirely open source so anybody can join the development team and influence future developments The goal is to ensure that stable versions of the tool suite can be used for large scale industrial applications of VDM technology Chapter 1 Introduction The Vienna Development Method VDM is one of the longest established model oriented formal methods for the development of computer based systems and software Bjgrner amp 78a Fitzgerald808a It consists of a group of mathematically well founded languages for express ing system models during early design stages before expensive implementation commitments are made The construction and analysis of a model using VDM helps to identify areas of incomplete ness or ambiguity in informal system specifications and provides some level of confidence that a valid implementation will have key properties especially those of safety or security VDM has a strong record of industrial app
130. s associations between the classes in a class diagram Otherwise these will be modelled as attributes Disable nested artifacts in Deployment Diagrams If this option is chosen ticked nested arti facts in a deployment diagram are disabled otherwise it is enabled 46 Chapter 13 Moving from VDM to VDM RT The methodology for the development of distributed real time embedded systems in VDM defines a step where you move from an initial VDM model to a VDM RT model Larsen amp 09 This step is supported by the Overture tool which will convert a VDM project to create the starting point for a new VDM RT project This is done by right clicking on the VDM project to be converted in the Explorer view followed by the Clone as VDM RT option A new VDM RT project is then automatically created and it will initially be given the same name as the one generated from with postfix with VDM RT It will have the same name as the original VDM project but with VDM RT appended Inside the project all the vdmpp files will have been converted to a vdmrt extension The original VDM project is not changed at all So this is simply a quick and easy way to get to the starting point for a VDM RT model You would then manually create a system class with appropriate declarations of CPUs and BUSses and proceed with the real time model development Also keep in mind that you may have some errors if your VDM model uses VDM RT keywords as names 47
131. shut down of the remote interpretation keeping the debugger alive for post execution communication such as coverage writing public class SmokerRemote implements RemoteControl RemoteInterpreter interpreter Override public void run RemoteInterpreter intrprtr throws Exception interpreter intrprtr SmokingControl ctrl new SmokingControl interpreter Gbtrl inTt Listing 15 6 Java implementation of the RemoteControl interface The implementation of the SmokingControl is shown in Listing 15 7 In the init method it can be seen how VDM statements are executed as strings commands the World class is created and the Run operation is invoked This is the basic way of interacting with a model through the remote control functionality The finish method informs the interpreter that the remote GUI is being disposed and that execution should be stopped The AddPaper method shows how the variables defined in the init method can be used for invoking an operation The AddPaper method is called directly from the GUI Button click action as shown in Listing 15 8 public class SmokingControl RemoteInterpreter interpreter public SmokingControl RemoteInterpreter intrprtr interpreter intrprtr Controller smoke this public void init interpreter create w new World interpreter valueExecute w Run public void AddPaper 61 E Overture VDM 10 Tool
132. t Can t get record value of kind Can t get quote value of lt kind gt Can t get sequence value of kind Can t get set value of lt kind gt Can t get string value of kind Can t get map value of lt kind gt Can t get function value of kind Can t get operation value of lt kind gt Can t get object value of kind Boolean pattern match failed Character pattern match failed Sequence concatenation pattern does not match expression Values do not match concatenation pattern Expression pattern match failed Integer pattern match failed Quote pattern match failed Real pattern match failed Record type does not match pattern Record expression does not match pattern Values do not match record pattern Wrong number of elements for sequence pattern Values do not match sequence pattern 125 Overture VDM 10 Tool Support User Guide 4119 4120 4121 4122 4123 4124 4125 4126 4127 4129 4130 4131 4132 4133 4134 4135 4136 4137 4138 4139 4140 4141 4142 4143 4144 Wrong number of elements for set pattern Values do not match set pattern Cannot match set pattern String pattern match failed Tuple expression does not match pattern Values do not match tuple pattern Set union pattern does not match expression Values do not match union pattern Cannot match set pattern Exit lt value gt
133. t name gt is type maplet in map enumeration in ar else expression 92 APPENDIX D SYNTAX ERRORS EB 2041 2042 2043 2044 2045 2046 2047 2048 2049 2050 2051 2052 2053 2054 2055 2056 2057 2058 2059 2060 2061 2062 2063 2064 2065 Expectin Expectin Expectin Expectin Expectin Expectin g two arguments for isofbase g lt class gt lt exp gt arguments for isofbase g two arguments for isofclass g lt class gt lt exp gt arguments for isofclass g two expressions in samebaseclass g two expressions in sameclass Can t use history expression here Expectin Expectin Expectin Expectin Expectin g Fact active fin req or waiting g end module g library name after uselib g end module g all types values functions or operations Exported function is not a function type Expecting types values functions or operations Y Imported function is not a function type Cannot use module id name in patterns Unexpected token in pattern Expectin g identifier Expectin Found qu Expectin g a name alified name lt name gt Expecting an identifier g a name Expected is not specified or is subclass responsibility Unexpected token in statement Expecting lt object gt identifier args or name args Expecti
134. te 1ib sensor in Java The delegate lookup is only done once and only when an is not yet specified statement or expression is first reached in a class or module The jar with the external library must be placed in the VDM project in a subfolder named lib where it will be put in the class path of the interpreter when it is executed 15 1 1 External Library Example In this example a remote sensor will be defined in VDM which can read a value from a real sensor The VDM model interface of the sensor can be seen in listing 15 I and the Java class implementing it can be seen in listing The values that are to be exchanged between the Overture IDE and the jar file needs to be the internal Value objects used in Overture Documentation about these classes can be found in Appendix I class remote lib sensor operations public getValue int gt int getValue id is not yet specified end remote lib sensor Listing 15 1 Remote sensor VDM class package remote lib import org overture interpreter runtime ValueException import org overture interpreter values IntegerValue import org overture interpreter values Value public class sensor public Value getValue Value id throws ValueException int result Read a value for sensor number id return new IntegerValue result Listing 15 2 Remote sensor Java class 54 CHAPTER 15 EXPANDING VDM MODELS S
135. tem called IFEX and its pdflatex feature This can for example be obtained from e Windows http miktex org https github com overturetool overture t is planned to develop an update facility allowing updates to be applied directly from within the Overture tools without requiring a reinstallation However this can be a risky process because of the dependencies on non Overture components and so is not yet supported E Overture VDM 10 Tool Support User Guide LINE SL D ma te File Edit Navigate Search Project Run Window Help 5 E Welcome 33 Overture Tools for Formal Modelling in VDM The Overture Platform Overture is an open source tool for the Vienna Development Method VDM The tool supports different VDM dialects which include the ISO VDM SL standard as well as the object oriented extension VDM and the real time extension of that called VDM RT Getting Started See the help containing the VDM Language Manual the User Guide and a collection of examples Go to Help gt Help Contents and look for Overture Visit the Overture website for general news about releases OvertureTool org For help please use the vdm tag on StackOverflow Bugs should be reported on the GitHub tracker registration required Figure 2 1 The Overture Welcome Screen e Mac http tug org mactex e Linux Most distributions offer TEX packages Chapter 3 Using the VDM Perspective 3 1 Understanding Eclipse Ter
136. then the type of the constructed VDM value is the union of the various types passed in this example seq of bool nat1 If this VDM type is not compatible with the use of a corresponding value in the VDM model a dynamic type exception occurs when the value is processed by the model Lastly as before to get the primitive Java values of a VDM collection the following methods are provided public ValueList seqValue Context ctxt throws ValueException public String stringValue Context ctxt throws ValueException public ValueSet setValue Context ctxt throws ValueException public ValueMap mapValue Context ctxt throws ValueException Note that as with the SeqValue constructor there is a special method to return a Java String from a seq of char SeqValue rather than a ValueList of CharacterValues As be fore if the Value being used is not a sequence set or map then these methods will throw a ValueException 140 APPENDIX I USING VDM VALUES IN JAVA EB I 4 Other Types The sections above describe how to create or deconstruct simple VDM values in Java as well as simple collections of these The remainder of this section describes the unusual cases for more sophisticated types 14 1 Function values Overture has an internal Funct ionValue class used for holding values of functions e g the value of a lambda expression or the value of a function defined within a module But as f
137. tion can be written as IEX and automatically converted to PDF format Chapters 9 to cover various VDM specific features Chapter 9 explains the notion of proof obligations and their support in Overture Chapter 10 explains combinatorial testing and the automation support for that Chapter l I explains how it is possible automatically to generate executable code in pro gramming languages such as Java and C for a subset of VDM models Chapter I2 explains the support for mapping between object oriented VDM models and UML models Chapter 13 shows how a VDM project can be converted into a new VDM RT project Chapter 14 shows how to analyse and display execution logs from VDM RT models Chapter 15 demonstrates how Java can be used in combination with VDM models and Chapter 16 gives an overview of the features of Overture which are also available from a command line interface Appendix A provides a list of all the standard templates built into Overture Appendixes B to give complete lists of pos sible errors warnings and proof obligation categories Appendix H provides an overview of the VDM VDM RT to UML mapping rules Appendix I provides details about how to represent VDM values in order to combine Java with VDM as described in Chapter 15 Finally there is an index of significant terms used in this manual Chapter 2 Getting Hold of the Software Overture This is an open source tool developed by volunteers and built on the
138. tion count expression is either 0 or 1 or if it s greather than 1 then the map s range is a subset of its domain map sequence compatible When defining a map with enumeration ensures that any two equal elements in the domain map to the same element in the range map set compatible When merging a set of maps any two equal elements in the domains of each map map to the same element in the range non empty sequence This kind of proof obligation is used whenever non empty sequences are required eg taking the head of a sequence non empty set This kind of proof obligation is used whenever non empty sets are required non zero This kind of proof obligation is used whenever zero cannot be used e g in division operation parameter patterns When using a pattern as an operation parameter ensures that all values in the operation parameter type can match the pattern operation post condition Whenever an explicit operation has a post condition there is an im plicit proof obligation generated to remind the user that you have to ensure that the explicit body of the operation satisfies the post condition for all possible inputs operation satifiability For all implicit operation definitions this proof obligation will be gener ated to ensure that it is possible to find an implementation satisfying the post condition for all arguments satisfying the pre conditions post condition Whenever a function has a post condition this checks that th
139. to the JAR Select the resources to export DIES Gif test Y D Controllerjava ME graphic 7 D Graphics java DE Smoking Y M ISmokingControl java 4 BE SmokingEx Y J Model java 4 MI src V JJ SmokerRemote java v gui 7 SmokingControl java Y FB gui resources V D Viewjava 7 gt settings Y Export generated class files and resources Export all output folders for checked projects Export Java source files and resources F Export refactorings for checked projects Select refactorings Select the export destination JAR file C vdmworkspace SmokingEx lib graphics jar X Browse Options Y Compress the contents of the JAR file Add directory entries Y Overwrite existing files without warning o Ge Gm es Figure 15 5 Exporting to a Jar in Eclipse 15 4 Generated GUI of VDM Models Overture has a feature for controlling a VDM model with a generic GUI automatically generated from the model The generated GUI follows the same principles as discussed in But rather than the user having to implement the GUI himself everything is automatically generated In order to use the Generated GUI feature simply launch the model as a VDM GUI configuration see Figure 15 8 Once the model has launched the generic GUI will offer a list of all classes allowing to create instances of each see Figure 15 9 These instances can then be selected to inspect their state and invoke operations see Figure 15 10 Any creat
140. top assuming the specification has no type checking errors For batch execution the e option can be used to identify a single expression to evaluate in the context of the loaded specification assuming the specification has no type checking errors 16 2 Parsing Type Checking and Proof Obligations Command Line All specification files loaded are parsed and type checked automatically by the command line tool There are no type checking options the type checker always uses possible semantics Ifa 70 CHAPTER 16 ACOMMAND LINE INTERFACE TO OVERTURE E specification does not parse and type check cleanly the interpreter cannot be started and proof obligations cannot be generated though warnings are allowed All warnings and error messages are printed on standard output even with the q option A source file may contain VDM definitions embedded in a BIEX file using vdm al envi ronments see Chapter 8 the markup is ignored by the parser though reported line numbers will be correct Note that each source file must start with a recognizable IZ TEX construct a Ndocumentclass section subsection or a MEX comment The Overture Java process will return with an exit code of zero if the specification is clean ignoring warnings Parser or type checking errors result in an exit code of 1 The interpreter and PO generator always exit with a code of zero 16 3 The Command Line Interpreter and Debugger Assuming a specification does not c
141. use of a special Combinatorial Testing per spective to automatically expand the trace and execute all of the resulting test cases Subsequently the results from the tests can be inspected and erroneous test cases easily found You can then fix problems and re run the trace to check they are fixed 10 1 Using the Combinatorial Testing GUI The syntax for trace definitions is defined in the VDM 10 Language Manual Larsen amp 10 If you have created a traces entry for a module or class it can be executed via the Combinatorial Testing perspective see Figure Different icons are used to indicate the verdict in a test case These are 4 This icon is used to indicate that the test case has not yet been executed 4 This icon is used to indicate that the test case has a pass verdict This icon is used to indicate that the test case has an inconclusive verdict 3 This icon is used to indicate that the test case has a fail verdict o SA 2800 skipped 120 If any test cases result in a run time error other test cases with the same sequence of calls will be filtered and automatically skipped in the test execution The number of skipped test cases is indicated after the number of test cases for the trace definition name In the CT Overview view you can right click on any individual test case and then send it to the interpreter for execution see Fgure 10 2 This is particularly useful for failed test cases since the interpreter allows you to
142. working on the specification The Outline view on the right hand side of Figure 3 1 presents an outline of the file selected in the editor The outline shows all VDM definitions such as state definitions values types functions and operations The type of each definition is also shown in the view and the colour of the icons in front of the names indicates the accessibility of each definition Red is used for private definitions yellow for protected definitions and green for public definitions Triangles are used for type definitions small squares are used for values state components and instance variables functions and operations are represented by larger circles and squares permission predicates are shown with small lock symbols and traces are shown with a T Functions have a small F superscript over the icons and static definitions have a small S superscript Record types have a small arrow in front of the icon and if that is clicked the fields of the record can be seen 7 E Overture VDM 10 Tool Support User Guide E VDM AlarmPP plantvdmpp Tools IO x File Edit Navigate Search Project Run Window Help SRS 0 i Switch perspective E vom Explorer 25 ELI alarm vdmpp Eg expert vampp Ez plantvdmpp ES PO Proof Obliga ff Combinatori 35 Debug ET 8 Outline 3 wwe web mberOfExperts p Q Plant BA PES ONDE Some eer o alarms set of Alarm rA PTe p in s
143. xt Templates rr Praag Create edit or remove templates Install Update Name Context Description Autolns Nem Run Debug act VDM PP Template context type The number of times that operation name operatio on E Edit Team st VDM RT Template context type The number of times that operation name operatio on al vom Y active VDM PP Template context type The number of operation name operations that are on Min IV active VDM RT Template context type The number of operation name operations that are on Es ae E bus VDM RT Template context type BUS Priority lt CSMACD gt capacity set of connecte on a V caseExpression VDM PP Template context type Case Expression on V caseExpression VDM RT Template context type Case Expression on V caseExpression VDM SL Template context type Case Expression on V class VDM PP Template context type Class Definition on V class VDM RT Template context type Class Definition on V classSkeleton VDM PP Template context type Class Definition full skeleton on V classSkeleton VDM RT Template context type Class Definition full skeleton on IV cpu VDM RT Template context type CPU Priority lt FP FCFS gt capacity on Preview Cw O Figure 5 2 Adjusting templates for Overture Chapter 6 Interpretation and Debugging in Overture This chapter describes how to run and debug a model using the Overture IDE 6 1 Run and Debug Launch Configurations To execute or debug a VDM model you
144. y day myex Error 4130 Instance invariant violated inv_Plant in Plant at line 6 4 Figure 10 1 Using Combinatorial Testing concfactorialvdmpp Worldwdmrt IO vdmrt usetreevdmpp 2 class UseTree instance variables tl BinarySearchTree new BinarySearchTree t2 Tree new BinarySearchTree traces let n in set 1 ti Insert n 2 ti breadth first search tl depth first search ti inorder tl isEmpty 5 in end UseTree Bi Problems EE Console Bil CT Test Case result 22 PO Proof Obligation Explorer Trace Test case Result tl Insert 2 0 tLinsert 1 0 tl breadth first search 4 POP3Test w Two 0 4 GS SAFERPP 4 Test w BT 62 w HT 4 amp SortPP 4 SortMachine 1 DiffSorting 0 a 5 Tree 4 UseTree 4 amp insertion BST 100 Test 000001 x Send to Interpreter Error 4087 Cannot convert lt Empty gt at line 75 23 Figure 10 2 Moving test case from Combinatorial Testing to Interpreter 38 Chapter 11 Automatic Generation of Code It is possible to generate Java code for a large subset of VDM SL and VDM models In addition to Java a C code generator is currently being developed but this work is in its early stages of development and it is not included with releases of Overture yet For comparison code generation of VDM SL and VDM specifications to both Java and C is a feature that is availa
145. y libraries and can be can be re loaded without the pars ing checking overhead If files are sufficiently large this may be faster pre This will disable all pre condition checks post This will disable all post condition checks inv This will disable type state invariant checks dtc This will disable all dynamic type checking measures This will disable recursive measure checking log This will enable VDM RT real time event logging see Chapter 14 remote This enables remote control of the Overture executable Alternatively a script file will also be made for the different platforms script and bat files wrapping this functionality so one does not need to explicitly point to the Overture jar This script 1s planned for the next version version of the tool Normally a VDM model will be loaded by identifying all of the VDM source files to include At least one source file must be specified unless the i option is used in which case the interpreter can be started with no specification If a directory is specified rather than a file then Overture will load all files in that directory with a suffix that matches the dialect e g vdmpp files for VDM Multiple files and directory arguments can be mixed If no i option is given the tool will only parse and type check the VDM model files giving any errors and warnings on standard output then stop The p option will run the proof obligation generator and then s

Overture VDM-10 Tool Support: User Guide

Contents

Download Pdf Manuals

Related Search

Related Contents