Home

XEmacs Interactive Prover Interface for Atelier B

1. HIA TC POG nPO nun Pr BOC COMPONENT TOYFONROOOOOYFTOO NNOr NOOOOQMO GVOOOG 2 B1 Be Ll1 12 Ro Arithmetic_1 Arithmetic_2 ice ice ice ice ice ice Serv Serv Serv Sery Sery Sery 71 97 OK 277 OK OK 4 4 4 4 pop Fundamental PenDel L1 C1 All ri components list Mark set Figure 3 2 The pri component list buffer 8 XEmacs Interactive Prover Interface for Atelier B User Manual 3 3 Interactive proof 3 3 1 Toolbar This toolbar is available as soon as a component has been selected cf figure 3 4 page 12 It contains buttons related to prover commands and buffer access You must have installed the text mode Lisp package and have your XEmacs compiled with support for xpm Right to left the buttons displayed are e Exit End of interactive proof returns to component list e Disk Save current proof command sw e te Synonymous with te Try everywhere e Refresh Bring back the PRI gt prompt when in case it has been lost e Stop Command interrupt e Prev Go to the previous Proof Obligation pv Previous PO e Next Go to the next Proof Obligation ne Next e Back Synonymous with ba Back e Step Synonymous with st Step e dd Synonymous with dd Deduction e ddo Synonymous with dd 0 Deduction force O o mp Synony
2. 4158 amp CoeffA 4158 amp VitMaxRecul 28 VitMaxJog 55 amp VitMaxCreep 100 amp VitMaxRM 100 amp VitMax4 0 amp VitMax3 499 amp VitMax2 360 amp VitMax1 499 amp MaxValiditeModif 961 amp Six 6 amp Cin 5 amp Quatre 4 amp O lt PosBlocInvar amp PosBlocInvar lt 1000 amp O lt 1 DernVarLoc 8 1 lt DernVarLoc DernVarLoc lt 21 amp O lt Station_VarNorm amp Station VarNorm lt 21 amp VariantSecu 0 21 gt BOOL amp dom VariantSecu 0 21 amp SorMsgSecu_i Initialisation 1 Check preconditions of called operation or While loop construction or Assert predicates a z m 4 H J al a y a mM mM z z mM z a 4 a a a a a Mm J l A XEmacs pri hypothesis PRI PenDel Font 11413 C1 Bot Figure 3 6 The pri hypothesis list buffer 16 XEmacs Interactive Prover Interface for Atelier B User Manual e Show This menu allows to show commands Show All Show all commands Show Entry Show the current selection Show Branches Show hidden branches of the selection Show Children Show hidden branches of the next level only Show Subtree Show all hidden branches of the current selection e Hide This menu allows to hide commands Hide Leaves This entry is a predefined XEmacs menu entry This item is not used by EmacsP RI Hide Body This entry i
3. The project list is displayed in the pri projects list buffer cf figure 3 1 page 6 To open a project just click with the middle button on the name of the project To exit you can use either e the Exit button of the toolbar e or the File gt Exit XEmacs menu entry e or the C x C c keyboard shortcut 3 2 Select a component Once a project is selected its status is displayed in the pri components list buffer cf figure 3 2 page 7 To start the interactive proof of a component just click with the middle button on the proof percentage of that component Completely proved components can not be opened if proved proof obligations are not displayed cf paragraph 8 3 3 To go back to the project list use either e the Exit button of the toolbar e or the File gt Exit XEmacs menu entry e or the C x C c keyboard shortcut XEmacs Interactive Prover Interface for Atelier B User Manual Lucid pri p PROJECT PAI4 PROJECT PAI MCS PROJECT enacspri Figure 3 1 The pri project list buffer USE lemac pri compone Lucid Cs xEmacs a 0 4 Emerald laris xemacs 2 SO fer Cd SV s binaries a E L Y E i i i 3 H 1 1 1 I 1 1 I 1 1 1 1 1 I 1 I 1 I 1 1 1 1 1 I 1 1 I 1 1 1 I 1 1 I 1 1 1 1 1 1 1 1 1 I 1 1 1 1 I 1 I 1 1 1 1 1 I 1 I 1 1 I 1 I Ez Ada C
4. binaries linux glibc bin xemacs 20 4 Emerald XEmacs Luc 27818218 26112 0 8 This is a customization buffer for group Pri Type RET or click button2 on an active field to invoke its action Invoke Help for more information Operate on everything in this buffer Set Save Reset 7 Done Pri group State visible group members are all at standard settings Interactive Proof Mode Show Proved Pos 7 Toggle off nil State this option is unchanged from its standard setting Non nil means show proved prooved obligations Inhibit Toolbar Y Toggle off nil State this option is unchanged from its standard setting Non nil means don t use the specialized Emacspri toolbar Hypothesis Buffer Toggle on non nil State this option is unchanged from its standard setting Non nil means use the hypothesis buffer Trace Y Toggle off nil State this option is unchanged from its standard setting Non nil means use trace in the scratch buffer Pri group end XEmacs Customize Group Figure 3 3 The customize buffer 3 3 4 Interactive Proof Buffers Proof Obligation List buffer pri po list This buffer contains the list of the unproved PO of the selected component cf fig ure page 12 The default behaviour is that only unproved PO are displayed To also display proved PO you have to customize the interface with PRI gt Customize cf paragraph 3 3 3 To go on a partic
5. Etat4 amp not ValEtat Local_EtatModeConduite EtatO amp not ValEtat Local_EtatModeConduite Etat2 amp not valEtat Local EtatModeConduite Etat1 amp ValEtatv Local EtatModeConduite Etat3 amp not PrecModeConduite 1 ValEtat Etat3 amp Check that the invariant ChgMode ChgMode 1 is preserved by the operation ref 4 4 5 57 amp gt pre _EtatModeConduite PrecModeConduite 1 13Un 34P0 Unproved ClMode_1 VerifChangeMode 14 PenDel Font L50 C1 Bot Figure 3 5 The pri log buffer Current proof tree buffer pri proof tree This buffer contains the current proof tree cf figure page 17 By default only unterminated branches are displayed Once a branch is completed it is automatically hidden except the first command which is abbreviated and completed with an ellipsis This buffer is equipped with the following scrolldown menu e Headings This menu allow to navigate into the proof tree Heading corresponds to a proof command Go up Next Go to the next command Previous Go to the previous command Next Same Level Go to the next command at the same level Previous Same Level Go to the previous command at the same level USE 15 emacs binaries linu File Edit Apps Options Buffers Tools op Ei Dons sels eles STE BYTrC 24331 amp BYTrB 25641 amp BYTrA 24331 amp CoeffD 4158 amp CoeffC 4158 amp CoeffB
6. frame This buffer contains the EmacsPRI version number the directory version number and options of the underlying Atelier B used host name Example EMACSPRI version V1 7 4 ATELIERB Directory beta 3 7Beta4 AB bbin Version 3 7 Option extra large HOST cubitus e Save Synonymous with sw Save e Customize Open the Interface Customize buffer Customize Group Prix cf figure page 11 This buffer contains editable fields allowing to modify the behaviour and the apparence of the interface The first line is composed of the name of the variable and of the possible values for that variable The Toggle button modifies the value of the variable switch between off and on selection with middle button The second line shows the current value of this variable The third line gives a short description of the use of that variable After having modified some variable click on the set button to apply your changes The save button saves the value of that variable in your emacs file Variables that can be customized are Show Proved Pos Indicates whether Proved PO should be displayed Inhibit Toolbar Indicates whether the toolbar should be displayed Hypothesis Buffer Indicates whether the hypothesis stack should be dis played Trace Indicates whether traces should be displayed in the scratch buffer e Exit C x C c Exit Interactive Proof Mode USE 11 emacs
7. Atelier B XEmacs Interactive Prover Interface for Atelier B User Manual version V1 7 4 CEN XS CLEARS Y SYSTEM ENGINEERING ATELIER B XEmacs Interactive Prover Interface for Atelier B User Manual version V1 7 4 Document made by CLEARSY This document is the property of CLEARSY and shall not be copied duplicated or distributed partially or totally without prior written consent All products names are trademarks of their respective authors CLEARSY Maintenance ATELIER B Parc de la Duranne 320 avenue Archimede Les Pl iades II Bat A 13857 Aix en Provence Cedex 3 France Tel 33 0 4 42 37 12 70 Fax 33 0 4 42 37 12 71 mail contact atelierb eu Contents 1 Introduction 2 Installation en Se 3 Use 3 1 Select a project 3 2 Select a component SETTET 3 3 1 Toolbar E A 3 3 4 Interactive Proof Buffers 4 EmacsPRI is free software 10 11 19 List of Figures NE EEE Gwe ee 6 EE 7 Je SG 11 Nr NER 12 e e 14 O ds EEEE 15 ee a o EN iz EE eee ee 17 Chapter 1 Introduction XEmacs Interactive Prover Interface EmacsPRI can be used with Atelier B 3 6 and 3 7 XEmacs v20 4 or v21 1 is required As Atelier B it works on Solaris or Linux systems The following XEmacs packages are required base and efs XEmacs text modes package is required for the EmacsPRI toolbar If this package is not installed EmacsPRI works without toolbar XEmacs for
8. Solaris can be downloaded from this internet site e http sunfreeware com XEmacs Interactive Prover Interface for Atelier B User Manual Chapter 2 Installation This interface should be installed by each user in the emacs directory of his own account Thus each user can modify Lisp source code and adapt the interface to his needs Lisp source code represents about 400 Kb 2 1 General Installation go into emacs directory copy the EMACSPRI V1 7 4 tar Z file in emacs directory type in the following command zcat EMACSPRI V1 7 4 tar Z tar xpf edit the emacs EMACSPRI emacspri file set the following variables ATELIERB DIR should contain the full path to the directory that contains the startBB file without the final Ex home atelierb AB bbin for home atelierb AB bbin startBB ATELIERB VERSION should contain the release of the Atelier B used 3 6 or 3 7 particular resource must be set for EmacsPRI to work correctly The resource and its value are ATB BATCH Print Messages For Emacs TRUE This resource can be set for instance in the user resource file AtelierB You just need to add the line above to the latter file XEmacs Interactive Prover Interface for Atelier B User Manual Chapter 3 Use Once installation is done type in emacs EMACSPRI emacspri The buffer which is displayed at startup then contains the project list 3 1 Select a project
9. ion Expr pri_varN e se Suggest For Exist e st End Step to End e re Reset e ap Arithmetic Proof e ct Contradiction e cts Special Contradiction e tp Hyp Proof by attempts based on hypothesis e tp Goal Proof by attempts based on goal USE 13 e ah amp pr e ah amp mp e ah amp pp rp 0 e mh amp pr e mh amp mp e dc amp pr e dc amp mp e dd amp eh e dd amp mh e ba amp dd Selecting one of these items executes the associated command s To execute ah eh sh dc dcs mh ae or se commands the user should first select an expression in the buffer with the left button then select the command to execute with the right button The last entries execute two commands at once To execute some of these commands the user should first select an expression or an hypothesis in the buffer Hypotheses stack buffer pri hypothesis This buffer is not displayed by default To display it you have to customize the interface with PRI gt Customize menu cf paragraph 3 3 3 This buffer contains the hypothesis stack cf figure 3 6 page 15 Each hypothesis is equipped with a square button A left click on one hypothesis selects it An other click deselects it A pop up menu can be displayed with the right button It contains the following items e ah Add hypothesis e fh False hypothesis eh Goal Use Equality in Hypothesis in Goal eh AllHyp Use Equality in Hypothesi
10. is free software It is distributed by ClearSy It is an experimental version so it is distributed without any warranty Lisp source code is distributed with the interface You can modify source code for your own use but you can t modify it to commercialize it ClearSy can help you to realise modifications ClearSy is interested in significant functional development you can make on this interface ClearSy can possibly integrate it into future versions ClearSy makes available new versions of this interface on its internet site http www atelierb societe com emacspri emacspri uk html 19
11. mous with mp Mini Proof e PP Synonymous with pp Predicate Prover e pp Synonymous with pp rp 0 Reduced Predicate Prover o pr Synonymous with pr Prove USE 9 ess Synonymous with ss Simplify Set e ddi Synonymous with dd 1 Deduction force 1 e dd2 Synonymous with dd 2 Deduction force 2 e Old Proof Display the buffer containing the old proof tree pri old proof in a new frame e Proof Tree Display the buffer containing the current proof tree pri proof tree in a new frame e Hyp Display the buffer containing the hypothesis stack pri hypothesis list in a new frame e Term Display the pri log buffer the one in which interactive proof is conducted in a new frame e Goal Synonymous with cg Current Goal e PO List Display the buffer containing the Proof Obligation list pri po list in a new frame 3 3 2 Status line The Term and PO list buffers contain at their bottom a status line cf figure 8 4Jpage 12 showing 1 Number of proved PO 2 Total number of PO 3 Status Proved Unproved of the current PO 4 Current component 5 Current operation 6 Current PO The displayed format is 1Un 2PO 3 4 5 6 ex 3Un 15PO Unproved composant1 op1 1 10 XEmacs Interactive Prover Interface for Atelier B User Manual 3 3 3 PRI menu It contains the following items e About Emacspri Horizontally split the current window and open a new buffer xAbout Emacspri in the bottom
12. s a predefined XEmacs menu entry This item is not used by EmacsP RI Hide Entry This entry is a predefined XEmacs menu netry This item is not used by EmacsP RI Hide Subtree Hide the commands below the current command Hide Others Hide all the commands except the current command and upper level commands Hide Sublevels Hide lower level commands pop up menu can be displayed with the right button It contains the following items e ba Back e st Step e st End Step to End e re Reset e Proof Paste For the Proof Paste menu entry a portion of the proof tree should be first selected Then this command executes the list of selected commands USE 17 lemacs binaries linux glibc bin xemacs 20 4 Emere IF File Edit Apps Options Buffers Tools IT EO JOGA se jeje Borce 0 amp PS dd amp Next inaries linux glibc bin xema File Edit Apps Options Buffers Tools T Force 0 amp dd amp ah Local EtatModeConduite ValEtat Etat3 amp ah valEtatv Local EtatModeConduite Etat3 amp Figure 3 8 The pri old proof tree buffer Old proof tree buffer pri old proof This buffer contains the old proof tree cf figure 3 8 page 17 The pop up menu is the same as in the current proof tree buffer pri proof tree 18 XEmacs Interactive Prover Interface for Atelier B User Manual Chapter 4 EmacsP RI is free software This interface
13. s in All Hypothesis e sh Search Hypothesis e mh Modus Ponens Selecting one ot these items executes the associated command in relation with the selected hypotheses To execute a sh command on an expression this expression should first be selected in the buffer with the left button then the sh command is executed with the right button 14 XEmacs Interactive Prover Interface for Atelier B User Manual El emacs binaries linux glibe bin xemacs 20 4 Emerald XEmacs Lucid pri log File Edit Apps Options Buffers Tools To Ae Det ada ISIS ValEtatv Local EtatModeConduite Etat4 gt Local EtatModeConduite ValEtat Etat4 Local EtatModeConduite ValEtat Etat4 gt ValEtatv Local EtatModeConduite Etat4 ValEtatv Local EtatModeConduite Etat3 gt Local EtatModeConduite ValEtat Etat3 Local EtatModeConduite ValEtat Etat3 gt ValEtatv Local EtatModeConduite Etat3 ValEtatv Local EtatModeConduite Etat1 gt Local EtatModeConduite ValEtat Etat1 Local EtatModeConduite WalEtat Etat1 gt ValEtatv Local EtatModeConduite Etat1 ValEtatv Local EtatModeConduite Etat2 gt Local EtatModeConduite ValEtat Etat2 Local EtatModeConduite ValEtat Etat2 gt ValEtatv Local EtatModeConduite Etat2 ValEtatv Local EtatModeConduite EtatO gt Local EtatModeConduite ValEtat EtatO Local EtatModeConduite ValEtat Etat0 gt ValEtatv Local EtatModeConduite Etato not ValEtat Local_EtatModeConduite
14. ular PO click middle button on the name of the PO the pri log buffer is then displayed Proof Terminal buffer pri log This buffer contains traces of past commands as well as the current goal cf figure page 14 using the format cmd lt command name gt lt prover messages gt goal lt current goal gt green underlined message PO Proved is displayed when the current PO has just been proved This buffer can t be edited The mini buffer at the bottom of the XEmacs window allows to type in commands when the PRI gt prompt is displayed Keyboard arrows up and down allow to browse the command history pop up menu can be displayed by a right click It contains the following items XEmacs Interactive Prover Interface for Atelier B User Manual emacs binaries linux A 20 4 Emerald XEmacs Lucid pri po list File Edit Apps Options Buffers Tools Top OREA ea aa Initialisation VerifChangeMode P01 unproved P03 unproved POS unproved PO unproved P09 unproved P011 unproved P012 unproved P013 unproved P014 unproved P019 unproved P020 unproved XEMacs pri po li 13Un 34P0 Unproved ClMode i VerifChangeMode O PenDel gt L14 C1 Al1 Figure 3 4 The pri po list buffer e ah Add hypothesis e eh Goal Use Equality in Hypothesis in Goal e sh Search Hypothesis e dc Do Case e dcs Do Case Special e fh False hypothesis e mh Modus Ponens e ae Abstract Express

XEmacs Interactive Prover Interface for Atelier B

Contents

Download Pdf Manuals

Related Search

Related Contents