Theorem Proving Support - User Manual
Contents
1. ES theory UserDwarf B theory UserDwarf imports utp_cml Dwa Vi Dwarf imports utp cml Dwarf Auto generated THY file for user create Y E generated begin Y F theorem nsa NeverShowAll mk_Dwarf Y gt Isabelle E oops gt 3 Thu Aug 29 09 42 x Y F theorem molc MaxOneLampChange r gt gt Thu Aug 29 09 56 text Auto generated THY file for user created proof with Dwarf thy oops Y Thu Aug 29 14 26 2 Y F theorem fstd ForbidStopToDrive mk_ gt model theorem nsa oops 18 Dwarf thy amp NeverShowAll mk_DwarfType 8stop amp stop 1 amp stop amp stop true 2 A UserDwarf thy oops DISCHARGE THEOREM nsa O Dwarf cml theorem molc MaxOneLampChange mk DwarfType stop amp stop 1 amp stop amp stop true oops DISCHARGE THEOREM molc theorem fstd amp ForbidStopToDrive mk_DwarfType amp stop amp stop amp stop amp stop true theories X PHS O oops DISCHARGE THEOREM fstd Prover ready type filter text end amp Dwarf ee amp UserDwarf type filter text P Prover Output X far Problems E Console 9 Error Log Y Arrow leftarrow longleftarrow rightarrow longrightarrow lt Leftarrow lt Longleftarrow gt Rightarrow gt Longrightarrow leftrightarrow Writable Figure 17 Unproved theorems in Isabelle perspective Outline 3 E m a theo2. 2 forms two parts executable code and documenta tion The executable code is provided as described in Section 2 and the documentation is provided in two documents This document D33 2a is the first part the user manual which provides details on obtaining and installing the theorem proving support for CML and also how to use this support within the CML platform inside Eclipse The second part of the D33 2 documentation the technical details of the theorem proving support 1s provided in document D33 2b D33 2a Theorem Proving User Manual Public COMPASS Contents 1 Introduction 6 2 Obtaining the Software 7 AU AI AA 7 22 UYP CMIL Theories 4 2 4 224 66 8 ee bee dew de wd 8 3 Instructions for installation of Isabelle UTP 10 3l MacOS Mins ecw ee een th eee ee eee eee ee ee 10 3 2 Windows aoaaa 13 aa ee nee eee MAPA nee a 15 3 4 Updating Theories 0 2 2 0 16 3 5 Troubleshooting 17 4 Using Isabelle perspective with COMPASS tool 18 5 Proving CML Theorems 22 6 Conclusions 26 D33 2a Theorem Proving User Manual Public COMPASS 1 Introduction This document 1s a user manual for the theorem proving support provided by the COMPASS tool an open source tool supporting systematic engineering of System of Systems using the COMPASS Modelling Language CML This document is targeted at users with limited experience working with Eclipse based tools Di rections are given
3. Aug 29 09 42 f Y E theorem molc MaxOneLampChange r gt Thu Aug 29 09 56 text Auto generated THY file for user created proof with Dwarf thy Y by Y Thu Aug 29 14 26 2 Y E theorem fstd ForbidStopToDrive mk_ gt model theorem nsa Y by 18 Dwarf thy NeverShowAll mk DwarfType amp stop amp stop 1 amp stop amp stop true e end 3 UserDwarf thy by cml_tac Dwarf cml theorem molc MaxOneLampChange mk DwarfType stop amp stop amp stop amp stop true by cml tac theorem fstd ForbidStopToDrive mk DwarfType amp stop amp stop amp stop amp stop true Theories X gt O by cml_tac Prover ready 7 type filter text end 6 Dwarf di a amp UserDwarf _ type filter text P Prover Output 33 fai Problems EJ Console 9 Error Log Y Es Arrow Ignoring duplicate rewrite rule leftarrow el pie t1 gt el ie b1 gt t1 True Ignoring duplicate rewrite rule el 3e tl gt el e b1 t1 True Ignoring duplicate rewrite rule b1 3b x1 gt x1 True Ignoring duplicate rewrite rule tl vtype x1 gt b1 3b x1 t1 True Ignoring duplicate rewrite rule D None False longleftarrow rightarrow longrightarrow lt Leftarrow lt Longleftarrow gt Rightarrow gt Longrightarrow leftrightarrow Writable Figure 19 Discharged the
4. as to where to obtain the software This user manual does not provide details regarding the underlying CML formal ism Thus if you are not familiar with this we suggest the tutorial for CML before proceeding with this user manual BGW12 However users broadly familiar with CML may find the Tool Grammar reference COMPASS Deliverable D31 2c Col13 useful to ensure that the they are using the exact syntax accepted by the tool This version of the document supports version 0 1 4 and later of the COMPASS tool suite The intent is to introduce readers to how use the theorem proving support plugin available in this version of the tool The main tool is the COMPASS IDE which integrates all of the available CML analysis functionality and provides editing abilities Section 2 describes how to obtain the software Section 3 describes how to install the software in the COMPASS tool Section 4 explains how to use the COMPASS Eclipse perspective and Section 5 describes how to prove theorems in the COM PASS tool Conclusions are drawn in Section 6 It should be noted that it is beyond the scope of this document to provide detailed descriptions of how to prove theorems in the Isabelle tool or to provide a tutorial on it s use We therefore recommend that interested parties should read this de liverable in conjunction with tutorials on Isabelle and proving in the Isabelle tool available on the Isabelle websitd http isabelle in tum de docu
5. correct logic More detailed instructions are provided at the Isabelle Eclipse website which may be of use http andriusvelykis github io isabelle eclipse getting started If errors persist please report them using the COMPASS platform bug tracking facility http sourceforge net p compassresearch tickets D33 2a Theorem Proving User Manual Public COMPASS 4 Using Isabelle perspective with COMPASS tool The steps in this section should be followed to begin proving theorems using the Isabelle theorem proving support plugin for the COMPASS tool The steps enable the user to prove theorems for a specific CML model 1 With a CML model open right click on the model filename in the Project Explorer and select CML THY gt Generate Theorem Prover THY as shown in Figure 600 CML Dwarf Dwarf cml CML Compass Project Users nrjp6 Deskt rv A A n He OQ A 4 to Pr CML Explorer 53 2 O pwarf cml 52 B v types gt EXCMLProject Lampld lt Ll gt lt L2 gt lt L3 gt Signal set of Lampld Y Dwarf ProperState Signal New p ps in set dark stop warning driv Dwarf 0 pen ype lastproperstate ProperState Open With gt turnoff set of Lamp turnon set of Lamp Copy C laststate Signal Paste currentstate Signal desiredproperstate ProperState X Delete DO _ Move currentstate d turnoff union d turnc Rename F2 arnoff inter d turnon and R everShow All 2
6. gt dl Isabelle Mac App S Press the Delete b is Press the Filter bu Edit or view an exis Configure launch perspe Figure 1 New Launch Configuration button 4 In the Main tab provide the location of the Isabelle application for example Applications Isabelle2013 app Use the Browse File System button to navigate to the correct location if required see Figure 2 NOTE do not select a logic at this point 10 D33 2a Theorem Proving User Manual Public COMPASS Le OO Isabelle Configurations Create manage and run configurations Q x Isabelle logic must be selected JE Jz Za X E Ser Name Isabelle CML ill E Main E Session Source PE Environment oi Build E Common dh isabelle Isabell lication bundl l l ion a kaheli for Widia sabelle application bundle app location V dh Isabelle Mac App Applications Isabelle2013 app dh New configuratio Browse File System Session type filter text HOL HOL Algebra HOL Library HOL Multivariate_Analysis HOL Nominal HOL SPARK HOL Word HOLCF o ZF Filter matched 4 of 4 items D Close Run Figure 2 Isabelle configuration in COMPASS Tool Mac 5 Select the Session Source tab and click the Add external button Nav igate to the location of the utp isabelle folder extracted in Section 2 2 see Figure 3 and click Open E Main Session
7. the menu bar select Run gt Isabelle gt Isabelle Configurations 3 Select Isabelle for Windows in the left hand pane click the New Launch Configuration button see Figure lin Section 3 1 and provide a name for the configuration sabelle CML 4 In the Main tab provide the location of the Isabelle application for example C Programs Isabelle2013 as chosen in Section 2 1 Use the Browse File System button to navigate to the correct location 1f required see Figure 8 13 D33 2a Theorem Proving User Manual Public COMPASS NOTE do not select a logic at this point Create manage and run configurations Isabelle logic must be selected Ex a 3 Name Isabelle CML type filter text FE Main gt E Session Source P Environment n Build Ed Common dh Isabelle Isabelle location a dh Isabelle for Windo rem C Program Files x86 Isabelle Isabelle2013 dh Isabelle Mac App Browse File System Cygwin directory location e g within Isabelle installation C Program Files x86 Isabelle Isabelle2013 contrib cygwin Browse File System Session type filter text HOL F HOL Algebra HOL Library HOL Multivariate_Analysis HOL Nominal HOL SPARK HOL Word HOICF yr TT i t Filter matched 4 of 4 items Figure 8 Isabelle configuration in COMPASS Tool Windows 5 Ensure that the Cygwin directory
8. 3 2a Theorem Proving User Manual Public Create manage and run configurations Isabelle logic must be selected v db Isabelle Isabelle CML dh Isabelle for Windows dk Isabelle Mac App C gt Filter matched 4 of 4 items O COMPASS a Name Isabelle CML E Main Ey Session Source BB Environment i Build Common Isabelle location local dOp6 simonf lsabelle lsabelle2013 Browse File System Session C 4 HOL Algebra C 4 HOL Library 4 HOL Multivariate Analysis C HOL Nominal C 4 HOL SPARK C 4 HOL Word C 4 HOLCF O 9 ZF 9 CCL C 4 CCL ex E HOL E Figure 9 Isabelle configuration in COMPASS Tool Linux Figure 6 9 Click the Apply button to save the configuration and click the Run button to start Isabelle NOTE the first time Isabelle is invoked several minutes are needed to initialise and build the theories Subsequent uses of Isabelle will not require this long wait To monitor progress click on the button on the bottom right of the tool as highlighted in Figure 7 3 4 Updating Theories Periodically the UTP CML theories will be updated When a new version is available follow the steps in Section 2 2 to obtain and unpack the newest theories When this is done several of the steps described in Section 3 1 3 2 or 3 3 should be repeated For all platforms 1 O
9. Import rrentstate lt gt lt L1 gt lt L2 gt lt L3 gt and t Export axOneLampChange Cd currentstate Y d laststate union amp Refresh FS rbidStopToDrive lastproperstate stop gt d desiredpror kOnlyToSto gt ar y p Debug As lastproperstate dark gt d desiredpror Run As gt arkOnlyFromStop Team gt jesiredproperstate dark gt d lastpror Compare With gt a ignal DwarfType Replace With gt 2 NeverShowAll d and Model check gt MaxOneLampChange d and Pos CML POG b ForbidStopToDrive d and y CML THY e Generate Theorem Prover THY Properties E dark Signal stop Signal lt L1 gt lt L2 gt woarninn Siannl felis el 21 Figure 10 Initiate production of a theory file for a CML model 2 This creates two theory files with the thy file extension a model specific read only file for the CML model lt modelname gt thy and a user editable file lt modelname gt Userthy These files along with a read only version of the CML model are added to a timestamped folder in the PROJECT gt generated gt Isabelle folder of the CML project see Figure 1 1 Note this file is specific to the current state of the model Any changes made to the CML model will not be reflected in the thy file and thus the process must be restarted The generated model thy file uses a combination of regular 18 D33 2a Theorem Proving User Manual Public COMPASS Isabelle syntax which 1s described in vari
10. SEVENTH FRAMEWORK PROGRAMME Grant Agreement 287829 Comprehensive Modelling for Advanced Systems of Systems COMPASS Theorem Proving Support User Manual Technical Note Number D33 2a Version 1 0 Date September 2013 Public Document http www compass research eu D33 2a Theorem Proving User Manual Public Contributors Simon Foster UY Richard Payne NCL Editors Simon Foster UY Richard Payne NCL Reviewers Juliano Iyoda UFPE Jan Peleska UB Lu s D Couto AU COMPASS D33 2a Theorem Proving User Manual Public COMPASS Document History 18 06 2013 Richard Payne 0 02 02 07 2013 Richard Payne Added details on obtain ing installing and using Isabelle 03 AE 07 2013 Richard O Initial draft of document e first milestone hai 04 ae 08 2013 Richard Payne Changes throughout to support ongoing work and to include details on prov ing in Isabelle perspective O hisi 04 2013 Richard Final changes to reflect 18 09 2013 Richard Payne Simon Foster LDC review comments pas o js ir se 0 07 23 09 2013 Richard Payne JI review comments ad a A amea o A 26 09 2013 Richard Payne Final revision for EC D33 2a Theorem Proving User Manual Public COMPASS Summary Work Package 33 delivers a collection of static analysis tool support for reason ing in CML This deliverable forms the documentation for Task 3 3 2 theorem proving Deliverable D33
11. Sor ree gt RE Environment lad Build E Common Additional Isabelle session directories gt Users nripo Isabelle utp isabelle Add directories Add external Remove Figure 3 Isabelle configuration in COMPASS Tool Session source 6 For licensing of the Z3 theorem prover used by the Isabelle tool select the Environment tab and click the New button In the Name text box This part of the tool is available free for non commercial use For licens 11 D33 2a Theorem Proving User Manual Public COMPASS enter Z3 NON COMMERCIAL and in the Value text box enter yes see Figure 4 and click Ok Ensure the Append environment to the native environment option 1s selected Name Isabelle CML EE Main Es Session source Environment E Build S Common Environment wariables to set Variable Value New 73_NON_COMMERCIAL yes AOG Edit Environment Variable Ras Name 3 NON COMMERCIAL Edit Value yes Variables Remove Cancel o Figure 4 Isabelle configuration in COMPASS Tool Environment 7 Select the Build tab and select the Build sessions to user home directory button see Figure 5 EE Main Es Session Source Pe Environment T bu id El Common A Build sessions before launch otherwise session heaps must be already av
12. ailable Build output location a Build sessions to Isabelle system directory Build sessions to user home directory Figure 5 Isabelle configuration in COMPASS Tool Build 8 Select the Main tab and in the Session field choose the HOL UTP CML logic there is a filter text box which may help locate the correct logic see Figure 6 9 Click the Apply button to save the configuration and click the Run button to start Isabelle NOTE the first time Isabelle is invoked several minutes are needed to initialise and build the theories Subsequent uses of Isabelle will not require this long wait To monitor progress click on the button on the bottom right of the tool as highlighted in Figure 7 ing information see http www microsoftstore com store msuk en GB pdp Microsoft Research Z3 Theorem Prover product ID 278142500 12 D33 2a Theorem Proving User Manual Public COMPASS E Es Session Source PE Environment n Build S Common Isabelle application bundle app location Applications Isabelle2013 app Browse File System Session HOL UTP CML Figure 6 Isabelle configuration in COMPASS Tool Selecting logic Insert 9 15 Launching Isabelle CML 57 Figure 7 Isabelle configuration in COMPASS Tool initialisation progress 3 2 Windows 1 Open the COMPASS Tool application 2 Configure the COMPASS Tool to use Isabelle From
13. avigate to their loca tion in the project explorer and double click on the file name Using the theory file editor pane theorems and lemmas may be defined and proven The theory editor of Isabelle Eclipse provides an interactive asynchronous method for theorem proving similar to the Edit interface distributed with Isabelle The theory file is submitted to Isabelle and results are reported asynchronously in the editor and prover output panes The editor has syntax highlighting for the Isabelle syntax and problems are marked and displayed in the output pane In the next section we use the steps defined here to use the Isabelle perspective to prove lemmas related to an example CML model Tt is beyond the scope of this document to describe the Isabelle syntax interested readers are directed to the tutorials available athttp isabelle in tum de 21 D33 2a Theorem Proving User Manual Public COMPASS 5 Proving CML Theorems In this section we provide a brief overview to theorem proving in the COMPASS tool As proving theorems about a CML model in Isabelle is performed in much the same way as normal theorem proving in Isabelle the interest reader should refer to tutorials on theorem proving with Isabelle for more details To illustrate the process of proving theorems we use an example introduced in Part B of this deliverable the Dwarf signal controller In Figure the original CML model Dwarf cml and the generated th
14. ck method of adding mathematical symbols to a the ory file The user can double click a symbol which will be added to the proof script http isabelle in tum de documentation html 19 D33 2a Theorem Proving User Manual Public COMPASS 8 theory Dates imports Main begin type synonym day nat datatype month jan Feb Mar r ar nat i Travel Agent definition months month list where months Jan Feb Mar Apr May June July Aug Sep Oct Nov Dec definition numberMonth nat gt month where numberMonth n months n 1 Project lemma monthNumber_inv simp numberMonth monthNumber m m Explorer apply unfold numberMonth_def apply unfold months_def apply case_tac m apply simp_all done lemma atLeastAtMost_unfold m lt n Theory File Suc m n by auto done lemma month list simp UNIV set ma r numpermonth n n S apply S apply S apply S apply lemma numberMonth_inv simp n 1 nat iz gt nnumoe apply simp del atLeastAtMost_iff add atLeastAtMost_unfold apply unfold numberMonth_def apply unfold months_def apply unfold atLeastAtMost_def apply auto done lemma month_list simp UNIV set months apply simp add months_def apply unfold set_eq_iff apply clarify apply case_tac x apply simp all done record raw date proof prove step O pegas sera A longleftrightarrow gt Leftrighta
15. ff inter d turnon and NeverShow ALL t definition warning lt L1 gt lt L3 gt Signal d currentstate lt gt lt Li gt lt L2 gt lt L3 gt and MaxOneLampChange definition drive lt L2 gt lt L3 gt Signal card d currentstate d laststate union d laststate Y d currentst ForbidStopToDrive ee daa r definition init MkChanD init arallel rallel gt Cd Lastproperstate stop gt d desiredproperstate lt gt drive and 00 S5 yop e DarkOnlyToStop inician E ET ar Cd lastproperstate dark gt d desiredproperstate in set dark stor definition HR a ASR oanp Ipari DarkOnlyFromStop sas TT n d desiredproperstate dark gt d lastproperstate in set dark stor definition extinguish MkChanD extinguish lt parallel gt LampId lt parallel gt DwarfSignal DwarfType definition shine MkChanD shine lt parallel gt Signal lt parallel gt inv d NeverShowA11 d and MaxOneLampChange d and definition thunk MkChanD thunk lt parallel gt lt parallel gt ForbidStopToDrive d and DarkOnlyToStop d and definition ProperState lt parallel gt Signal inv ps ps in set dark stop DarkOnLyFromStop d typedef DwarfType Tag True by auto values i instantiation DwarfType_Tag tag dark Signal begin stop Signal lt L1 gt lt L2 gt definition tagName_DwarfType_Tag x DwarfType_Tag DwarfT
16. he underlying theories used Mhnttp isabelle in tum de 26 D33 2a Theorem Proving User Manual Public COMPASS References BGW 12 CMLC13 Col13 FP13 WCF 12 Jeremy Bryans Andy Galloway and Jim Woodcock CML definition 1 Technical report COMPASS Deliverable D23 2 September 2012 Joey W Coleman Anders Kaels Malmos Rasmus Lauritsen and Luis D Couto Second release of the COMPASS tool user manual Technical report COMPASS Deliverable D31 2a January 2013 Joey W Coleman Second release of the COMPASS tool tool grammar reference Technical report COMPASS Deliverable D31 2c January 2013 Simon Foster and Richard J Payne Theorem proving support de velopers manual Technical report COMPASS Deliverable D33 2b September 2013 J Woodcock A Cavalcanti J Fitzgerald P Larsen A Miyazawa and S Perry Features of CML a Formal Modelling Language for Systems of Systems In Proceedings of the 7th International Confer ence on System of System Engineering IEEE July 2012 27
17. ibed in various Isabelle manuals and tutorials and the Isabelle syntax defined for CML This Isabelle CML syntax is described in detail in FP13 Each theorem has the oops keyword below This signifies that we aim to prove the theorem at a later point and do not yet provide any proof In the theory outline pane shown in more detail in Figure the oops keyword is specified and the box icon denotes the proof is not complete Also no prover output is shown when selecting an area after the proofs If the user wants more information about the theorem this is available by placing the editor cursor on the theorem In Figure 19 we discharge these theorems The theorems are all simply proved us ing the cml_tac proof tactic The tactic is applied by using the line by cml tac on the line below the theorem This applies rules and tactics defined in the isabelle utp UTP and CML theories imported during the initial setup of the the orem prover This tactic is described in more detail in Part B of this deliver able FP131 inttp isabelle in tum de documentation html 23 D33 2a Theorem Proving User Manual Public COMPASS 8 O O Isabelle Dwarf generated Isabelle Thu Aug 29 14 26 20 BST 2013 UserDwarf thy CML Compass Project Users nrjp6 Desktop COMPASS COMPASS app Contents MacOS workspace y EZ a ma Q 77 ES cm dhe Isabelle PS Project Explorer 32 O warfeml B UserDwarf thy 53 8 Dwarf thy BE Outline 33 ll
18. ions 3 Select Isabelle in the left hand pane click the New Launch Configuration button see Figure I in Section 3 1 and provide a name for the configura tion Isabelle CML 4 In the Main tab provide the location of the Isabelle application for exam ple usr bin Isabelle2013 as chosen in Section 2 1 Use the Browse File System button to navigate to the correct location 1f required see Figure 9 NOTE do not select a logic at this point 5 Select the Session Source tab and click the Add external button Nav igate to the location of the utp isabelle folder extracted in Section 2 2 see Figure 3 and click Ok 6 For licensing of the Z3 theorem prover used by the Isabelle tool select the Environment tab and click the New button In the Name text box enter Z3 NON COMMERCIAL and in the Value text box enter yes and click Ok Ensure the Append environment to the native environment option is selected 7 Select the Build tab and select the Build sessions to user home directory button see Figure 5 8 Select the Main tab and in the Session field choose the HOL UTP CML logic there is a filter text box which may help locate the correct logic see This part of the tool is available free for non commercial use For licens ing information see http www microsoftstore com store msuk en GB pdp Microsoft Research Z23 Theorem Prover productID 278142500 15 D3
19. is automatically populated Isabelle dis tributes Cygwin thus this should be automatically obtained if not manu ally locate a Cygwin installation 6 For licensing of the Z3 theorem prover used by the Isabelle tool select the Environment tab and click the New button In the Name text box enter Z3 NON COMMERCIAL and in the Value text box enter yes and click Ok Ensure the Append environment to the native environment option is selected 7 Select the Main tab and in the Session field choose the HOL UTP CML This part of the tool is available free for non commercial use For licens ing information see http www microsoftstore com store msuk en GB pdp Microsoft Research Z3 Theorem Prover productID 278142500 14 D33 2a Theorem Proving User Manual Public COMPASS logic there is a filter text box which may help locate the correct logic see Figure 6 8 Click the Apply button to save the configuration and click the Run button to start Isabelle NOTE the first time Isabelle is invoked several minutes are needed to initialise and build the theories Subsequent uses of Isabelle will not require this long wait To monitor progress click on the button on the bottom right of the tool as highlighted in Figure 7 33 Linux 1 Open the COMPASS Tool application 2 Configure the COMPASS Tool to use Isabelle From the menu bar select Run gt Isabelle gt Isabelle Configurat
20. ists This is ok choose to replace the existing file 4 Copy the utp isabelle folder from the extracted folder to the src folder in the Isabelle2013 application folder e g C Program Files Isabelle20131src As the CML and UTP theories are improved new versions will be made available As new versions are uploaded follow the above steps to obtain and unpack the updates See Section 3 4 for details of setting up updated theories D33 2a Theorem Proving User Manual Public COMPASS 3 Instructions for installation of Isabelle UTP This section provides the steps required to use Isabelle in the COMPASS tools This setup procedure 1s only required on the first use of the theorem prover How ever if a new version of the COMPASS tools is installed then the procedure must be repeated Instructions for installation with the COMPASS tool are given for each supported platform below 3 1 Mac OSX 1 Open the COMPASS Tool application 2 From the menu bar select Run gt Isabelle gt Isabelle Configurations 3 Select Isabelle Mac App in the left hand pane click the New Launch Con figuration button see Figure 1 and provide a name for the configuration Isabelle CML B600 Isabelli Create manage and run configurations Configure Isabelle theorem prover by indicating the ir E Ger Configure launch setting A filter text Ly Press the New but Isabelle ES Press the Duplicats db Isabelle for Windows
21. mentation html 6 D33 2a Theorem Proving User Manual Public COMPASS 2 Obtaining the Software This manual assumes the user has the version 0 2 0 or later of the COMPASS tools pre installed The COMPASS tool set may be obtained from http sourceforge net projects compassresearch files Releases For instructions on installation see the COMPASS user manual CMLC13 To use the theorem proving functionality of the tools the Isabelle theorem prover and UTP CML theory files must first be obtained This is described in this sec tion 2 1 Isabelle Isabelle is a free application distributed under the BSD license It is available for Linux Windows and Mac OS X The tool is available at http isabelle in tum de Instructions for installation for each platform are provided in the following sec tions 2 1 1 MacOSX Instructions for installation of Isabelle for Mac are as follows 1 Download Isabelle for Mac distributed as a dmg disk image 2 Open the disk image and move the application into the Applications folder 3 NOTE Do not launch the tool at this point 2 1 2 Windows Instructions for installation of Isabelle for Windows are as follows 1 Download Isabelle for Windows distributed as an exe executable file 2 Open the executable which automatically installs the Isabelle tool 3 NOTE Do not launch the tool at this point D33 2a Theorem Proving User Manual Public COMPASS 2 1 3 Linux Instruc
22. orems in Isabelle perspective JE Outline E a theory UserDwarf imports utp_cml Dwarf begin Auto generated THY file for user created proof Y E theorem nsa Never5ShowAll mk_DwarfTypel stop amp sto v by Y E theorem molc MaxOneLampChange mk_DwartfType si v by Y E theorem fstd ForbidstopToDrivelmk_DwarfTypel stop v by e end Figure 20 Proof outline of proved theorems Isabelle perspective recommend that interested parties should read this deliverable in conjunction with tutorials on Isabelle and proving in the Isabelle tool available on the Isabelle website nttp isabelle in tum de documentation html ZS D33 2a Theorem Proving User Manual Public COMPASS 6 Conclusions This document has given an introduction to using Isabelle in the COMPASS tool to perform theorem proving with CML models The document is not able to pro vide a thorough introduction to proving using Isabelle therefore the interested reader should refer to the Isabelle websitd for extensive tutorial and exercise lit erature on proving in Isabelle and the underlying fundamentals of Isabelle Whilst the UTP logic used in proving in CML 1s not used in the literature at this website the general lessons are applicable The companion deliverable D33 2b provides more technical insight into the de velopment of the theorem proving support plugin and should be read in conjunc tion to this user manual for a greater understanding of t
23. ous Isabelle manuals and tutori als and the Isabelle syntax defined for CML This Isabelle CML syntax is described in detail in FP 131 E Project Explorer 3 H S A gt Y BitRegister g Dwarf gt generated Isabelle b 2013 09 18 12 31 15 b 2013 09 18 12 34 13 2013 09 18 15 55 10 b 2 model Dwarf_User thy Dwarf thy Dwarf cmil Dwarf launch E2 EmergResp TIF Figure 11 Project explorer with generated thy files 3 The COMPASS tool should automatically switch to the Isabelle perspective and open the newly generated files Once open the Isabelle perspective will look like Figure 12 There are various panes in the perspective as follows Project Explorer Similar to the CML perspective this pane shows the projects created in the user s workspace and their contents Theory File Editor A text editor which enables the user to interact with the theory script and prove theorems add additional definitions lemmas and theorems Theory Outline This pane provides an outline to the contents of the se lected theory file including definitions functions lemmas and theo rems and may be used to navigate the theory file Prover Progress A collection of status bars for the currently open theory files shows the progress made by Isabelle in proving the scripts in the theory file Prover Output A window to report error messages and the status of the goals of selected theorems Symbol Viewer A qui
24. pen the COMPASS Tool application 16 D33 2a Theorem Proving User Manual Public COMPASS 2 Select Run gt Isabelle gt Isabelle Configurations from the menu bar to begin editting the existing Isabelle configuration 3 Select Isabelle in the left hand pane select the configuration Isabelle CML found under the option corresponding to the correct platform 4 Select the Session Source tab select the location of the previous utp isabelle folder and click the Remove button 5 Still on the Session Source tab click the Add external button Navigate to the location of the new utp isabelle folder extracted in Section 2 2 6 Select the Main tab and in the Session field choose the HOL UTP CML logic there is a filter text box which may help locate the correct logic see Figure 6 7 Click the Apply button to save the changes made to the configuration and click the Run button to start Isabelle NOTE the first time Isabelle is invoked with the new theory several minutes are needed to initialise and build the theories Subsequent uses of Isabelle will not require this long walt 3 5 Troubleshooting Error reporting in Isabelle is not always very clear If errors are encountered ensure that the instructions have been followed carefully especially when set ting the Z3 NON COMMERCIAL environment variable in OS X and Linux selecting the correct location of the utp isabelle theory and selecting the
25. rrow Prover Output lt gt Longleftrightarrow mapsto longmapsto midarrow Midarrow Figure 12 Overview of Isabelle perspective in COMPASS Tool 4 If the Isabelle perspective 1s not opened automatically or the perspective needs changing manually then select the icon labelled b in Figure and then select Isabelle and then ok If the perspective has been used previously then select the Isabelle perspective using the button labelled e in Figure 13 HE Outline 53 Y Types Lampld Signal ProperState a Fe Pr M gt 2 CMLProject YE Dwarf inv ps s Figure 13 Running Isabelle and selecting Isabelle perspective 5 If Isabelle is not already running press the button labelled a in Figure This will run the most recent Isabelle configuration defined in Section 3 20 D33 2a Theorem Proving User Manual Public COMPASS If a different configuration is required use the down arrow to select the required configuration If there is already an instance of Isabelle running an error message will appear as in Figure 14 This can be safely dismissed a00 Problem Occurred T Launching Isabelle CML has encountered a problem Only a single prover can be running at any time stop the running prover before launching a new one Details gt gt K Figure 14 Overview of Isabelle perspective in COMPASS Tool 6 To view or edit those theory files created in step 1 n
26. ry UserDwarf imports utp_cml Dwarf begin Auto generated THY file for user created proof Y E theorem nsa NeverShowAll mk_DwarfType amp stop Esto AO oops Y E theorem molc MaxOneLampChange mk_DwarfType amp s AO oops Y E theorem fstd ForbidStopToDrive mk_DwarfType astop A oops amp end Figure 18 Proof outline of unproved theorems Isabelle perspective As can be seen in the proof outline pane shown in more detail in Figure 20 each theorem now has a green tick signifying the theorem has been discharged Proof output is also shown in the output pane providing some details on the proof It is beyond the scope of this document to provide detailed descriptions of theorem proving using the Isabelle tool or to provide a tutorial on it s use We therefore 24 D33 2a Theorem Proving User Manual Public COMPASS 8 O O Isabelle Dwarf generated Isabelle Thu Aug 29 14 26 20 BST 2013 UserDwarf thy CML Compass Project Users nrjp6 Desktop COMPASS COMPASS app Contents MacOS workspace y AGS z t 0 Q y Q Quick Access ES cmL dh Isabelle PS Project Explorer 32 Im o Dwarf cml D UserDwarf thy 23 8 Dwarf thy m B Outline i gt m Er theory UserDwarf theory UserDwarf imports utp_cml Dwa v E Dwarf imports utp_cml Dwarf Auto generated THY file for user create Y E generated begin Y E theorem nsa NeverShowAll mk_Dwarf Y 5 Isabelle E by gt Thu
27. tions for installation of Isabelle for Linux are as follows 1 Download Isabelle for Linux distributed as a tar bundled archive 2 Unpack the archive into the suggested target directory 3 NOTE Do not launch the tool at this point 2 2 UTP CML Theories To prove theorems and lemmas for CML models Isabelle must have access to the UTP and CML Theories Instructions for obtaining these theories are given below for different platforms 2 2 1 Linux Mac OS X 1 Download the latest version of the utp isabelle x archive from https sourceforge net projects compassresearch files HOL UTP CML Linux Mac can choose either zip or tar bz2 2 Extract the downloaded theory package and save the utp isabelle directory to your machine for example home me Isabelle utp isabelle 0 x As the CML and UTP theories are improved new versions will be made available As new versions are uploaded follow the above steps to obtain and unpack the updates See Section 3 4 for details of setting up updated theories 2 2 2 Windows 1 Download the latest version of the utp isabelle x windows zip archive from https sourceforge net projects compassresearch files HOL UTP CML 2 Extract the downloaded theory package D33 2a Theorem Proving User Manual Public COMPASS 3 Copy the ROOTS file from the extracted folder to the Isabelle2013 applica tion folder e g C Program Files Isabelle20131 Windows will warn you a ROOTS file already ex
28. y file Dwarf thy are shown in the COMPASS tool The process detailed in Section 4 was used to gen erate the thy file The generated file 1s set as read only by the tool and therefore should not be edited The generated thy file uses a combination of regular Is abelle syntax which is described in various Isabelle manuals and tutorials and the Isabelle syntax defined for CML This Isabelle CML syntax is described in detail in FP13 80900 CML Dwarf Dwarf cml CML Compass Project e ES Jem 8 POG Resource Oc X 7 O 20 E B Y IO Dwarf cmi 38 8 Dwarf thy 53 tS CMLModel1 ig i types theory Dwarf ent LampId lt li gt lt L2 gt lt L3 gt imports utp cal Dwarf cml Signal set of Lampld E Y generated ProperState Signal indi Y gt Isabelle inv ps ps in set dark stop warning drive Y Tue Aug 20 text Auto generated THY file for Dwarf cml 8 Dwarf thy DwarfType lastproperstate ProperState 8 UserDwar set of LampId definition LampId lt parallel gt lt L1 gt lt L2 gt lt L3 gt lt parallel gt turnon set of LampId laststate Signal definition Signal lt parallel gt set of LampId lt parallel gt currentstate Signal desiredproperstate ProperState definition dark Signal inv d CCCd currentstate d turnoff union d turnon d desiredproperstate definition stop lt L1 gt lt L2 gt Signal Cd turno
29. ype warning Signal lt L1 gt lt L3 gt R drive Signal lt L2 gt lt L3 gt by intro classes metis full types Abs DwarfType Tag cases singleton iff functions E a a o 9 Error Log i Problems 8 Tasks E console 0 items Description 4 Resource Path Location Type Writable Insert 12 48 Figure 15 Example Dwarf CML model and generated thy file http isabelle in tum de documentation html http isabelle in tum de documentation html ZZ D33 2a Theorem Proving User Manual Public COMPASS In the corresponding generated timestamped Isabelle directory a user editable thy file 1s produced in this example that file is named Dwarf_User thy This file imports the utp_cml theory and the generated Dwarf model theory This file is shown in Figure 16 gt Dwarf cml Dwarf thy UserDwarf thy 23 m theory UserDwart imports utp cml Dwarf begin text Auto generated THY file for user created proof with Dwarf thy Figure 16 Initial user editable Dwarf_User thy file Switching to the Isabelle perspective and running the Isabelle configuration we may start stating and proving theorems and lemmas In Figure we begin to prove some of those theorems introduced in FP13 These theorems named nsa molc and fstd are added to the user editable theory file Dwarf_User thy The theorems use a combination of regular Isabelle syntax both using apply style scripts and the Isar syntax which is descr
Download Pdf Manuals
Related Search