Home

Prouveur interactif - Manuel Utilisateur

image

Contents

1. GOAL max 0 vv aa EN LA PHASE DE MISE AU POINT 35 3 Utiliser les fonctions de recherche du prouveur interactif Penser en parti culier la fonction rp ReducedPO qui permet de ne visualiser que les hypoth ses ayant une variable en commun avec le but Dans l exemple pr c dent nous devons d montrer que max 0 vv aa est un naturel ce qui est toujours vrai mais il est quand m me souhaitable de contr ler la d finition de aa et vv En tapant rp dans la zone de commandes nous obtenons PRI gt rp Reducing hypothesis of lemma 1 inclusion iteration s Goal max 0 vv aa N Hypothesis 1 pass es of inclusion by common symbols from goal vu N A a EN gt aaeN A aa lt 2147483647 A 0 lt 2147483647 aa 2147483647 lt aa A aa lt amaz End of reduced PO PRI gt Cette fois les deux premi res hypotheses d finissent vv comme un entier naturel et aa comme un entier relatif cette derni re forme tant une normalisation du prouveur Le lemme est donc juste la fonction sh SearchHypothesis qui permet de rechercher des hypoth ses Vous pouvez utiliser cette commande en mode simple par exemple sh card EE renvoie toutes les hypoth ses qui contiennent card E E Dans notre exemple nous pourrions rechercher les hy poth ses qui concernent vv sh vv puis celles qui conc
2. Les buts non d coup s ce sont des buts qui mettent en chec l algorithme de d coupage du g n rateur d obligations de preuve Nous allons tudier ces trois cat gories Dans les exemples qui illustrent la suite nous n utiliserons plus la Deduction dd pour faire monter les hypoth ses locales mais la com mande pr Red qui lance le c ur de preuve en mode r duit En preuve interactive on utilise pr Red d s qu il faut faire avancer une d monstration sans la terminer ou charger des hypoth ses pour des raisons que nous verrons longuement dans le chapitre 6 5 7 1 Les buts existentiels particularisables Montrons cette cat gorie sur des exemples Exemple 1 une valeur triviale trouver Soient les composants suivants MACHINE ComplexGoall ABSTRACT_CONSTANTS cc IMPLEMENTATION PROPERTIES ComplexGoall_1 cc E 1 3 NAT A REFINES Vxx xx ran cc gt xx mod 2 0 A ComplexGoall Vxx xx ran cc gt xx mod 3 0 A END Vxx xx ran cc gt xxmod5 0 A Vxx xx ran cc xx mod 7 0 END Ce composant n a artificiellement aucune op ration mais il repr sente le cas r el o une constante abstraite est utilis e pour sp cifier le logiciel sans servir l implantation Nous avons une obligation de preuve pour l implantation dont le but est Jec ccE1 3 NAT A Vxx xx ran cc gt x mod2 0 A Vax xx ran cc gt xxmod3 0 Vxx xx ran cc
3. 1 1 il y a donc un autre but d montrer apr s tablissant que l expression initiale est sup rieure 1 Nous supposons que le prouveur ne contient aucune r gle sur les restes de divisions enti res par exemple nous l avons constat par examen de la base de r gle avec la commande SearchRule sr Il y a donc une connaissance math matique amener dont les deux parties de la preuve devraient b n ficier C est pourquoi il est pr f rable de revenir au d but de la d monstration avant de proc der a cet ajout de connaissance ce que nous faisons par la commande Reset re Les r gles minimales priori suffisantes pour faire cette d monstration sont les suivantes 144 Prouveur interactif Manuel Utilisateur THEORY IntDiv IS b a b a a mod b a NATURAL amp b NATURAL amp not b 0 gt a mod b 0 b 1 a NATURAL amp b lt 0 amp not b 0 gt a mod b 0 1 b a lt 0 amp b NATURAL amp not b 0 gt a mod b 1 b 0 a lt 0 amp b lt 0 amp not b 0 gt a mod b b 1 0 END Nous avons pr sent ces r gles en langage de th orie dans le format qui permet de les crire dans un fichier composant pmm Ce format n cessite quelques commentaires Pour indiquer qu une variable doit tre un entier positif nous crivons a N plut t que a Z A 0 lt acar N fait partie des symboles de ba
4. 1 d o Vabsence de simplification Sans chercher analyser plus avant nous nous doutons que le passage au prouveur de pr dicats d un tel but provoquera sa simplification lors de l analyse plus compl te qui permet la transform e en pr dicats quantifi s Il y a peut tre beaucoup d hypoth ses dans ce cas la commande pp peut tre longue car toutes les hypoth ses doivent tre traduites Aucune hypoth se n est n cessaire pour d montrer ce but nous pouvons donc utiliser pp rp 0 PRI gt pp rp 0 Starting Prover Predicate Call Proved by the Predicate Prover Current PO is Initialisation 2 Proved saved Unproved Goal Check that the invariant gt card EE cc card EE End La d monstration est finie la zone du but devient verte et l tat courant est Proved 6 2 5 La protection des regles manuelles Puisque le prouveur de pr dicats est bien adapt a la preuve de regles il est naturel de Vemployer pour d montrer les r gles manuelles que l op rateur ajoute Ceci a t implant par la commande Validation of Rule vr qui permet de d montrer une r gle l aide du prouveur de pr dicat Si l op rateur n ajoute que ce type de r gles ma nuelles la preuve est valide sans v rifications suppl mentaires Nous allons voir l utilisation de ce principe sur un exemple Soit d montrer le lemme suivant 22 20 30 gt 22 1 2 V 22 20 30 V 22 300 400 Bien
5. Unproved PO D521 47483647 EE 5 asie alo ilote 1 amp Local hypo heses A r Y pilote gt Rec that the invariant vv IN is preserved by the operation ref 3 4 PO1 Unproved PO2 Proved End Y 15 L fal basic_train pilote 1 GOAL Current Goal CA max 0 vv aa E N Y P01 Unproved mae aa Ena P02 Proved co ah e N pom gt m gt go pilote 1 Current 5 is pilote 1 Unproved saved Unproved Goal SLocal hypotheses A q iS dus LE Peake that the invariant HE N is preserved by the operation ref Next Goto Math D ait Demo max 0 H aa N End PRI gt dd Current State of PO Unproved saved Unproved Starting Deduction Current PO is pilote A Co Hi ted Next Unprove saved Unprove max 0 ij aa je N Force 0 A N dd PRI gt r Next EA hypothesis of lemma 1 inclusion iteration s x 0 H aa N Hypothesis 1 lotes of inclusion by common symbols from goal me N aaE NA aas2147483647 A Force 0 0 lt 2147483647 aa 2147483647 lt aa A aa lt amax End of reduced PO PRI gt 5 3 Le parcours des obligations de preuve Le bon choix de l ordre de lecture des obligations de preuve sert se diriger en premier vers celles qui ont le plus de chances d tre fausses Leur correction pr coce vite d avoir a rev rifier les obligations de preuves justes priori apr s modification du composant Un mauvais choix de parcours de
6. 1Les parenth ses dans une formule sont uniquement des modificateurs d associativit on consid re par exemple qu il n y a aucune diff rence entre 3 3 x 6 et 3 3 x 6 66 Prouveur interactif Manuel Utilisateur la b A b gt a A gt bool a bool b car le but coincide avec le gabarit bool a bool b avec le filtre suivant a xx 2 lt 10 b xx lt 12 Ce gabarit bool a bool b plac apr s le symbole implique est appel cons quent de la r gle tandis que a gt b et b a sont les ant c dents L application de cette r gle provoque le d chargement du but initial et l apparition des sous buts suivant a b qui devient xx 2 lt 10 xx lt 12 b gt a qui devient xx lt 12 gt xx 2 lt 10 Certaines r gles n ont pas d ant c dent dans ce cas le symbole implique est omis par exemple 2x x BOOL Ces r gles sont appel es r gles feuilles ou terminales car elles liminent un but sans en produire de nouveau Une preuve aboutit quand tous les buts ont disparu par l action de r gles feuilles Notion de r criture Une r gle dont le cons quent est de la forme F est une r criture elle ne fonctionne pas comme une r gle normale Elle s applique s il existe une sous formule dans le but qui coincide avec le gabarit E le nouveau but est alors obtenu par remplacement de E par F Par exemple la r gle transforme le but uu uu
7. Atelier B sont les suivants Employer la force 0 ne jamais examiner une obligation de preuve avant d avoir tent de la d montrer avec le prouveur automatique en force 0 Occuper les ordinateurs si vous disposez d ordinateurs inemploy s sur lesquels l Atelier B est install il est toujours utile de lancer le prouveur automatique en force 1 2 ou 3 sur ceux ci pour d montrer des obligations de preuve justes de votre projet Ne pas attendre n attendez pas que le prouveur automatique en force 1 et ou 3 termine le traitement de votre projet pour commencer les phases de mise au point ou de preuve formelle Le prouveur automatique est aussi employ en preuve interactive Ceci peut sembler paradoxal mais ce que nous appelons preuve interactive est en fait une preuve semi automatique dans laquelle les actions de l op rateur s intercalent entre des appels au coeur de preuve Il faut donc choisir la force utilis e galement en preuve interactive elle condi tionne toutes les interventions du coeur de preuve dans les d monstrations manuelles Dans la majorit des cas il est conseill d employer la force 0 la force 1 est parfois utilis e aussi Nous verrons ceci en d tail dans le chapitre 6 4 3 Les lemmes de bonne d finition Il est possible d crire des expressions qui ressemblent des expressions math matiques mais qui n ont pas de sens par exemple max Nous utilisons tort l op
8. Les tactiques simples de preuve 60 Prouveur interactif Manuel Utilisateur Utilisation avanc e du prouveur Les recettes de preuve on y trouve en particulier le tableau des commandes choisir en fonction de chaque type de situation Les pi ges viter ce paragraphe est lire imp rativement avant une utilisation in tensive du prouveur 6 2 Introduction la preuve interactive Cette partie est destin e aux utilisateurs s initiant la preuve interactive avec l Atelier B mais qui connaissent le langage B les principes math matiques de preuve et les notations utilis es dans les obligations de preuve Les notions pr sent es sont les suivantes Les commandes du prouveur interactif Le langage des r gles Le prouveur de pr dicats 6 2 1 Les commandes du prouveur interactif Les explications qui suivent ne remplacent pas le manuel de r f rence du prouveur inter actif en particulier la syntaxe pr cise de chaque commande n est pas d crite Dans ce paragraphe nous cherchons donner les indications n cessaires pour penser utiliser la bonne commande au bon moment Si vous ne connaissez pas les commandes du prouveur interactif la lecture du pr sent paragraphe vous est recommand e Nous avons class les commandes dans diff rentes rubriques class es par ordre d impor tance pour une bonne utilisation du prouveur Ces rubriques sont les commandes de d pla
9. choisir en fonction de type de situation Il faut parfois refaire passer des hypoth ses dans le prouveur pour orienter le prouveur sur elles En particulier des galit s apparues en hypoth se peuvent n cessiter cette op ration pour tre prises en 59 56 Prouveur interactif Manuel Utilisateur compte Pour mettre une hypoth se dans la forme exacte qui lui permettra de coincider avec quelque chose utiliser AddHypothesis Utiliser AddHypothesis plut t qu une r gle par l avant Utiliser AddHypothesis pour produire des expressions avec les bonnes parenth ses Contr ler le nombre de cas de la preuve en utilisant pr Red plut t que pr Ne pas d truire de regle manuelle si cela peut introduire un d calage dans les num ros de r gles Il faut sauvegarder la d monstration avant de changer de force en cours de preuve interactive 6 1 M thode g n rale La phase de preuve formelle consiste d montrer avec le prouveur interactif les obliga tions de preuve qui restent apr s la phase de mise au point voir paragraphe 5 Pour tre efficace dans ces preuves interactives il faut tirer le meilleur parti possible des tactiques automatiques de preuve c est dire utiliser autant que possible les appels au prou veur Ces appels se font par la commande Prove pr qui lance le c ur de preuve dans la force courante dans certains cas on essaie galement la commande PredicateProver pp qui peut aussi d charger autom
10. r yy yy lt 5 gt lt Tout ile a xx lt 5 co ncide avec x lt z x et z s instancient sur xx et sur 5 Puis la recherche de xx lt y se fait en remontant dans les hypoth ses celles ci sont yy lt 5 et xx lt yy La coincidence se produit alors pour xx lt yy en instanciant y sur yy la garde est VRAIE Le but yy lt 5 est alors produit Attention la recherche d une hypoth se s arr te la premi re coincidence Si le lemme est res yy A re lt uu A yy lt 9 gt xx lt 5 La r gle s applique toujours mais c est le but uu lt 5 qui est produit Celui ci ne permet pas la preuve d aboutir band il s agit d un conjoncteur de gardes band g1 g2 provoque l ex cution de la garde gi pour tout les cas possibles tant que ga n est pas v rifi e Par exemple la r gle band binhyp x lt y binhyp y lt z gt L lt z S applique a l exemple suivant res yy A rx lt uu yy lt 9 gt lt Tout dde a xx lt 5 co ncide avec x lt z x et z s instancient sur xx et sur 5 Puis la recherche de zx lt y se fait en remontant dans les hypoth ses la co ncidence se produit pour zx lt uu en instanciant y sur uu le premier binhyp est VRAI Mais il n y a aucune hypoth se uu lt 5 qui permettrait le succ s du deuxi me binhyp Par l action de band le parcours en remontant du premier binhyp se poursuit la co ncidence a alors lieu sur zx lt yy qui permet le succ s btest
11. PRI gt pc Loading theory func Loading theory simpl On v rifie que cette r gle est bien charg e en m moire PRI gt sr simpl a Searching in simpl rules with filter consequent should contain a Starting search Rule list is simpl 1 Backward f A gt B amp b A gt B gt f lt b A gt B End of rule list La r gle simpl 1 peut maintenant tre utilis e notamment au sein d un appel tendu au prouveur automatique Dans ce cas particulier la th orie simpl va tre utilis e en compl ment des r gles et m canismes natifs du prouveur Le mode trace du prouveur est utilis afin de visualiser l action de la r gle simpl 1 PRI gt pr Tac simpl Ru Goal None INDICATIONS UTILES POUR LA PREUVE 133 Starting Trace in mode Ru Goal None NoFile NoSimpl Starting Prover Call After deduction goal is now tab 1 lt 01 gt 0 lt 11 gt 1 lt 21 gt 1 lt 31 gt 0 lt 41 gt 1 lt 5 gt 0 lt 6 gt 1 lt 7 gt 0 0 7 gt 0301 By applying atomic rule simpl 1 f A gt B amp b A gt B gt f lt b A gt B the goal tab 1 lt 0 gt 0 lt 11 gt 1 lt 21 gt 1 lt 31 gt 0 lt 41 gt 1 lt 51 gt 0 lt 61 gt 1 lt 71 gt 0 0 7 gt 0 1 is now tab 1 lt 01 gt 0 lt 11 gt 1 lt 21 gt 1 lt 31 gt 0 lt 41 gt 1 lt 5 gt 0 lt 16 gt 1 0 7 gt 0 1 and 7 gt 0 0 7 gt 0 1 Le but va alors tre successivement
12. avoir une m thode d affichage rationnelle 78 Prouveur interactif Manuel Utilisateur ej StationUnix fork 6 INTE StationUnix fork 6 HYPOTHESIS 4 Font Mode lt Asdi Math Add Hyp my Global dom tident taches A banion 1 Unproved PO tporte taches gt PORTS A Situation don tport taches A hae cute aches teonnal t tt E pags tident tt A i or reconditions in is component 250 oenm sige i A tac PO4 Proved tconnait tt pgss dent ct A POS Proved o tonk oca otheses wee Unproved atte TACH HER A st gt ntte taches PO1 Proved tt DE taches tt A L make Provod SL that che inva StationUnix fork 6 GOAL LOS Proved ntte dom tport A Goal PO4 Proved gt monte donc tiden 3 Current Goal POS Proved AY tconnaitu ntt xtconnait tt ttso EOS ee Gen fpacet tident d Cnttetident Cet yCEESO 3 0s0 PO1 Proved DE SLA A PO2 Proved DE tte TACHES A PO3 Proved tte dom tp port A fi PO4 Proved tie domiti dew i a POS Proved iden ran tide Goa Es PO6 Proved Hide re ADR Check that tne eN tconnaite taches gt PASSWORDS y is preserved PO7 Proved tident taches pi 1D by ithe operation ref 3 ttjatconnaite taches tt lt gt PASSWORD ass IDENTITES amp P POL Proved tconnaitEftt rand Current PO 5411 1 PO2 Proved dom tiden amp taches Unproved saved Proved End ran tident c IDENTI
13. gt Pp binhyp C operation2 3 Y bcall WRITE bwritef A gt P END Ces r gles s appuient sur la pr sence d une hypoth se non math matique de la forme composant op ration num ro qui est syst matiquement rajout e par le prouveur lors du chargement d une obligation de preuve Cette hypoth se dite hypoth se de rep rage est d ailleurs affich e dans l interface La th orie d admission ci dessu admet toutes les PO de l op ration op rationl et la PO num ro 3 de op ration2 La directive binhyp du langage de th orie n autorise l application d une r gle que si la formule argument est trouv e dans les hypoth ses Cette th orie peut s utiliser sans avoir citer les num ros de r gles gr ce la commande ar Admis qui a pour effet d appliquer toutes les r gles de la th orie Admis tant que l une d elles s applique Attention aux d calages de num ros il est important de mettre les r gles d admission dans une th orie s par e Ainsi il sera possible de les retirer la fin sans que les autres r gles perdent leur num ro ce qui d truirait les d monstrations manuelles utilisant ces r gles En effet l utilisation d une r gle par une commande ApplyRule s effectue en d signant la r gle par son num ro d ordre dans sa th orie d appartenance Supprimer des r gles dans une th orie risque de d caler ces num ros voir paragraphe 6 8 2 6 6 3 Le d placemen
14. habitude il est possible de pressentir cette d monstration interactive tr s vite Malheureusement elle ne se g n ralise pas aux autres obligations non d montr es du composant 5 4 6 Admettre des obligations de preuve Il est possible d utiliser une r gle d admission voir cette notion en 6 6 2 pour admettre des obligations de preuve Cette m thode consiste faire agir une r gle manuelle d montrant artificiellement les obligations de preuve que l on ne veut pas voir Elle a deux avantages les obligations de preuve ainsi limin es sont r ellement marqu es comme prouv es la commande Next par exemple ne les atteint plus les forces sup rieures du prouveur pourront tre lanc es sur les obligations de preuve non cart es sans perdre de temps sur celles qui sont admises LA PHASE DE MISE AU POINT 45 Par contre l application de la r gle d admission est m moris e comme d monstration ma nuelle des obligations de preuve concern es ce qui peut tre g nant en cas de modification du composant En effet les obligations de preuve peuvent alors avoir chang et l appli cation de la r gle d admission fait croire a tort qu elles sont justes L utilisation d une r gle d admission n cessite une connaissance suffisante du prouveur interactif nous nous contentons ici de voir quel moment cette m thode s applique en phase de mise au point Pour apprendre utiliser les r gles d admiss
15. ouvrir les composants depuis l Atelier B il suffit d ouvrir la fen tre principale qui s est ic nifi e et de cliquer deux fois sur le composant Une fois que le sens du but est compris nous pouvons chercher pourquoi il doit tre vrai c est la justification intuitive LA PHASE DE MISE AU POINT 41 5 4 2 Conseils pour la justification intuitive Utiliser le sens physique raisonner partir de ce que repr sentent physiquement les quantit s et les expressions manipul es par exemple vv aa x tt correspond une nouvelle vitesse RESSOURCES xo est le nouvel ensemble de ressources disponibles Ce n est pas la preuve math matique qui est recherch e cette tape mais une bonne interpr tation du mod le abstrait Utiliser le raisonnement par cas et par contradiction tr s souvent on ne pense pas ces deux artifices dans des raisonnements naturels Ils s appliquent g n ralement bien quand la justification directe n aboutit pas Noter la justification intuitive Elle servira pour la d monstration intuitive Noter tr s rapidement au brouillon Exemple reprenons notre pr c dent exemple Pourquoi la fin de la boucle avons nous construit la valeur de pumpon pr vue dans la sp cification Simplement parce que chaque pompe a t contr l e utilisation du sens physique C est a dire que indice_I 7777 qui repr sente la valeur de l indice de boucle quand elle se termine doi
16. taille 1 1 A taille 1 2 A v1 1 ee A 7 ETUDES DE CAS 139 v2 1 ee v3 1 ee taille 1 3 A card ens U ee lt 3 A Check that the invariant ov 1 ov is preserved by the operation ref 8 gt bfalse A A Il y a deux m thodes pour charger ces hypoth ses la commande Deduction dd les hypoth ses sont alors directement charg es sans in tervention du prouveur En particulier le prouveur ne peut pas r duire les identifiants utilis s au minimum comme il le fait sur les autres hypoth ses la commande Prove pr les hypoth ses sont alors charg es par le prouveur qui enchaine sur la preuve Le but initial est donc transform Dans notre cas le but bfalse ne peut pas se transformer Nous pouvons donc charger les hypoth ses par la commande Prove en utilisant l option Red pour viter le d clenchement de preuves par cas intempestives PRI gt pr Red Starting Prover Call Le but devient bfalse L hypoth se contradictoire card ensU ee lt 3 c est transform e elle appara t maintenant sous deux formes diff rentes Sans m me chercher comprendre ces nouvelles formulations nous v rifions facilement qu elles sont toujours contradictoires si card ensU ee Il suffit alors d indiquer l une de ces formes au prouveur par la commande FalseHypothesis PRI gt fh 0 lt 2 card ens card ens ee Starting False Hypothesis Le but devien
17. une nouvelle expression est n cessaire ou si une hypoth se n est pas compl tement simplifi e Deduction dd cette commande permet de faire monter l hypoth se h si le but est de la forme h gt B sans passer par le c ur de preuve Penser Deduction quand le prouveur monte une hypoth se sous une forme normalis e peu avantageuse Par contre une hypoth se introduite de cette mani re n est pas trait e par certains m canismes du prouveur en particulier le simplificateur d galit s DoCases dc cette commande permet la preuve par cas L op rateur peut donner un pr dicat p en argument la preuve se fait alors dans les cas p et p ou bien il peut donner le nom d une variable v et un ensemble Y fini de petit cardinal la preuve se poursuit alors pour v tant chacun des l ments de E Dans ce dernier cas il faut d abord tablir v E Il y a beaucoup de d monstrations qui ne peuvent se faire que par cas ce que le prouveur ne d tecte pas toujours Penser DoCases si la d monstration intuitive se fait par cas SearchRule sr permet de rechercher une r gle dans la base de r gles du c ur de preuve Utiliser SearchRule avant de tenter d ajouter une r gle S il manque des hypoth ses pour appliquer la r gle trouv e utiliser ah plut t que d crire une r gle manuelle de remplacement ApplyRule ar cette commande permet l application d une r gle de la base du prouveur trouv e par
18. 1 2 3 les m canismes du c ur de preuve sont regroup s en ensembles compatibles qui sont les forces voir paragraphe 4 2 Plus la force est lev e plus la preuve est longue et risque de boucler mais plus elle est puissante La force 0 repr sente le meilleur compromis performance rapidit des diff rentes forces disponibles c est elle qu il faut utiliser en premier Ce que nous avons fait pr c demment c est le lancement du coeur de preuve en force 0 c est dire avec les m canismes de la force 0 sur chaque obligation de preuve Les d monstrations r ussies se r sument l application de r gles issues de la base de r gles choisies par les m canismes de la force 0 3 1 3 Le prouveur interactif Pour examiner l obligation de preuve restante nous allons maintenant entrer dans le prou veur interactif S lectionnez votre composant et choisissez comme indiqu ci dessous Atelier B composant Bo Prove d Ep Mitrei La fen tre principale de l Atelier B se range en ic ne tandis que la fen tre de situation globale du prouveur interactif appara t Cette mise en ic ne automatique de la fen tre principale est justifi e par importance de l activit de preuve dans un projet B l interface essaie de favoriser la concentration de l op rateur en pr sentant la preuve comme une activit pa
19. 51 gt 0 lt 61 gt 1 lt 71 gt 0 0 0 is now tab 1 lt 0 gt 0 lt 1 gt 1 lt 2 gt 1 lt 3 gt 0 lt 4 gt 1 lt 51 gt 0 lt 61 gt 1 0 0 La r gle s est bien appliqu e Le but est simplifi La preuve continue avec les applications successives de cette r gle the goal tab 1 lt 0 gt 0 lt 1 gt 1 lt 2 gt 1 lt 3 gt 0 lt 4 gt 1 lt 51 gt 0 lt 61 gt 1 0 0 is now tab 1 lt 0 gt 0 lt 11 gt 1 lt 21 gt 1 lt 31 gt 0 lt 41 gt 1 lt 51 gt 0 0 0 the goal tab i lt 01 gt 0 lt 11 gt 1 lt 21 gt 1 lt 81 gt 0 lt 41 gt 1 lt 51 gt 0 0 0 is now tab 1 lt 0 gt 0 lt 1 gt 1 lt 2 gt 1 lt 3 gt 0 lt 4 gt 1 0 the goal tab 1 lt 0 gt 0 lt 1 gt 1 lt 2 gt 1 lt 3 gt 0 lt 4 gt 1 0 tab 1 lt 0 gt 0 lt 1 gt 1 lt 2 gt 1 lt 3 gt 0 0 0 the goal tab 1 lt 0 gt 0 lt 1 gt 1 lt 2 gt 1 lt 3 gt 0 0 0 is now tab 1 lt 0 gt 0 lt 1 gt 1 lt 2 gt 1 0 0 the goal tab 1 lt 0 gt 0 lt 1 gt 1 lt 2 gt 1 0 0 is now tab 1 lt 0 gt 0 lt 11 gt 1 0 0 the goal tab 1 lt 0 gt 0 lt 1 gt 1 0 0 is now tab 1 lt 0 gt 0 0 0 0 O is now puis le dernier but est d montr par le prouveur natif Goal tab 1 lt 0 gt 0 0 O is discharged La d monstration est alors sauvega
20. Il pa End PRI gt pr Starting Prover Call Current PO is Initialisation 1 Unproved saved Unproved Goal 96 Prouveur interactif Manuel Utilisateur Il bE XX 3 gt xx End PRI gt pr Starting Prover Call Current PO is Initialisation 1 Unproved saved Unproved Goal XX 2 gt xx Il bE End PRI gt pr Starting Prover Call Current PO is Initialisation 1 Unproved saved Unproved Goal xx 1 gt xx Il pa End PRI gt pr Starting Prover Call Current PO is Initialisation 1 Proved saved Unproved Goal Local hypotheses amp xx 7 6 5 4 3 2 1 amp Check ref 3 3 gt xx 1 2 3 4 5 6 7 End Dans cet exemple nous avons utilis une seule commande de preuve DoCases pour d clencher une preuve avec plus de cas que ce qui est autoris en preuve automatique Les autres com mandes ne sont que des appels au coeur de preuve La preuve par cas est souvent utile d s que le lemme contient des ensembles num r s ou num rables ou des cas particuliers de valeur de variables 6 5 3 Recherche et application de r gles de la base La base de r gles de prouveur peut tre utilis e en interactif cela vite d ajouter des r gles dont la validit n est pas s re et qu il faudra d montrer apr s Quand le but courant semble pouvoir de simplifier par l action d une regle math matique simple on recherche la r gle correspondante par la commande SearchRule et on l applique pa
21. Le but de la d monstration intuitive est d viter de croire tort que certaines obligations de preuve sont justes suite a des confusions facilement faites dans une justification intuitive La m thode g n rale est la suivante transposer la justification intuitive en utilisant les hypoth ses s lectionn es voquer les r gles utilis es il ne s agit pas de se ramener des r gles existantes dans la base de r gles ou dans le B Book mais seulement de voir quelles sont les r gles qui sont implicitement utilis es dans la justification intuitive examiner ces r gles car c est au moment o la transformation utilis e a t sortie de son contexte en tant que r gle g n rale que l on voit toutes les conditions pour qu elle soit valide Exemple reprenons toujours l exemple pr c dent Les tapes de notre justification taient remplacer l indice par sa valeur la r gle utilis e est la d finition de l galit sans probl mes simplifier 0 1 NB_PUMP en 1 NB_PUMP r gles de calcul entier liminer la restriction 1 NB_PUMP nous avons une expression de la forme 1 NB_PUMP lt f f tant d fini par f TRUE gt l_wpok gt TRUE FALSE gt on 1 la r gle appliquer est clairement JE A B Aaf f LA PHASE DE MISE AU POINT 43 mais comment montrer que f est une fonction partant de 1 NB_PUMP II est n cessaire de faire deux cas on 1 TRUE ou
22. Le choix de la bonne commande pour faire progresser une preuve n est pas donn par des lois syst matiques sinon ces lois auraient t int gr es aux tactiques du c ur de preuve Nous devons donc nous contenter de donner des listes de commandes consid rer en fonction des diff rentes situations possibles C est l objet du tableau suivant En cours de preuve l op rateur pourra chercher identifier la situation courante dans la colonne de gauche puis essayer les commandes correspondantes recherche d une d monstration intuitive sh SearchHypothesis rp showReducedPo essayer en premier pr Prove pp PredicateProver surtout pour un but ensembliste ou fonctionnel expression clef manquante ah AddHypothesis eh useEqualityinHypo thesis repassage d hypoth ses dans le prou veur voir paragraphe 6 7 2 application de r gles de r criture la d monstration intuitive se fait par cas dc DoCases ce qu il faut faire s exprime par une r gle simple sr SearchRule vr Validation of Rule ar ApplyRule des hypoth ses devraient se simplifier entre elles refaire passer la conjonction de ces hypoth ses dans le prouveur voir paragraphe 6 7 2 but existentiel de la forme 2x P se SuggestforEzists hypoth ses contradictoires fh FalseHypothesis faire monter une hypoth se sans le c ur de preuve dd Deduction but de la forme
23. Manuel Utilisateur PRI gt pr Starting Prover Call Le but devient 2EN Il s agit bien de l ant c dant suivant de la deuxi me r gle de la th orie IntDiv Le simple fait de refaire passer l hypoth se clef dans le prouveur lui a permis de d montrer le but pr c dent Continuons PRI gt pr Starting Prover Call Le but devient Continuons PRI gt pr Starting Prover Call Le but devient ncl nc2 mod 2 0 2 1 gt ncl ncl nc2 2 nc2 ncl nc2 2 1 1 L ajout de l hypothese indiquant l intervalle de variation du reste est termin Il reste appliquer la r gle a b a a mod b apr s simplification du but PRI gt pr Red Starting Prover Call Le but devient 0 lt 1 nc1 nc2 2x nc1 nc2 2 puis PRI gt ar IntDiv 1 Goal Starting Apply Rule Le but devient 0 lt 1 nc1 ne2 ncl nc2 ncl nc2 mod 2 Nous pouvons tenter de d charger ce but PRI gt pr Starting Prover Call Le but devient nc1 nc1 nc2 2 nc2 nc1 nc2 2 lt 1 Le but qui appara t correspond la deuxi me borne de l intervalle nous le traitons de mani re analogue ETUDES DE CAS 153 PRI gt pr Red Starting Prover Call Le but devient 0 lt 1 nc1 nc2 2x ncl nc2 2 Puis PRI gt ar IntDiv 1 Goal Starting Apply Rule Le but devient 0 lt 1 ncl nc2 ncl nc2 ncl nc2 mod 2 Nous pouvons tenter la preuve de ce dernier sous but PRI gt pr Start
24. N A uu 0 0 en uu uu E N A wu 0 0 La sous formule uu 0 est localis e et transform e en uu 0 Chaque application d une r gle de r criture ne transforme qu une occurrence de la sous formule de gauche Ainsi aa bb transforme la formule aa aa 0 en aa bb 0 pour la premi re application de la r gle puis en bb bb 0 pour la deuxi me application nous ne pr ciserons pas pourquoi c est Poccurence de droite qui se transforme en premier cela nous m nerait trop loin Lors de l application d une r gle par ApplyRule une r gle de r criture se r applique toujours tant qu elle transforme quelque chose les modes Once et Multi ne s appliquent pas aux r critures Attention aux bouclages la r gle r x 0 LA PHASE DE PREUVE FORMELLE 67 provoque un bouclage Par exemple sur le but aa bb aa bb aa bb 0 aa bb 0 0 aa bb 0 0 0 etc Notons que cette r gle est d ailleurs fausse car x peut co ncider avec des expressions non num riques Notion de garde Il arrive souvent qu une r gle ait besoin de plus d information que ce que contient le but pour s appliquer Par exemple soit prouver re lt yy A yy lt 5 gt xx lt 5 Quelle r gle d inf rence permettrait de d charger ce lemme La r gle suivante ne convient pas LIYA y lt z gt BO En effet analysons comment elle s appliquerait le but xx lt 5 coincide ave
25. but courant Nous pourrions alors essayer pp mais l usage du prouveur de pr dicat se fait plus rarement au milieu d une preuve car il met une minute a chouer Nous faisons donc l tape 2 ba et pr Red Le but devient LA PHASE DE PREUVE FORMELLE 59 tconnait U ntt x tconnait tt ntt pass tident tt Nous sommes dans l tape 4 Comme le but s est nettement simplifi nous passons dans l tape 6 choix d une nouvelle commande Ici le nouveau but contient toujours des unions et des relations peut tre le prouveur de pr dicats le d montre t il La commande choisie est pp et le but devient tt 0 ntt gt tconnait U ntt x tconnait tt tt 0 pass tident 4 ntt gt tident tt tt 0 Nous sommes pass s dans le deuxi me cas qui se d montre pareillement nous verrons dans ce chapitre comment savoir dans quel cas on se trouve Nous refaisons les deux tapes pr c dentes la preuve aboutit L arbre de preuve est le suivant Force 0 amp pr Red dc tt 0 ntt amp pr Red amp pp amp pr Red amp pp amp Next Cet arbre est affich dans l une des zones de l interface MOTIF comme nous le verrons La preuve est termin e en six commandes Nous voyons sur cet exemple quel point il est possible de s appuyer sur pr et pp pour d bloquer une d monstration en utilisant Vorganigramme pr sent dans ce paragraphe Il faut de plus consid rer les points suiv
26. cc NATURAL End PRI gt pr Starting Prover Call Current PO is Initialisation 1 Unproved saved Unproved Goal cc mod 3 0 2 gt cc mod 3 0 100 End PRI gt pr Starting Prover Call Current PO is Initialisation 1 Proved saved Unproved Goal End La commande ApplyRule a t utilis e avec la syntaxe ar ModProps 1 0nce ce qui veut dire appliquer la r gle num ro 1 de la th orie ModProps une seule fois Once signifie une fois C est l utilisation la plus commune de la commande ApplyRule sauf pour les r gles de r criture o il faut employer ar Theorie numero Goal pour indiquer que la r criture doit se faire dans le but Pour plus d informations sur la commande ApplyRule voir le manuel de r f rence du prouveur 6 2 4 Le prouveur de pr dicats Le m canisme sur lequel est bas le prouveur principal de l Atelier B est l inf rence de r gles Autrement dit une d monstration ne peut aboutir que s il existe un encha nement de r gles qui fait dispara tre tous les buts Il n y a aucune garantie th orique de compl tude de plus l quilibre des r gles entre elles est obtenu par des r glages empiriques Il existe d autres m thodes de preuve L une de ces m thodes consiste ramener toute preuve dans le langage l mentaire des pr dicats quantifi s puis essayer diff rentes ins tanciations pour aboutir une preuve par contradiction Par exemple voici la d monstration dere An ACB xe
27. le menu de lancement du prouveur permet de choisir le mode de pilotage la fen tre de situation globale montre la liste des PO la fen tre de contr le permet d envoyer les commandes le prouveur interactif communique avec son interface en mode ligne utiliser les boutons de l interface est quivalent taper des commandes orienter la preuve sans ajout de connaissance non valid e une d monstration manuelle peut n employer que des r gles valid es les r gles manuelles sont des r gles non valid es 10 Prouveur interactif Manuel Utilisateur 3 1 Approche pratique 3 1 1 Un exemple Il faut tout d abord disposer d un projet prouver Vous pouvez prendre l exemple suivant MACHINE DemoExample VARIABLES few many INVARIANT few CNA many CNA few C many INITIALISATION few many 1 2 3 2 3 4 END Ce composant est volontairement faux l initialisation n tablit pas invariant parce que 1 2 3 n est pas inclu dans 2 3 4 Il produit donc une obligation de preuve fausse ce qui nous permet de trouver l erreur En effet il ne faut jamais oublier que la preuve sert trouver les erreurs dans les sources B Cet exemple nous permettra quand m me de faire une visite de l outil de preuve Rappelons galement que l activit de preuve ne sert qu a valider le logiciel d velopp avec la m thode B ce n est aucunement une activit de programmation Il nous para t utile d insister car l op ra
28. matique 2De plus le contr leur de types de l Atelier B attend des pr dicats quantifi s de la forme syntaxique Vu P gt Q o P est un pr dicat typant les variables introduites Prouveur interactif Manuel Utilisateur Chapitre 3 Introduction au prouveur Cette partie est destin e aux utilisateurs du langage B et de l Atelier connaissant les principes de la preuve mais n ayant pas encore utilis le prouveur de l Atelier B Il s agit d une visite guid e qui permet de savoir o sont les fonctionnalit s de preuve de Atelier B et o se trouve leur documentation R sum des notions principales la preuve sert trouver des erreurs prouver n est pas programmer la preuve peut tre partiellement automatique le prouveur ne sait pas d montrer qu une obligation est fausse la base de r gles est l ensemble des connaissances math matiques du prouveur les m canismes de preuve choisissent les r gles utiliser le c ur de preuve d signe la base et les m canismes les forces Rapide 0 1 2 3 regroupent les m canismes en niveaux une obligation de preuve poss de un tat Proved Unproved les commandes de preuve contr lent le prouveur en automatique comme en interactif une PO poss de un niveau de d monstration automatique une PO poss de une d monstration interactive le sch ma g n ral de l outil un c ur de preuve des commandes un pilote automatique ou interactif
29. monstration de l obli gation num ro 30 de l op ration Op toutes les PO non prouv es du composant Rap pelons que le nom de l op ration et le num ro de l obligation courante sont visibles dans les barres de titre des trois fen tres du prouveur et dans tous les messages de r ponse de la zone de commandes te dd pp Replace Gen Unproved essayer la d monstration consistant faire une d duction et lancer le prouveur de pr dicats sur toutes les PO non prouv es du composant Pour plus d informations sur la commande TryEverywhere voir le manuel de r f rence du prouveur 5 7 Les expressions complexes Dans certains cas le but tient sur plusieurs lignes et sa lecture directe n est pas possible Il faut alors commencer sa d monstration avec le prouveur interactif pour le d composer et le LA PHASE DE MISE AU POINT 49 rendre compr hensible La pr sence d un but complexe indique souvent qu il faut changer la forme des expressions du composant pour rendre la preuve plus simple en tous cas il faut quand m me analyser le but avant de faire des modifications Les buts complexes appartiennent g n ralement l une des trois cat gories suivantes Les buts existentiels particularisables le but est de la forme 2x P mais on peut trouver une valeur simple de x qui convient Les buts existentiels abstraits la valeur de x qui convient est unique et complexe g n ralement une fonction
30. montrer le sous but qui bloquait Il voit alors appara tre un nouveau but qui ne semble pas avoir de rapport avec le pr c dent c est normal puisqu il s agit du prochain sous but engendr par la commande pr Red initiale Mais si l op rateur n est pas accoutum suivre sa d monstration dans la ligne de commande il peut tre surpris Dans notre exemple l appel au coeur de preuve s est termin lors de l chec du premier sous but Peut tre suffit il de le relancer pour terminer la d monstration Force 0 amp pr Red ah not EE amp pr amp pr amp pr amp Next 6 5 Tactiques simples de preuve Parmi toutes les diverses strat gies que l op rateur utilise au cas par cas dans les d monstrations interactives il y a des groupes de commandes qui reviennent souvent ensemble L usage conjoint de ces commandes semble tre des sortes de tactiques l mentaires a partir des quelles les d monstrations complexes sont baties Nous avons identif quatre tactiques de base Prove et PredicateProver AddHypothesis et DoCases SearchRule et ApplyRule R gles manuelles et ApplyRule Aa N RA Ce d coupage est bien entendu assez subjectif Nous allons n anmoins pr senter ces quatre tactiques 6 5 1 Prouveur et prouveur de pr dicats Souvent une d monstration peut tre men e simplement en alternant les appels au c ur de preuve et au prouveur de pr dicats Normal
31. par exemple apr s une boucle op rations import es pour g n rer les obligations de preuve d une implantation le g n rateur de PO expanse textuellement les op rations import es Donc il faut s attendre trouver dans ces obligations de preuve le code des op rations import es Par exemple si une op ration sp cifi e par ANY xx WHERE est utilis e la variable interm diaire xx peut appara tre dans les obligations de preuve de l implantation utilisatrice La remarque pr c dente est vraie tous les niveaux de raffinement pour des op rations incluses positionnement dans des cas quand la sp cification ou le raffinement contiennent des cas le g n rateur de PO s pare les diff rents cas dans diff rentes obligations de preuve Il est alors n cessaire de regarder les hypoth ses locales elles sp cifient dans quels cas on se place et permettent de retrouver pr cis ment la ligne concern e Voici des exemples qui provoquent des s parations par cas ANY WHERE P gt Q A Po gt Qs dans une sp cification SELECT P THEN S WHEN Po THEN S2 END dans une sp cification IF THEN ELSE END dans une implantation CASE dans une implantation limination de variables le g n rateur d obligations de preuve limine de lui m me les variables interm diaires inutiles Par exemple pour VAR vv IN vv op si la sp cification de op est rr op rr var c
32. que le but g n r est compl tement instanci Par exemple la r gle binhyp H A h B gt va produire pBur le but le but d riv h chdtent Autre exempl amp r gle 9 binhyp b gt est fausse car lemme math matique associ b gt B est faux si le but est de la forme et que l on d stle mtiliG r les hypoth ses H pour r soudre Q il faut d abord les faire monter dans la pile des grace a la commande dd ou dd 0 une r gle backward en arri re est de la forme garde s A sous but s gt qui signifie queybut est transform en sous but si la garde est vraie garde s et sous but s peuvent tre inexistants On parle alors de r gle atomique Par exemple a a 0 une r gle de r criture est de la forme INDICATIONS UTILES POUR LA PREUVE 121 garde s A sous but s gt qui signifie quorforhedlle efonmmkf rm en formule2 si la garde est vraie et si le sous but est d montr garde s et sous but s peuvent tre inexistants On parle alors de r gle atomique Par exemple a 1 1 q Les gardes sont l pour restreindre le champ d application de la r gle aux cas o elle est juste Les gardes les plus utiles sont binhyp H vraie si H est en hypoth se btest a op b vraie si a op b est vrai op doit appartenir lt gt lt gt et a b doivent tre des identificateurs B ou des nu
33. tconnait tt 0 pass tident tt LA PHASE DE PREUVE FORMELLE 83 pass tident lt ntt gt tident tt tt 0 End Notez toutes les nouvelles hypoth ses d riv es qui ont t g n r es par le coeur de preuve En mode batch seules les nouvelles hypoth ses sont affich es chaque tape sauf quand on recule dans l arbre de preuve par exemple cause d une commande Back comme nous allons le voir l tape suivante Nous reculons sur la commande pr conform ment la m thode g n rale PRI gt ba Current PO is fork 6 Unproved saved Unproved Command line is Force 0 Next Saved line pos 1 Force 0 dd Hypothesis Component properties amp pass IDENTITES gt PASSWORDS amp tconnait tt pass tident tt Y StationUnix fork 6 Goal Local hypotheses amp ntt TACHES amp not ntt taches amp tt 0 taches ntt amp Check that the invariant tt tt gt tconnait ntt tconnait tt tt 0 pass tident lt ntt gt tident tt tt 0 End Pour courter ce texte nous n avons pas fait figurer toutes les hypoth ses Notez l volution de la ligne de commandes sous la clause command line is Nous sommes revenus au d but de la d monstration nous pouvons essayer l application du prouveur de pr dicats PRI gt dd amp pp Starting Deduction Starting Prover Predicate Call EXECUTION ABORTED ON GOAL long dump
34. Aide 4 prouv es restantes DemoExample INTERACTIVE PROOF 1 Nom du composant Font Mode ascii math Quit Bouton de fin 5 j inte A Sobin 1 Unproved PO De interru ption 6 Situation Initialisation PO1 Proved PO2 Proved PO3 Unproved End 22 Menu de position 23 Liste des obligations de preuve du composant ____ Zone de gestion 2 des PO F E 5 Math Deme 24 Boutons de d placement 31 Etat de la PO courante Current State of PO No current PO Commands Executed Next Zone de gestion 3 32 Fen tre de la ligne de la PO courante de commandes 33 D monstration sauv e Les diff rentes parties de cette fen tre sont les suivants 1 Le nom du composant qui est rappel dans la barre de label de la fen tre 2 La zone de gestion des PO regroupe tout ce qui concerne le composant vu dans son ensemble 21 L indicateur d obligations de preuve restant d montrer indique le nombre de lemmes non encore prouv s Cette zone devient verte lorsque le composant est enti rement prouv 22 La barre des menus de position permet de r gler l affichage de la liste des obliga tions de preuve d utiliser les Goto sp ciaux comme Goto Withoutsave etc Le bouton Show Print permet d imprimer ou de sauver dans un fichier les l ments de la preuve interactive 23 La liste donne le
35. E2 gt xx 1 ETATS PRI gt pp rp 0 Starting Predicate Prover Call Proved by the Predicate Prover xx EO gt xx 1 ETATS Le second sous but est prouv Le troisi me sous but est alors d montrer Il suffit d ajou ter l hypoth se xx E0 gt xx l e E0 E1 puis d ex cuter nouveau le prouveur de pr dicats afin de d montrer le dernier but PRI gt ah xx 1 E0 E1 Starting Add Hypothesis xx 1 FO E1 gt xx 1 ETATS PRI gt pp rp 0 Starting Predicate Prover Call Proved by the Predicate Prover 128 Prouveur interactif Manuel Utilisateur L arbre de preuve de la d monstration est le suivant xx 1 IP ETATS xx 24 gt ETATS xx fl 1 3 ETATS xx 1 1 3 ETATS y xx 1ESETATS gt xx 1 1 3 ETATS xx 1 1 3 ETATS a xx 3E gt ETATS gt xx 1 1 3 ETATS xx 1 1 3 ETATS xx l RE gt ETATSPYBR gt ETATS gt xx 1 1 3 JETATS xx l IF gt ETATSARPSETATS gt xx 1 1 33ETATSH xx 1 IP gt ETATSP y RE gt ETATS PY BP gt ETATS gt xx 1 1 37 ETATS 7 7 Application premier exemple Soit les composants MACHINE M1 VISIBLE_VARIABLES tab INVARIANT tab 0 7 gt 0 1 INITIALISATION tab 0 7 0 OPERATIONS op BEGIN tab tab 0 7 gt 0 1 amp tab 0 0 tab 1 1 amp tab 2 1 amp tab 3 0 amp tab 4 1 amp tab 5 0 amp tab 6 1 amp tab 7 0 END
36. END INDICATIONS UTILES POUR LA PREUVE 129 et IMPLEMENTATION M1_i REFINES M1 INITIALISATION tab 0 7 0 OPERATIONS op BEGIN tab 0 0 tab 1 1 tab 2 1 tab 3 0 tab 4 1 tab 5 0 tab 6 1 tab 7 0 END END L tat du projet apr s avoir ex cut la preuve des 2 composants en force 0 est le suivant Project status 3557 COMPONENT TC POG Obv nPO nUn Pr BOC C Ada C gt M1 OK OK 31 21 O1 100 M1_i OK OK 71 181 81 551 I Here TOTAL OK OK 10 201 81 601 I Apr s avoir d marr le prouveur interactif la commande gs permet de conna tre la forme des obligations de preuve restant d montrer PO9 Unproved tab 1 lt 01 gt 0 lt 11 gt 1 lt 21 gt 1 lt 31 gt 0 lt 41 gt 1 lt 51 gt 0 lt 61 gt 1 lt 71 gt 0 0 7 gt 0 1 P011 Unproved tab 1 lt 0 gt 0 lt 11 gt 1 lt 21 gt 1 lt 31 gt 0 lt 41 gt 1 lt 51 gt 0 lt 61 gt 1 lt 71 gt 0 0 0 P012 Unproved tab 1 lt 0 gt 0 lt 11 gt 1 lt 21 gt 1 lt 81 gt 0 lt 41 gt 1 lt 51
37. F d sCheck that the invariant taches c TACHES is preserved by the dom Paes PASSION operation ref 3 47 taehos tty c TACHES gt p 4 N pass tident tt c PRI gt f tident tt 0 fork 6 Next Goto Pass Current 0 is Rrk 6 et om tident lt TA ES Unproved saved Proved Goal Local hypotheses A Current State of PO Unpro g ntte TACHI CHER A i gt ntte taches tt DE taches ntt A Commands Executed Next Check t he invariant Vtt tte taches tconnait tt pass tidentett 1 is preserved by the operation ref 3 4 force A pr Red A teonnaitufntt e tt o ae AE ntident tt tt 0 Next st E Red ext step_pr Re 4 Starting Prover all d o Current PO is fork 6 Unproved saved Proved Force 0 A a Goal pr Red A E teonnaitufntt means ERIN FE et REVERS ntt A fpass tidenta at wtident tt an 2 PRI gt EE SJ pa 7 Nous montrons ci dessus la disposition typique des fen tres lorsque l op rateur est concentr sur une obligation de preuve la fen tre de commande et du but est en avant la zone de ligne de commande est visible gauche La fen tre des hypoth ses est intercal e de mani re ce que les plus r centes hypoth ses soient visibles et proches par d bordement gauche tout en gardant une taille de fen tre suffisante En appuyant sur une seule touche l op rateur peut ramener les hypoth ses devant nous ne dirons pas quelle touche cela d pend de votre en
38. SearchRule Penser ApplyRule d s qu il est clair qu une transform e math matique simple permet de conclure En effet il faut chercher appliquer des r gles les plus simples possibles ces r gles ont ainsi plus de chances de se trouver dans la base LA PHASE DE PREUVE FORMELLE 63 Les commandes pour les r gles manuelles Les commandes suivantes deviennent n cessaires si on est conduit a utiliser des r gles manuelles ApplyRule ar cette commande permet l application d une r gle Il peut s agir d une r gle de la base trouv e par SearchRule d une r gle ajout e apr s preuve par le prouveur de pr dicats voir paragraphe 6 2 4 ou d une r gle manuelle Penser ApplyRule d s qu il est clair qu une transform e math matique simple permet de conclure En effet il faut chercher appliquer des r gles les plus simples possibles ces r gles ont ainsi plus de chances de se trouver dans la base ou d tre d montr es par le prouveur de pr dicats Si la r gle doit tre ajout e manuellement sa validation sera facilit e si elle est simple PmmCompile pc cette commande permet la lecture et la compilation du fichier composant pmm contenant les r gles manuelles Utiliser PmmCompile pour prendre en compte une modification dans le fichier pmm La g n ralisation La commande suivante s utilise apr s le succ s d une premi re obligation de preuve si Vop rateur d sire g n raliser sa
39. Starting Prover Call Current PO is Initialisation 1 Unproved saved Unproved Goal 0 lt 400 c1 c2 c3 c4 End Il s agit maintenant d obtenir des intervalles de variation qui ne d pendent plus des autres variables pour c2 c4 c est dire qu il faut d corr ler les variables Nous allons sugg rer au prouveur de faire cette op ration en commencant par c2 qui ne d pends que de c1 PRI gt ah c2 lt 100 Starting Add Hypothesis Current PO is Initialisation 1 Unproved saved Unproved Goal c2 lt 100 End LA PHASE DE PREUVE FORMELLE 93 Le prouveur tente maintenant de d montrer ce premier r sultat simple Nous relancons le coeur de preuve PRI gt pr Starting Prover Call Current PO is Initialisation 1 Unproved saved Unproved Goal c2 lt 100 gt 0 lt 400 c1 c2 c3 c4 End Ce r sultat interm diaire a t prouv directement ce qui se voit par la r apparition du but initial sous la forme H gt B o H est l hypoth se ajout e La commande pr ne termine toujours pas le lemme l essai n est pas repr sent Nous pouvons faire monter cette hypoth se par une simple commande de d duction PRI gt dd Starting Deduction Current PO is Initialisation 1 Unproved saved Unproved Goal 0 lt 400 c1 c2 c3 c4 End Continuons de m me avec c3 PRI gt ah c3 lt 100 Starting Add Hypothesis Current PO is Initialisation 1 Unproved saved Unproved Goal c3 lt 100 End PRI gt pr Starti
40. aa 157 9 4 Les diff rents niveaux des commandes interactives 158 E E Ee ee d 159 dive Se nee aod So A aoe dle bs AAS So 159 oie de 160 Mutha Ga fe ae dds eee eee en OR 160 9 9 Utilisation de pp rp 0 42 4428 4 ae a ae ae 40e A EO 161 9 10 Pourquoi pr choue pp choue et pp rp 0 r ussit dans certains cas 162 Chapitre 1 Introduction Ce manuel d crit la m thode que nous conseillons pour les activit s de preuve d un projet avec les outils de l Atelier B Le credo de cette m thode est de d composer ces activit s de preuve en deux phases La phase de mise au point analyse rapide des obligations de preuve et modification des composants B quand ces obligations r velent des erreurs La phase de preuve formelle preuve formelle complete des obligations de preuve Les composants B ne sont plus modifi s Cette m thode n est bien entendu pas la seule envisageable I y a deux utilisations pos sibles de ce manuel vous pouvez le lire avant d utiliser 1 Atelier B vous pouvez aussi vous en servir au moment de la preuve de votre projet pour faire un suivi pas pas des tapes correspondantes Attention ce document ne remplace pas le manuel de r f rence du prouveur Il ne contient pas une description analytique de chaque commande Par exemple le lecteur n y trouvera pas la liste des mots clefs employer dans la commande ApplyRule Ce manuel cherche plut
41. c est en fait le mode de pilotage du coeur de preuve dans lequel la commande Prove pr est essay e sur chaque obligation de preuve La d monstration interactive au contraire permet a l op rateur de d cider lui m me quelles commandes de preuve sont appliqu es La s quence des commandes qu il a choisies pour d montrer une obligation est m moris e avec l tat de preuve c est la d monstration in teractive Pour le mode automatique il suffit de m moriser la force maximale tent e pour chaque obligation c est le niveau de preuve automatique de lVobligation 3 1 4 L outil de preuve en g n ral Le fonctionnement global de l outil de preuve prouveur automatique et prouveur interac tif peut se comprendre sur le sch ma suivant Prouveur Prouveur Automatique Interactif Commandes de preuve C Coeur de preuve Quand vous utilisez le prouveur interactif une interface vous permet d envoyer des com mandes vers le prouveur L une de ces commandes est Prove pr qui lance le c ur de preuve sur le but courant Vous disposez ainsi tout instant des m canismes de preuve au tomatiques Quand vous utilisez le prouveur automatique toutes les obligations de preuve du composant sont trait es soit en appliquant une commande pr soit en rejouant les commandes enregistr es Dans ce cas il s agit des commandes enregistr es pour chaque obligation de preuve lors de la derni re session int
42. cette garde value une expression litt rale de l une des formes suivantes a b a b a lt b a gt b a lt bet a gt b l criture ASCII correspondante est btest a b btest a b btest a lt b btest a gt b btest a lt b btest a gt b LA PHASE DE PREUVE FORMELLE 69 Les quatre derni res formes qui concernent la relation d ordre ne sont VRAIES que si a et b sont des entiers litt raux et positifs Par exemple la r gle btest x gt 0 gt EN permet de d charger les buts 3 N 100 N etc Les formes btest a b et btest a 4 b concernent l galit lexicale elles testent si a et b sont lexicalement gaux Par exemple btest varl var2 est faux m me si il existe une hypoth se qui pr cise varl var2 mais btest aa aa est vrai Attention l galit lexicale ne s applique qu aux nombres ou aux identifiants Par exemple btest xx yy xx yy est faux car xx yy n est ni un nombre ni un identifiant 6 2 3 L criture d un fichier de r gles manuelles En dernier recours l op rateur peut introduire une r gle manuelle non d montr e pour d panner une preuve Cette m thode ne doit tre employ e qu apres chec de la preuve par les commandes interactives et chec de l ajout de la r gle d sir e comme r gle prot g e par le prouveur de pr dicats commande Validation of Rule La r gle est alors crite en langage de th orie dans un fichier Ce fichier doit s appeler co
43. cours de la phase de mise au point I ne peut s agir que de d monstrations tres simples mais elles vitent d avoir revenir sur l obligation de preuve concern e et leur simplicit leur permet souvent de se g n raliser d autres obligations Nous allons d crire ceci en deux tapes trouver une d monstration rapide et la g n raliser 5 6 1 Trouver une d monstration rapide Se donner un d lai limite il faut viter de s garer dans une v ritable preuve formelle on se donnera donc une limite de temps variant entre 30 secondes et deux minutes suivant la complexit de l obligation Essayer le prouveur de pr dicats si l obligation semble pouvoir se d montrer sans notions arithm tiques vous pouvez essayer la commande PredicateProver pp qui lance 48 Prouveur interactif Manuel Utilisateur le prouveur de pr dicats avec un temps limite de 60 secondes G n ralement il vaut mieux faire cette commande apr s une d duction dd pour faire monter les hypoth ses locales Quelques variantes utiles pp 30 pour r duire le d lai d expiration 30 secondes pp rp 1 ou pp rp 2 qui permet d appliquer le prouveur de pr dicats sur l obliga tion r duite avec une ou deux passes d inclusion d hypoth ses partir du but En effet si vous avez plus d une centaine d hypoth ses la commande pp sera longue le seul temps de traduction en pr dicats quantifi s est d j important S
44. d abord simplifier le but qui devient zx lt 17 Il est alors beaucoup plus difficile de faire le lien avec l hypoth se clef xx 1 8 lt yy Si op rateur voit cette simplification mal choisie il d cide d agir avant d appeler le c ur de preuve Une action possible est de provoquer l application de l une des r gles de la base du prouveur nous verrons plus loin le format de ces r gles et comment on les recherche par SearchRule Supposons qu il existe une r gle OrderXY 77 qui puisse d montrer notre PO La commande pour l appliquer 22 Prouveur interactif Manuel Utilisateur est ApplyRule nous ne d crirons pas ici sa syntaxe ni celle de notre r gle La commande tap e serait par exemple ar OrderXY 77 Once La preuve r ussit Nous avons alors affaire une preuve effectu e de mani re totalement manuelle sans appel au coeur de preuve et sans ajout de r gle Dans certains cas il se peut que la r gle sp cifique n cessaire a la preuve ne soit pas dans la base du prouveur et qu aucune autre m thode de d monstration n aboutisse Il faut alors ajouter la r gle en tant que r gle manuelle Si des r gles manuelles ont t utilis es pour la preuve d un composant cette preuve peut tre fausse si certaines des r gles sont fausses Il s agit alors d une preuve sortant de la sph re s curitaire du prouveur de l Atelier B mais la validation de cette preuve se ram ne la validation des r g
45. d compos par action de la r gle simpl 1 et des r gles natives du prouveur 134 Prouveur interactif Manuel Utilisateur 7 8 Application second exemple Soit le nouveau composant M1_i en remplacement du pr c dent IMPLEMENTATION M1_i REFINES M1 INITIALISATION tab 0 7 0 OPERATIONS op BEGIN tab 0 0 mod 2 tab 1 1 mod 2 tab 2 1 mod 2 tab 3 0 mod 2 tab 4 1 mod 2 tab 5 0 mod 2 tab 6 1 mod 2 tab 7 0 mod 2 END END La seule diff rence par rapport l exemple pr c dent est apparition uniquement d monstrative ici du modulo qui rend le rejeu des d monstrations inefficace car apr s rejeu il reste tou jours 8 obligations de preuve non prouv es Pour se ramener au cas pr c dent il suffirait d ajouter en hypoth se de toutes ces obligations de preuve les pr dicats 0 mod 2 0 1 mod 2 1 puis d utiliser ces galit s pour remplacer le terme de gauche par le terme de droite dans chacune des obligations de preuve Une solution consiste ajouter des pr dicats en assertions ASSERTIONS O mod 2 0 1 mod 2 1 Ces 2 assertions se d montrent facilement en preuve interactive pp rp 0 La d monstration des obligations de preuve non prouv es se fait par utilisation de ces 2 galit s puis ex cution de la d monstration interactive de l exemple pr c dent INDICATIONS UTILES POUR LA PREUVE 135 La d monstration d
46. d monstration lors de la preuve du composant c est dire imm diatement Conclusion en pr sence d un but existentiel abstrait il faut toujours modifer le composant pour faire appara tre une d finition explicite de la notion math matique concern e 5 7 3 Les buts non d coup s Les buts non d coup s apparaissent quand l algorithme de d coupage du g n rateur d obli gations est mis en d faut Il n est pas forc ment n cessaire de modifier le composant de telles obligations pouvant tre plus faciles prouver qu il n y para t Dans la plupart des cas le but non simplifi est de la forme P V Q Pour lire de tels buts il faut utiliser la commande pr Red pour faire monter les hypoth ses locales en simplifiant le but compl ter 5 8 Les obligations de preuve qui semblent fausses Lorsque le composant examin comporte des erreurs certaines obligations de preuve sont fausses C est ainsi que l utilisation de la m thode B signale les erreurs telles que le non res pect de la sp cification ou des propri t s invariantes Nous proposons la m thode suivante en cas d obligation de preuve fausse S assurer que l obligation de preuve est bien fausse quand une obligation de preuve semble fausse il faut en avoir une assurance suffisante avant de commencer les modifications dans le composant Les cons quences d une modification faite tort peuvent tre tr s co teuses Trouver la faut
47. d monstrations math matiques formelles nous vous recommandons la lecture de ce court chapitre Le chapitre 3 est une pr sentation g n rale des outils de preuve de l Atelier B Il montre comment acc der ces outils depuis les menus de l interface et explique comment vous pourrez intervenir pour piloter une d monstration qui n aurait pas abouti automatique ment Si vous n avez jamais utilis les outils de preuve la lecture de ce chapitre est vivement recommand e Les chapitres et 6 d finissent la m thode pr conis e dans ce manuel pour conduire les activit s de preuve Le chapitre 4 montre la d composition principale de la preuve en deux phases la phase de mise au point du projet et la phase de preuve formelle proprement dite Il indique comment savoir dans quelle phase on se trouve et quand en changer Le chapitre 5 d crit la phase de mise au point et le chapitre 6 d crit la phase de preuve formelle Dans ces deux chapitres 5 et 6 la phase de preuve concern e est d compos e en plusieurs activit s Lors du d veloppement d un projet en B vous pouvez suivre dans ce manuel chacune des tapes de vos activit s de preuve vous disposerez ainsi imm diatement des remarques adapt es chaque situation Le chapitre 8 est un recueil d tudes de cas I vous permettra de voir sur des exemples les astuces utilis es en preuve interactive Chapitre 2 Rappels de preuve formelle Le principe des
48. de la preuvel 99 dace dh ah Seon eae sent ie a EE 99 Ey aoe e eS a y 101 Sng tt Poot ae Pa Big be 103 Sy Ste wr ev Oe OR ee eS Ee ee ak 104 fh ee o CN eee eee te ee 108 6 7 1 Les commandes par situation 108 oe 108 6 7 3 Instancier p gt q si p est presque en hypoth sel 109 6 7 4 Penser ah plut t que r gle par l avant 110 6 7 5 Probl mes de normalisation parenth ses 110 MAN ew MN ain e e oe Pe ee e 111 6 8 1 Le contr le des preuve par cas 111 E aa 111 aa 112 6 8 4 Les probl mes de chargement 2 2222004 113 115 7 1 Poursuite de la preuve en fonction de la forme du but 115 ish eee iam 116 Roe E E ee eee a a 116 7 2 2 Limitation du temps de calcull 117 7 2 3 Utilisation de pp bon escient 117 fae oe et eee oe 118 ae Re ok ee eae ee ee ne 120 O Ge byte Bk eee hk ee aes ag ee ee 122 a te 124 7 6 Utilisation de la commande Do Casesl 126 hl OL E ee eon a ee 128 7 8 Application second exemple 134 137 he Dh ce le eh ideas as 138 Pw oe ed oe Do dk de da SSS 142 155 teas 155 atte Meee ep eee ees ioe ee 156 9 3 Comment savoir s il faut ajouter une r gle manuelle 157 iv TABLE DES MATIERES ie a a e E a i ee ete ea A 157 cl ee ea
49. est rr et non pas vu qui appara t dans les obligations de preuve Ceci peut surprendre car ce n est pas la donn e manipul e dans le composant a prouver qui apparait ordre des obligations de preuve Les obligations de preuve concernant les pr conditions des op rations appel es dans la clause prouver apparaissent g n ralement au d but 40 Prouveur interactif Manuel Utilisateur m me si ces appels sont la fin de la clause Dans une implantation les obligations de preuve de non d bordement des calculs interm diaires sont au tout d but commentaire du but l hypoth se qui appara t en dernier dans la fen tre des hypoth ses apr s que vous ayez tap dd est un commentaire qui explique la provenance du but Ce commentaire contient une phrase explicative et une r f rence au manuel des obligations de preuve Exemple supposons que le but de l obligation de preuve 30 de l op ration Commandes Pompes du composant CmdPmp_1 soit 1 NB_PUMP x FALSE 4 indice_187777 1 NB_PUMP lt TRUE l_wpok gt TRUE FALSE 2 on 1 1 NB_PUMP x FALSE 4 TRUE gt l_wpok gt TRUE FALSE gt 3 on 1 Les quatre variables utilis es dans ce but sont NB_PUMP l_wpok indice_187777 et on 1 On retrouve d abord le sens de chacune des variables NB_PUMP est le nombre de pompes a commander l_wpok est un tableau qui indique pour chaque pompe si elle est OK ou non indice_1 7777 est un i
50. fini une AN hypoth ses lt Barres de label IS PO Donne en particulier situation globale elles rappellent le nombre de PO restantes touj oujours le nom du composant de op ration et le fen tre de contrBle numero de la PO zone de la ligne de commandes l indentation ermet de savoir o on est p RS Zone de but dans la d monstration TE zone de visualisation des commandes sauv es celle qui est en t te de liste sera Ne y ex cut e au prochain Step Zone principale de commande C est l que l on tape les commandes directement Il y a deux modes principaux d utilisation au cours d une session de preuve circulation entre les PO quand l op rateur a fini une d monstration il cherche quelle est la prochaine obligation de preuve a traiter et combien il en reste Son attention est alors port e sur la fen tre de situation globale LA PHASE DE PREUVE FORMELLE 77 preuve quand l op rateur fait une preuve son attention est port e sur le but sur la zone de commandes et sur la zone de la ligne de commandes qui lui permet de se positionner dans la d monstration Les zones d attention dans ces deux modes sont montr s ci apres mode circulation mode preuve En mo
51. gt x mod5 0 A Vax xx ran cc gt xxmod7 0 Nous voyons qu il faut simplement prouver la validit de notre sp cification en montrant qu il existe bien une constante qui v rifie les propri t s annonc es Ici il suffit de prendre cc Y Nous utilisons la commande SuggestforErists se qui permet de sugg rer de tenter la preuve avec une valeur particuli re pr Red pour charger les hypoth ses locales 50 Prouveur interactif Manuel Utilisateur se suggestion prendre cc Y pr relancer le c ur de preuve Et la preuve aboutit directement Si ce n tait pas le cas il faudrait examiner les buts produits apr s la commande SuggestforExists en utilisant ventuellement la technique du paragraphe Ce type de but complexe n indique pas que le composant soit modifier Exemple 2 forme trop ind termiste Soient les composants suivants MACHINE ComplexGoal2 OPERATIONS IMPLEMENTATION XX Op ANY ee WHERE ComplexGoal2_1 REFINES ee C NAT A Vuu uu ee gt uu mod 3 0 ComplexGoal2 OPERATIONS THEN E ee XX Op xx 9 XX Ro END END La sp cification ci dessus signifie simplement que l op ration doit retourner un r sultat divisible par 3 mais elle est exprim e sous une forme bien trop ind terministe Nous obtenons le but suivant Jee ee E NAT A Vuu uu ee gt uumod3 0 A xx 0 xx 0 ee A 9 xx 0 Pour pouvoir lire le but plus simplemen
52. gt 0 lt 61 gt 1 lt 71 gt 0 1 1 P013 Unproved tab 1 lt 0 gt 0 lt 11 gt 1 lt 21 gt 1 lt 81 gt 0 lt 41 gt 1 lt 51 gt 0 lt 61 gt 1 lt 71 gt 0 2 1 P014 Unproved tab 1 lt 0 gt 0 lt 11 gt 1 lt 21 gt 1 lt 381 gt 0 lt 41 gt 1 lt 51 gt 0 lt 61 gt 1 lt 71 gt 0 3 0 P015 Unproved tab 1 lt 0 gt 0 lt 11 gt 1 lt 21 gt 1 lt 31 gt 0 lt 41 gt 1 lt 51 gt 0 lt 61 gt 1 lt 71 gt 0 4 1 P016 Unproved tab 1 lt 0 gt 0 lt 11 gt 1 lt 21 gt 1 lt 81 gt 0 lt 41 gt 1 130 Prouveur interactif Manuel Utilisateur lt 5 gt 0 lt 6 gt 1 lt 7 gt 0 5 0 P017 Unproved tab 1 lt 0 gt 0 lt 1 gt 1 lt 2 gt 1 lt 3 gt 0 lt 4 gt 1 lt 5 gt 0 lt 6 gt 1 lt 7 gt 0 6 1 7 obligations de preuve ont m me forme La recherche de r gles de la forme f lt g x e par la commande sr A11 f lt g x c ne permet pas de d couvrir de r gle direc tement applicable Plut t que de r aliser 7 preuves interactives successives l ajout d une regle de simplification peut tre envisag e Le fichier M1_i pmm contient maintenant THEORY func IS bcalli BackwardRule func 1 amp bnum a amp bnum c amp bnot btest a c amp f c d gt lt al gt b c d END Cette r gle doit maintenant tre compil e et charg e en m moire g
53. hypoth se dans le prouveur pour faire aboutir directement une d monstration La commande AddHypothesis est optimis e pour ce cas l ah h si h est d j en hypoth se cr e directement le but h B sans demander la d monstration de h Il faut penser faire repasser des hypoth ses par le prouveur dans les cas suivants si une galit importante semble tre une hypoth se d riv e Attention en particulier aux galit s g n r es par instanciation de p gt a b Il faut alors refaire passer la nouvelle hypoth se a b dans le prouveur si plusieurs pr dicats se simplifient entre eux par exemple p A Vx x EE p gt q faire passer la conjonction de ces pr dicats dans le prouveur Cette tactique permet de faire agir le m canisme de simplification des conjonctions disjonctions car celui ci est lanc sur tout nouveau but si une hypoth se dont la normalisation n est pas termin e pourrait faire aboutir la d monstration exemple P non simplifi L interface du prouveur interactif est optimis e pour permettre la s lection rapide d une hypoth se pour la refaire passer dans le prouveur 1 Pacer le curseur a gauche de l hypoth se choisie dans la fen tre des hypoth ses et tirer vers le bas pour noircir une zone commen ant par cette hypoth se 2 Presser le troisi me bouton de la souris la s lection se cadre automatiquement sur l hypoth se choisie 3 D signer le bouto
54. indique que le terme de gauche de la r criture doit contenir cette formule La r ponse du prouveur est Searching in Rewr rules with filter consequent should contain f a b Starting search Rule list is SimplifyRelImaLongXY 6 Backward r u v rlulX rtv End of rule list La r gle existe donc bien Notons que les jokers r u et v utilis s ne sont pas ceux que nous avons employ s pour la recherche le nom des jokers n importe pas En fait une r gle de la forme rlu x aurait galement t retenue Nous pouvons appliquer cette r gle PRI gt ar SimplifyRelImaLongXY 6 Goal Starting Apply Rule Current PO is Initialisation 1 Unproved saved Unproved Goal 98 Prouveur interactif Manuel Utilisateur ff 0 50 ff 51 100 lt 0 100 End Finissons la d monstration PRI gt pr Starting Prover Call Current PO is Initialisation 1 Proved saved Unproved Goal Check 3 3 gt f 0 50 51 100 lt 0 100 End Dans cet exemple nous avons vu comment chercher une r gle dont l id e nous est venue au lieu de l crire dans un fichier pmm Cela permet d tre s rs que la r gle est valide La r gle que nous avons utilis e appartient a une th orie dont le nom contient le mot Long Les th ories qui ont cette particularit regroupent des r gles qui rallongent les expressions qu elles transforment Ces r gles ne sont jamais utilis es par le prouveur automatique car el
55. initial va donc tre divis en deux comme nous l avons vu plus haut Pour viter d avoir faire les deux cas ncl nc2 lt 0 et ncl nc2 gt 0 pour deux sous buts nous sommes oblig s d utiliser dd L option pr Red de la commande pr ne nous permet pas d viter apparition des deux sous buts dans ce cas car il ne s agit pas d une tentative de preuve par cas du prouveur mais bien d une r gle de base pour prouver x u v il faut d montrer u lt x puis x lt v Ces consid rations peuvent tre faites en effectuant rapidement quelques essais de la commande pr a partir du but pr c dent il n est pas n c ssaire d tudier la programmation interne du prouveur La premi re commande que nous allons utiliser est donc dd PRI gt dd Starting Deduction Le but devient nel ncel ne2 2 nc2 nel ne2 2 1 1 Les hypoth ses locales sont maintenant la fin de la liste affich e dans la fen tre des hypotheses Pour faire deux cas suivant le signe de ncl nc2 nous disposons de la commande DoCases dc Rappelons les deux formes de cette commande 146 Prouveur interactif Manuel Utilisateur dc P permet de se placer dans les cas P et P dc v E preuve pour v valant chacun des l ments de E Nous devons utiliser la premi re forme Dans une preuve par cas il est toujours indiqu de commencer par le cas le plus difficile ici c est probablement le cas o ncl nc2 est n gatif E
56. ne pas tre d montr par le prouveur de pr dicats car les termes qu il contient g n rent des pr dicats complexes lors de la traduction du but en pr dicats manipulables par le prouveur de pr dicats Dans ce cas il suffit de remplacer chaque terme 158 Prouveur interactif Manuel Utilisateur complexe par une variable afin d obtenir une r gle plus facilement d montrable Cette r gle une fois d montr e est ajout e au fichier Pmm puis utilis e afin de d montrer le but Par exemple le but xalrzx INT A x mod10 0 xx xx Z A Ayy yye Z 10 x yy xx A xxalrreZ A Ayy yyeZ A 10 x yy xx C xxlxx Z A xxmod10 0 gt min x xx Z A xxmod10 0 min xxlxxeZ A Ayy yy EZ A 10 yy xx n est pas d montr par le prouveur de pr dicats ni par le prouveur Par contre la r gle aCb A bCa gt min a min b est d montr e par les outils de preuve de r gles PRI gt vr Back a lt b amp b lt a gt min a min b The rule was proved Elle est ajout e au fichier Pmm qui contient alors THEORY MyRule IS a lt b amp b lt a gt min a min b END Elle est ensuite charg e en m moire grace a la commande pc PRI gt pc Loading theory MYRule Elle peut enfin tre appliqu e PRI gt ar MyRule 1 Once Starting Apply Rule 9 4 Les diff rents niveaux des commandes interactives On peut s parer les commandes d orientation de la pre
57. not p ct Contradiction la d monstration faire ressemble une autre te TryEverywhere hypoth se clef de la forme Vx P x Q x ph ParticularizeHypothesis hypoth se P gt Q non exploit e avant toute commande risqu e mh Modusponenson Hypothesis sw Save Withoutquestion 6 7 2 Refaire passer des hypoth ses dans le prouveur La commande AddHypothesis ah h s utilise souvent avec le param tre h correspon dant textuellement une hypoth se qui existe d ja Dans ce cas le r sultat cherch n est videmment pas de rajouter l hypoth se mais simplement de la faire redescendre dans le but qui devient h gt B B tant le but courant Au prochain appel au c ur de preuve h recevra le traitement privil gi des hypoth ses locales en fait c est un moyen d attirer LA PHASE DE PREUVE FORMELLE 109 Vattention du prouveur sur cette hypoth se Ceci est particuli rement utile si h tait une hypoth se d riv e Les hypoth ses d riv es sont celles qui sont produites apr s normalisation par des r gles par l avant par exemple a FALSE A a bool P gt P Cette r gle produit l hypoth se d riv e P si a FALSE et a bool P sont en hypoth se Les hypoth ses g n r es de cette fa on ne b n ficient pas du m me traitement que les autres pour des raisons d efficacit risque de bouclage Il suffit donc parfois de refaire passer une
58. on puisse d montrer que P gt Q et Q gt P soient quivalents autrement dit que P V Q est identique Q V P D autre part la d finition de P V Q est un exemple justifiant notre assertion que tout but est vrai sous des hypoth ses fausses voir paragraphe 2 2 En effet consid rons la proposition btrue V Q De fa on ce que la d finition du ou corresponde la notion naturelle nous souhaitons que cette proposition soit toujours vraie Autrement dit btrue V Q 4 btrue D apr s la d finition du symbole V cela s crit btrue VQ lt 7 btrue gt Q bfalse gt Q Il est donc n cessaire de consid rer que bfalse gt Q est toujours vrai Le lecteur pourra se reporter au B Book pour avoir la liste des propri t s essentielles des op rateurs propositionnels Nous citerons ici quelques propri t s moins fondamentales mais choisies pour leur importance lors de l utilisation de l Atelier B bfalse gt P btrue P P btrue P bfalse lt btrue P lt btrue AP NN EPS ET NS 2 4 Les pr dicats quantifi s Afin d exprimer les propri t s de nos composants crits en langage B nous aurons besoin de nouvelles notions Par exemple nous pourrions avoir d montrer une propri t sur un indice de boucle indice 1 10 gt indice lt MAXINT Il nous manque encore beaucoup d op rateurs pour cette criture Tout d abord nous avons besoin de la noti
59. phase de mise au point C est a partir de cette d monstration et non pas en relisant toute l obligation que nous devons d marrer notre preuve formelle pour cet exemple que le lecteur nous fasse confiance pour la d monstration intuitive Nous sommes dans l tape 1 Il est inutile d essayer pr puisque l obligation n est pas d montr e automatiquement Par contre la pr sence d unions et de relations nous sugg re d essayer le prouveur de pr dicats pp pr c d de dd pour s parer les hypoth ses Le prouveur de pr dicats choue Nous devons donc conform ment aux tapes 2 et 3 revenir de deux pas en arri re ba 2 et fair un appel au coeur de preuve mode r duit pr Red Cet appel charge les hypoth ses et cr e des hypoth ses d riv es Le but n a pas chang tconnait U ntt x tconnait tt 4t 0 pass tident lt ntt gt tident tt tt 0 Nous sommes dans l tape 4 le but peut tre consid r comme plus simple puisqu il ne contient plus les hypoth ses Nous passons en tape 6 choix de la commande interactive La d monstration intuitive que le lecteur nous fasse confiance sugg re de faire deux cas tt 0 ntt ou tt 0 ntt La commande est donc dc tt 0 ntt Le but devient tt 0 ntt gt tconnait U ntt x tconnait tt tt 0 pass tident lt ntt gt tident tt tt 0 Nous sommes revenus dans l tape 1 il faut essayer pr qui ne d montre toujours pas le
60. premier ant c dent instanci de la r gle Essayons de le d montrer par un simple appel au prouveur PRI gt pr Starting Prover Call Le but devient 2EN C est le deuxieme ant c dent le but pr c dent a t d charg Continuons PRI gt pr Starting Prover Call Le but devient C est le troisi me ant c dent le but pr c dent a t d charg Continuons PRI gt pr Starting Prover Call 148 Prouveur interactif Manuel Utilisateur Le but devient ncl nc2 mod 2 1 2 0 ncl ncl nc2 2 nc2 ncl nc2 2 1 1 Nous retrouvons le but pr c dent l ajout d hypoth se sous l hypoth se voulue Cette par tie de la d monstration a profit a la fois de la r gle ajout e et des fonctionnalit s de preuve automatique ce qui nous permet de ne pas s attarder sur les parties d montrables automatiquement La zone de ligne de commande contient l arbre de preuve suivant Force 0 dd amp dc nci nc2 lt 0 amp dd amp ah nci nc2 mod 2 1 2 0 amp ar IntDiv 4 0nce amp pr amp pr amp pr amp Next Le mot clef Next indent directement sous la commande ah indique que le but actuel est un sous but produit par cette commande Rappelons que ah H produit deux sous buts a partir d un but B le sous but H puis le sous but H B Nous sommes donc sur ce deuxi me sous but en effet Next est le deuxi me mot clef indent sous ah apr s ar La r gle manuelle
61. preuve Il s agit entre autre de closure closurel INTER UNION inter union Si votre but comporte un de ces symboles il est pr f rable de tenter la simplification d monstration du but par la combinaison r gles manuelle commande pr 162 Prouveur interactif Manuel Utilisateur 9 10 Pourquoi pr choue pp choue et pp rp 0 r ussit dans certains cas En preuve interactive on dispose de 3 prouveurs qui ont chacun leur sp cificit le prouveur automatique appel par mp ou pr qui applique des m canismes g n raux de simplification r solution et les r gles de la base de r gles le prouveur de pr dicats qui transforme le but d montrer en pr dicats puis ex cute quelques heuristiques charg es de d montrer le lemme par contradiction le prouveur arithm tique qui ne fonctionne qu avec une in galit en but Il recherche alors par combinaison lin aire des hypoth ses arithm tiques d montrer le but par contradiction Ces 3 prouveurs ont des domaines qui se recouvrent partiellement Il est bon de tester l un ou l autre des prouveurs sur un but pour voir s il est effectivement d montr Les 2 derniers prouveurs sont uniquement des solveurs en indiquant si le but est d montr ou non sans transformation simplification de celui ci Le prouveur automatique appliquant des r gles d quivalence transforme simplification d coupage le but et peut le d montrer lorsqu il se
62. remettant sa force 0 Si il y a beaucoup d hypotheses le chargement d une PO peut tre long en particulier pour la premi re PO d une op ration o il comprend le chargement de toutes les hypoth ses de contexte 1 minute par centaine d hypoth ses en force 1 Utiliser GotowithReset quand il y a plusieurs centaines d hypoth ses pour aller sur la premi re PO d une op ration SaveWithoutquestion sw provoque la sauvegarde forc e de la ligne de commande Utiliser sw de temps autre si la d monstration devient longue en particulier avant un changement de force ou des retours en arri re r p t s Reset re permet de revenir au d but de la d monstration d une PO Cela s utilise soit pour relire le but initial penser aussi 1p soit pour reprendre la d monstration avec l exp rience de l essai pr c dent penser sauvegarder auparavant sw Step st la commande Step ex cute la prochaine commande sauvegard e et avance de un le curseur dans la d monstration sauvegard e Utiliser Step pour rejouer une preuve sauvegard e Force ff permet de rejouer une d monstration dans une force diff rente Souvent utilis e pour remettre z ro la force d une PO avant de commencer une d monstration interactive cette commande devrait tre r serv e aux cas plus rares o l op rateur veut tenter l utilisation d une force sup rieure voir paragraphe 6 8 3 Sinon utiliser plut t GotowithRe
63. se ramenant des pr dicats quantifi s c est la commande pp L interface du prouveur utilise plusieurs fen tres pr vues pour tre juxtapos es et empil es L op rateur peut se concentrer soit sur le choix d une PO soit sur la preuve Les composants B en cours de preuve doivent tre facilement accessibles L op rateur doit organiser son cran avec le prouveur et les composants en cours de preuve Le prouveur interactif peut galement tre employ en mode batch dans un terminal La ligne de commande repr sente l arbre de preuve c est un rep re essentiel Les quatre tactiques simples de preuve sont Utilisation de pr et pp Utilisation de l ajout d hypoth ses et de la preuve par cas Recherche et utilisation de r gles du prouveur Utilisation de r gles manuelles La v rification finale de la preuve consiste rejouer toutes les d monstrations Cette v rification se fait avec les option Unprove et Replay du menu de preuve Une r gle d admission permet d admettre des buts pour explorer la suite de la d monstration C est une r gle ajout e dans le fichier pmm dont le cons quent est un joker Les forces sup rieures 1 2 et 3 s emploient parfois en preuve interactive La force 1 simplifie mieux les hypoth ses la force 2 ajoutes des hypoth ses d riv es La trace de preuve permet d analyser l action d une commande pr Il y a un tableau qui indique la commande de preuve
64. sur le chargement d une obligation 100 hypoth ses se chargent en 1 ou 2 secondes en force 0 et en 1 minute en force 1 La force conseill e pour la lecture d une PO est la force 0 car le temps d acc s est toujours n gligeable et les hypoth ses sont quand m me largement simplifi es en particulier les variables gales entres elles ont t limin es N anmoins on peut utiliser la force rapide si on veut visualiser les hypoth ses brutes La force m moris e sur chaque PO pour la d monstration interactive est bien s r celle que vous avez choisie lors de la derni re session interactive sur cette obligation Si c est la premi re fois que vous l acc dez c est la force 0 Une fois la PO charg e la force est affich e dans la zone de la ligne de commandes INTERACTIVE PROOF HYPOTHESIS GOAL Force 0 x LA PHASE DE MISE AU POINT 33 Si vous vous souvenez avoir sauv une force lev e pour l obligation acc der et que vous ne voulez pas que l acc s soit trop long vous pouvez utiliser le bouton GotowithReset qui remet en force 0 INTERACTIVE PROOF HYPOTHESIS Goto s Goto Save Goto Reset GOAL Maintenant l obligation de preuve est charg e les zones but hypoth ses et com mandes sont renseig
65. tre utilis e dans d autres pr dicats sans conflit Par exemple xx 2000 A Vere 10 xg lt 100 Ce pr dicat indique que la variable externe xx vaut 2000 et d autre part que tout nombre gal 10 est plus petit que 100 Il n y a pas de confusion entre l occurence de la variable externe et celle de la variable muette Une telle criture bien que correcte pr te toutefois a confusion il faut l viter Les r gles d inf rence relatives aux pr dicats universellement quantifi s sont l gerement plus complexes car elles font appel a la notion de variable non libre dans une expression notion que nous n aborderons pas dans ce chapitre La r gle principale restreinte aux pr dicats de la forme Vx P Q est la suivante Pour d montrer Vx P Q sous les hypoth ses HYP si la variable x n est pas utilis e dans HYP il suffit de d montrer Q sous les hypoth ses HYP P Cette r gle dite r gle de g n ralisation signifie que pour d montrer que Q est vrai pour toute variable x v rifiant P il suffit de se donner une variable x v rifiant P et de faire la preuve de Q sous ces hypoth ses Il y a videmment un probl me si la variable x est d j utilis e avec un autre sens dans les hypoth ses il faut alors r crire Vx P gt Q avec une autre variable De telles r critures de pr dicats font intervenir la notion de substitution que nous ne d velopperons pas dans cette introduction math
66. une d monstration est obtenue elle est correcte mais l chec d une tactique ne prouve pas que V nonc est faux Une diff rence importante entre la preuve et d autres taches plus classiques comme par exemple la conception de programmes est donc la possibilit d aboutir par le travail au tomatique d un ordinateur Pour cette raison il est toujours souhaitable de faire travailler les prouveurs automatiques sur les projets d montrer quel que soit le temps de calcul n cessaire parall lement au travail de preuve manuel Les tactiques employ es en preuve automatique sont g n ralement d autant plus cotiteuses en temps de calcul qu elles sont capables de trouver des d monstrations complexes De plus les tactiques les plus compl tes peuvent souvent provoquer des boucles infinies dans les d monstrations C est pourquoi les diff rentes tactiques du prouveur de l atelier B ont t regroup es en forces Les diff rentes forces sont les suivantes Force Temps indicatif par lemme performance 0 toujours moins de 10 secondes 70 1 de quelques secondes 2 ou 3 minutes 1 2 de quelques minutes quelques dizaines de minutes 3 3 de quelques dizaines de minutes plusieurs heures 1 Rapide moins de trois secondes 30 Les temps ci dessus sont indicatifs ils concernent surtout les premi res obligations de preuve de chaque op ration En effet les obligations de preuve suivantes ont beaucoup d hy
67. valid e Deux cas peuvent se produire la r gle est d montr e automatiquement par les outils de preuve de r gles Le travail de validation est r duit sa plus simple expression Dans ce cas on peut ajouter sans soucis la r gle au fichier Pmm et l utiliser la r gle n est pas d montr e automatiquement Cela ne signifie pas que la r gle est fausse Simplement le prouveur de pr dicats et le prouveur arithm tique n ont pas r ussi d montrer la justesse de cette r gle Cela peut tre d au fait que certains op rateurs B ne sont pas manipul s de mani re efficace par le prouveur de pr dicats par exemple closure ou bien encore que les heuristiques utilis es pour la preuve ne sont pas suffisamment efficaces dans ce cas La r gle doit alors tre d montr e manuellement Des l ments de d monstration doivent tre donn s par le concepteur de la r gle afin de tracer le raisonnement ayant servi sa cr ation Ces l ments de d monstration permettront un relecteur de s assurer de la justesse de la r gle On peut tre plus exigeant et r diger une d monstration math matique compl te de la justesse de la r gle en se reportant l axiomatique du B Book Dans tous les cas une relecture par un tiers s av re n cessaire car selon notre exp rience il est tr s facile de cr er une r gle fausse sans que l on s en apercoive 9 3 2 Simplification des lemmes Un but trivial peut
68. vitons ainsi de nous retrouver en train de reconstruire un prouveur automatique d di notre preuve partir de r gles manuelles complexes Une autre remarque importante est que nous n avons pas fait toute la d monstration manuellement Nous nous concentrons sur les parties d licates en d chargeant tous les buts faciles par la commande pr Une telle d monstration est la fois plus facile et plus s curitaire qu une d monstration manuelle cette derni re tant souvent fastidieuse quand on s interdit les raccourcis intuitifs inacceptables dans une preuve formelle Chapitre 9 Questions fr quemment pos es 9 1 Pr peut nous engager dans une mauvaise voie pour la preuve Il y a une diff rence fondamentale entre la commande mp et la commande pr Quelque soit la force de prouveur utilis e la commande mp applique des r gles de simpli fication du but et des hypoth ses ainsi que quelques m canismes de r solution La commande pr est construite selon les m mes principes mais elle contient d autres m canismes En particulier des heuristiques de simplification des pr dicats existentiels de traitement des derni res galit s mont es en hypoth ses et le d clenchement de preuves par cas Ces ajouts rendent cette commande plus performante dans la plupart des cas Par exemple si le but courant est de la forme ES et que l hypoth se e AUa existe alors la preuve courante est d coup e en 2 cas LEE gt aE
69. 3 4 amp gt xx 1 ETATS On ex cute d abord mp afin que les hypoth ses soient mont es dans la pile des hypoth ses Le but devient PRI gt mp Starting Prover Call xx 1 ETATS En examinant les hypoth ses on s apercoit que le domaine de xx 1 est d pendant de la valeur de xx Il faut donc d clencher une preuve par cas pour xx d crivant toutes les valeurs de l ensemble num r s ETATS PRI gt dc xx ETATS Do Cases on Enumerated E2 E1 E0 xx E2 gt xx 1 ETATS Le premier but xx ETATS a t trivialement d montr par le prouveur Les 3 cas vont maintenant tre g n r s Il faut r soudre le premier d entre eux ax E2 gt xx l ETATS On peut r aliser un appel au prouveur automatique mp ou pr On peut aussi r aliser un appel au prouveur de pr dicats pp rp 0 condition d ajouter l hypoth se locale xx E2 xx 1 e El E2 INDICATIONS UTILES POUR LA PREUVE 127 avec la commande ah PRI gt ah xx 1 E1 E2 Starting Add Hypothesis xx 1 E1 E2 gt xx 1 ETATS L appel au prouveur de pr dicats permet de d montrer ce premier but puis de passer au second cas PRI gt pp rp 0 Starting Predicate Prover Call Proved by the Predicate Prover xx El gt xx 1 ETATS On ajoute l hypoth se xz E1 gt 11281 E0 El E2 puis on active le prouveur de pr dicats PRI gt st Next step ah xx 1 E0 E1 E2 Starting Add Hypothesis xx 1 FO E1
70. Atelier B Prouveur interactif Manuel Utilisateur version 3 7 LEN DA CLEARS Y SYSTEM ENGINEERING ATELIER B Prouveur interactif Manuel Utilisateur version 3 7 Document tabli par CLEARSY Ce document est la propri t de CLEARSY et ne doit pas tre copi reproduit dupliqu totalement ou partiellement sans autorisation crite Tous les noms des produits cit s sont des marques d pos es par leurs auteurs respectifs CLEARSY Maintenance ATELIER B Parc de la Duranne 320 avenue Archim de Les Pl iades III Bat A 13857 Aix en Provence Cedex 3 France T l 33 0 4 42 37 12 99 Fax 33 0 4 42 37 12 71 email maintenance atelierb clearsy com Table des matieres 1 Introduction 2 Rappels de preuve formelle 2 1 Les symboles 2 2 Le raisonnement formell 4 ee 2 3 Le calcul propositionnell 2 4 Les pr dicats quantifi s 3 Introduction au prouveur 3 1 Approche pratique 3 1 1 Un exemple 3 1 2 La preuve automatique 3 1 3 Le prouveur interactif 3 1 4 L outil de preuve en g n ral 4 M thode g n rale 5 4 1 Les phases de preuve 4 2 L utilisation des forces du prouveur 4 3 Les lemmes de bonne d finition La phase de mise au point 5 1 La m thode g n rale de mise au point 3 1 5 D tail des principales fen tres 3 1 6 Echanges avec le prouveur interacti 3 2 Le
71. B Il faut rechercher une contradiction dans LEAN ACBA LA PHASE DE PREUVE FORMELLE 73 x B Transformation en pr dicats quantifi s TEAN Vy ye A gt yeB A x B En instanciant par x la deuxi me hypoth se TEB Ce qui est en contradiction avec la derni re hypoth se Les performances de ce proc d peuvent tre pressenties sur cet exemple les chances d aboutir sont grandes m me si la d monstration est math matiquement complexe mais il faut un nombre r duit d hypoth ses pour viter des probl mes de saturation li s l ex pansion importante lors de la transform e en pr dicats quantifi s Les choix d instanciation possibles sont nombreux ce qui donne des temps de preuve parfois longs D autre part ce proc d n est pas tr s adapt aux d monstrations arithm tiques Le prouveur de pr dicats de l Atelier B est fond sur ce principe c est lui qui a permis la validation de la base de regles math matiques du prouveur principal Il s utilise par la commande PredicateProver que nous allons tudier La commande PredicateProver En preuve interactive il est toujours possible de lVutiliser pour tenter de prouver une branche de preuve c est la commande PredicateProver pp qui lance le prouveur de pr dicats sur le lemme courant ventuellement all g d hypotheses avec un temps maxi mum Nous conseillons l utilisation suivante Si le lemme est d montrable sans notions ari
72. FALSE si on 1 FALSE f est vide l limination de la restriction est imm diate si on l TRUE f l_wpok gt TRUE Le raisonnement est un peu plus com plexe il fera intervenir des r gles de typage d une fonction co restreinte Dans une d monstration intuitive il n est pas n cessaire de tout d velopper il suffit de faire apparaitre les r gles essentielles utilis es une fois la restriction limin e nous avons deux termes litt ralement gaux r gle em ploy e d finition de l galit Au cours de ce processus il faut faire attention aux pi ges classiques que nous num rons ci apr s Pi ges classiques priorit gt et A l implication est moins prioritaire que la conjonction Par exemple AN B gt CA D sera compris comme A A B C D Pour viter une mauvaise interpr tation mettre des parenth ses par exemple crire A A B gt Cy A D intervalles vides un intervalle peut tre vide si sa borne de gauche d passe celle de droite Par exemple aa aa bb n est pas toujours vrai ajout de divergences une fonction si ff est une fonction l objet obtenu en ajoutant des couples a ff n est plus forc ment une fonction En effet l un des couples ajout s peut avoir le m me l ment de d part qu un couple existant de ff dans ce cas ff est transform e en une relation division enti re en B le symbole d signe la division en
73. Ne jamais ou blier de tenter un appel au coeur de preuve sur un but avant de faire des commandes interactives pour le d montrer PredicateProver pp cette commande appelle le prouveur de pr dicats sur le lemme courant Le prouveur de pr dicats voir paragraphe 6 2 4 agit souvent avec succ s sur des buts compos s d expressions ensemblistes ou fonctionnelles Penser Predica teProver si le but est uniquement compos d expressions ensemblistes ou fonctionnelles Les commandes de preuve sans ajout de r gle Les commandes suivantes sont celles qui permettent de faire aboutir des preuve sans ajout de r gle manuelles ou contr l es par le prouveur de pr dicats AddHypothesis ah op rateur peut proposer de nouvelles hypoth ses qui seront ajout es aux hypoth ses existantes apr s d monstration de l hypoth se propos e Cette commande permet donc d ajouter des hypoth ses superf tatoires Ces hypoth ses sont saisies par l op rateur qui peut ainsi introduire de l information suppl mentaire dans la preuve en apportant le b n fice de son intuition et de son imagination AddHypothesis est l une des commandes de preuve les plus importantes elle permet de diriger la preuve en faisant d montrer des buts interm diaires partant des hypoth ses afin de s approcher du but principal Une autre utilisation est de refaire passer les hypoth ses dans le prouveur voir paragraphe 6 7 2 Penser AddHypothesis d s qu
74. RMELLE 87 Force 0 dd New Hypothesis since last command Goal tconnait ntt tconnait tt tt 0 pass tident tt 0 End PRI gt pp Starting Prover Predicate Call Proved by the Predicate Prover Current PO is fork 6 Proved saved Unproved Command line is Force 0 pr Red dc ntt tt 0 amp pr Red pp pr Red amp pp Next Saved line pos 1 Force 0 dd Hypothesis Goal Local hypotheses amp ntt TACHES amp not ntt taches amp tt 0 taches ntt amp Check that the invariant tt tt gt tconnait ntt tconnait tt tt 0 pass tident lt ntt gt tident tt tt 0 End Nous pouvons quitter le prouveur interactif et l Atelier B Notons que la commande h du mode batch permet d obtenir la liste des commandes disponibles PRI gt qu PO fork 6 saved bbatch 6 gt h General commands 88 Prouveur interactif Manuel Utilisateur cd change_directory ddm disable_dependence_mode erf edit_res_file eur edit_users_res edm enable_dependence_mode h help hh html_help hph html_prover_help hrb html_rules_base 1sb list_sources_b 1rf load_res_file pc print_code pwd print_working_directory q quit rs restore_source srb show_rules_base v version_print Project level commands add add_definitions_directory apl add_project_lib apr add_project_reader ap
75. S LEA A notlx a gt 1ES Autre exemple si la formule dom A x B appara t dans le but courant P alors 2 cas vont tre g n r s B S gt dom Ax B 9 P A not B gt dom A x B AJP f g P signifie ici que toutes les occurrences de f dans P sont remplac es par g Toutefois le d clenchement de preuves par cas peut s av rer inutile et n cessiter de prou 155 156 Prouveur interactif Manuel Utilisateur ver un lemme autant de fois qu il y a de cas En effet ces preuves par cas se d clenchent selon certains crit res locaux qui peuvent ne pas correspondre au type de preuve qu il faudrait r aliser Par exemple si le lemme se d montre par contradiction plusieurs hypoth ses sont contra dictoires le d clenchement d une preuve par cas va multiplier inutilement le nombre de lemmes a d montrer par contradiction Il est donc conseill de tenter en preuve interactive la commande mp avant la commande pr Si mp choue on v rifie alors si pr permet de conclure ou de transformer le but en une forme plus facilement prouvable 9 2 Utilisation d un plan de preuve La r daction d un plan de preuve avant de commencer une d monstration interactive est n cessaire si l on veut que cette preuve soit la plus courte et la plus productive possible Il faut bien entendu s tre assur au pr alable que l obligation de preuve que l on veut d montrer est juste Cela se fait par inspection visuel
76. a preuve sans risque de cas exploratoires La m thode g n rale pour faire les d monstrations formelles est la suivante LA PHASE DE PREUVE FORMELLE 57 But pr ou pp oui succ s non ba et pr Red oui lt but plus simple non commande interactive G 18 E TE O 1 Nouveau but Ce sch ma explique comment avancer dans la preuve en traitant chaque nouveau but qui se pr sente Quand il ne reste plus de but traiter la preuve est finie D taillons les tapes Etape 1 Pour chaque nouveau but il faut lancer le prouveur pour ne jamais perdre de temps s il est automatiquement d montr Il ne faut pas faire cette tape lors qu il est certain que le prouveur ne peut pas aboutir c est le cas en particulier du but de d part Sa preuve choue forc ment puisque l obligation de preuve n a pas t d montr e automatiquement Penser aussi essayer la commande pp cette tape ventuellement pr c d e de dd pour faire monter des hypoth ses rappelons comme nous l avons vu dans le chapitre pr c dent que le prouveur de pr dicat r agit g n ralement mieux si toutes les hypoth ses sont mont es Etape 2 Si la derni re branche de preuve est d charg e nous avons obtenu un nouveau but Sinon nous passons l tape 3 Etape 3 La pr c dente commande peut avoir tent des pr
77. a servi fabriquer une nouvelle hypoth se il s agit donc d une sorte de g n ration par l avant Il aurait t possible de fabriquer une r gle forward pour obte nir le m me r sultat mais celle ci serait moins simple Le proc d utilisant l ajout d hy poth se nous permet d exploiter facilement une r gle crite uniquement en fonction de consid rations math matiques Nous avons introduit l intervalle de variation du reste mais le prouveur ne peut pas encore aboutir sans utiliser la premi re r gle de la th orie IntDiv b a b a a mod b Si nous utilisons la commande pr il est clair que le but courant ne va pas tre d charg Il est n anmoins utile que le prouveur simplifie la nouvelle hypoth se et commence la preuve en simplifiant le but Pour faire tout ceci sans d marrer des preuves par cas exploratoires nous pouvons utiliser pr Red PRI gt pr Red Starting Prover Call Le but devient 0 lt 1 nc1 nc2 2x nc1 nc2 2 ETUDES DE CAS 149 Comme pr vu le prouveur a simplifi le but et limin l intervalle en produisant deux sous buts L hypoth se a bien t simplifi e et charg e elle appara t en bas de la liste d hypoth ses Nous devons maintenant utiliser la premiere r gle de IntDiv Il s agit d une r gle de r ecriture pour laquelle la commande ApplyRule ar poss de les modes Goal r ecriture dans le but et Hyp AllHyp et Hyp h r ecriture dan
78. ace pour la preuve interactive simule donc toujours un dialogue en mode ligne avec le prouveur dialogue que l op rateur peut avoir directement depuis la zone des com mandes en ligne Toutes les op rations peuvent tre faites depuis cette zone commande de preuve positionnement mais il faut conna tre la syntaxe de chaque commande Ta pez help pour obtenir la liste des commandes disponibles Ces commandes sont toujours compos es de deux lettres minuscules qui sont les premi res lettres des mots composant le mn monique de la commande Par exemple La commande Search Hypothesis s crit sh S il n y a qu un seul mot dans le mn monique la commande est form e de ses deux premieres lettres par exemple ne pour Next ou qu pour Quit Ces commandes prennent souvent des arguments utilisant des mots clefs comme Goal A11Hyp des dialogues par boutons pourraient viter d avoir employer ces mots clef INTRODUCTION AU PROUVEUR 21 3 2 Le principe de la preuve interactive Comment les commandes voqu es pr c demment peuvent elles faire aboutir une preuve qui choue lorsqu elle est lanc e en mode automatique Comment pourrez vous piloter une preuve vers son succ s avec ces commandes Ce sont les questions auxquelles nous allons r pondre dans ce paragraphe Nous montrons le principe de ce pilotage sur un exemple Soit d montrer le lemme suivant xx El1 10 A y E2 10 A 22 3 10 gt max xx yy z
79. aisonnement math matique effectu D une mani re g n rale toutes les jus tifications recueillies lors de la mise au point du composant facilitent les phases de preuve ult rieures Nous allons maintenant examiner plus en d tail comment viter de consid rer tort des obligations de preuve comme fausses 5 8 1 S assurer que l obligation de preuve est bien fausse Pour viter des modifications nuisibles dans le composant il faut v rifier que l obligation de preuve qui semble fausse l est vraiment Pour cela il faut consid rer les points suivants V rifier que Pobligation de preuve n est pas rendue vraie par la pr sence d hypotheses contradictoires il est normal que de telles PO apparaissent elles traduisent l application rigoureuse de la th orie Les buts de ces obligations de preuve n ont pas tre vrais il peuvent m me tre d pourvus de sens Dans tous les cas la contradiction dans laquelle on se place correspond des branches du composant et de son niveau sup rieur c est en se guidant sur ces branches qu il faut chercher la contradiction Chercher un contre exemple chercher des valeurs particuli res des variables qui v rifient les hypoth ses mais pas le but On fera attention aux points suivants chercher utiliser les valeurs 0 et elles permettent souvent de fabriquer des contre exemples simples si il y a beaucoup d hypotheses chercher le contre exemple uniquement s
80. alll BackwardRule regle 1 A binhyp H A H gt B gt B bcalll BackwardRule regle 2 A binhyp H A bgoal C gt D A H gt B ok gt B peuvent s appliquer une infinit de fois Il est possible d viter ce ph nomene en appliquant les r gles de mani re unitaire ar regle 1 Once au lieu de ar regle en gardant les r gles L ajout de la garde bnot bsearch H C R permet d viter un bouclage par la commande ar Par contre un appel 4 pr Tac regle provoque un bouclage En r gle g n rale il faut viter d ajouter des hypotheses de cette mani re On pr f rera utiliser des r gles forward 9 9 Utilisation de pp rp 0 Le prouveur de pr dicats n utilisant que le but courant sans aucune hypoth se commande pp rp 0 se r v le tr s efficace l utilisation pour d montrer des lemmes interm diaires En effet pp est particuli rement efficace quand le nombre d hypoth ses est peu lev On peut consid rer que son efficacit d cro t de fa on exponentielle lorsque le nombre d hy poth ses croit Aussi on se contente de s lectionner les hypoth ses qui permettent de d montrer le but par la commande ah puis on applique la commande pp rp 0 Le domaine d utilisation de pp est lemmes arithm tiques hors et modulos propositions ensembles pr dicats quantifi s Certains symboles sont moins bien manipul s par pp au niveau de la
81. ants La preuve interactive se fait en force 0 Il est toujours possible d utiliser des forces plus lev es en preuve interactive mais cela se justifie rarement rappelons qu il faut environ une minute pour charger 100 hypoth ses en force 1 contre moins d une seconde en force 0 Le gain en performance dans l optique d une d monstration interactive c est dire guid e par l op rateur ne justifie pas ce co t On acc de en interactif une PO en la remettant en force 0 par gr GotowithReset Pour repasser en force 0 sur une obligation de preuve charg e il suffit d utiliser la commande ff 0 D marrer avec une d monstration intuitive Dans la phase de mise au point la PO concern e a du tre visit e une justification et une d monstration intuitive ont t faites Il faut repartir de cet tat En principe des notes auront t prises dans ce but en phase de mise au point I faut refaire le raisonnement intuitif La suite de ce chapitre est d coup e de la mani re suivante Introduction la preuve interactive les notions essentielles d utilisation de cet outil y sont expliqu es En particulier les commandes sont pr sent es dans l ordre d impor tance Utilisation de l interface le prouveur interactif fonctionne avec une interface Motif dont Vutilisation est pr sent e dans ce paragraphe La ligne de commande ce rep re essentiel pour la preuve est d taill dans ce paragraphe
82. aragraphe 6 3 2 GotoWithoutsave gw rarement utilis e cette commande permet de quitter une obligation de preuve sans aucune sauvegarde SavewithQuestion sq provoque la sauvegarde de la ligne de commande courante en demandant confirmation l op rateur si il n est pas clair que le remplacement de la d monstration sauv e par la d monstration courante soit b n fique par exemple si aucune des deux d monstration n aboutit 6 2 2 Les r gles et leur usage Une preuve math matique formelle se fait en utilisant des r gles math matiques Par exemple on d montre pes gt tAq s gt t gt dom p dom q C dom p q LA PHASE DE PREUVE FORMELLE 65 en utilisant la d finition de l inclusion dom p dom q E dom p q Vx x dom p dom q x dom p q puis la d finition du domaine d une relation etc Le math maticien fait souvent des d monstrations sans citer explicitement toutes les r gles qu il utilise N anmoins le choix des r gles consid r es comme autoris es est important pour savoir ce qu on appelle une d monstration correcte Il serait trop facile de pr tendre que le lemme d montrer est toujours une r gle autoris e Dans une d monstration B les r gles autoris es sont celles de la th orie de construction du langage voir B Book et celles de la base du prouveur Comment de telles r gles math matiques peuvent elles tre traduites en quelque chose
83. arting Do Cases Current PO is fork 6 Unproved saved Unproved Command line is Force 0 pr Red dc ntt tt 0 amp Next Saved line pos 1 Force 0 dd New Hypothesis since last command Goal ntt tt 0 gt tconnait ntt tconnait tt tt 0 pass tident lt ntt gt tident tt tt 0 End PRI gt pr Red Starting Prover Call Current PO is fork 6 Unproved saved Unproved Command line is Force 0 pr Red dc ntt tt 0 amp pr Red Next Saved line pos 1 Force 0 dd 86 Prouveur interactif Manuel Utilisateur New Hypothesis since last command ntt tt 0 amp not tt tt 0 Y not tt 0 tt pass tident tt ran pass amp pass tident tt PASSWORDS Goal tconnait tt o tconnait tt tt 0 pass tident tt End PRI gt pp Starting Prover Predicate Call Proved by the Predicate Prover Current PO is fork 6 Unproved saved Unproved Command line is Force 0 pr Red dc ntt tt 0 amp pr Red pp Next Saved line pos 1 Force 0 dd Hypothesis Goal not ntt tt 0 gt tconnait ntt tconnait tt tt o pass tident lt ntt gt tident tt tt 0 End PRI gt pr Red Starting Prover Call Current PO is fork 6 Unproved saved Unproved Command line is Force 0 amp pr Red amp dc ntt tt 0 pr Red amp pp amp pr Red amp Next Saved line pos 1 LA PHASE DE PREUVE FO
84. atiquement le but Le c ur de preuve est pr vu pour obtenir les meilleurs r sultats possibles en preuve auto matique c est pourquoi il tente des tactiques exploratoires avant de conclure l chec Ces tactiques sont nuisibles en preuve interactive quand elles chouent car elles conditionnent le but en chec Le plus souvent il s agit de preuves par cas comme dans l exemple ci apr s Soit prouver une obligation de preuve de la forme HN pbs do B si le prouveur choue dans la d monstration il peut d cider de faire deux cas p et p pour tenter de tirer parti de l hypoth se p q Si la preuve choue toujours le but en chec peut tre celui du cas p L op rateur poursuit la preuve interactive son aboutis sement seul le cas p aura t d montr et il restera traiter l autre cas Ce comportement est particuli rement g nant quand le prouveur tente des preuves par cas qui ne servent pas la d monstration dupliquant alors gratuitement la preuve Les preuves par cas ne sont signal es que par les hypoth ses de cas ce qui n veille pas facilement l attention de Vop rateur C est pourquoi il est recommand d employer la commande pr Red qui lance le prouveur sans les tactiques de preuve exploratoires plus pr cis ment lancer pr si la branche de preuve courante aboutit continuer sur le but suivant si la preuve choue reculer par Back ba et lancer pr Red pour avancer l
85. b parceque le solveur arithm tique met les coefficient les plus simples en premier Ecrire une telle r gle directement dans sa forme optimale n est pas chose facile cela n cessite de l exp rience N anmoins il est toujours possible d am liorer la forme de la r gle quant elle s av re peu pratique Nous introduisons ces r gles dans le fichier pmm du composant concern puis nous chargeons ce fichier en utilisant la commande PmmCompile pc Comment utiliser cette connaissance math matique dans notre exemple Pour nous a vaut ncl nc2 et b vaut 2 b est donc positif mais il faut faire deux cas suivant le signe de ncl nc2 il faut faire ces cas le plus tot possible et de toutes mani res avant que le but soit divis en deux sous buts Il ne serait pas logique de faire les deux cas ncl nc2 lt 0 et ncl ne2 gt 0 partir du but courant puisque ncl et nc2 sont d finis dans les hypoth ses locales Celles ci sont encore dans le but il n est donc pas possible de les utiliser avant leur mont e Nous avons deux moyens de faire monter les hypoth ses locales la commande Deduction dd les hypoth ses sont alors directement charg es sans in tervention du prouveur En particulier le prouveur ne peut pas r duire les identifiants utilis s au minimum comme il le fait sur les autres hypoth ses la commande Prove pr les hypoth ses sont alors charg es par le prouveur qui enchaine sur la preuve Le but
86. bsolue cette question Ce sera l utilisateur de d cider en final laquelle des deux options choisir en fonction de son exp rience et de ses pr f rences Il est toutefois possible de fournir des l ments de r ponse pour chaque approche une d monstration interactive pure sans ajout de r gle manuelle ne n cessite pas de v rification suppl mentaire mais peut exiger la r alisation de nombreux pas de preuve et se traduire par une dur e de preuve importante Il ne faut pas perdre de vue que ce travail de preuve peut s av rer co teux si des modifications des mod les B entra nent des pertes de d monstration par modification des obligations de preuve l ajout d une r gle permet souvent de gagner du temps en preuve interactive surtout si la base de r gles est insuffisante pour traiter le but d montrer Cette r gle ajout e devra par contre tre soigneusement d montr e par la suite de pr f rence par une personne diff rente du r dacteur afin d viter de d montrer des obligations de preuve fausses et invalider ainsi le d veloppement en cours 118 Prouveur interactif Manuel Utilisateur 7 2 4 Utilisation dans les tactiques de preuve pp rp 0 peut tre utilis dans la User_Pass Il faut alors introduire dans le fichier PatchProver localis dans le r pertoire bdp du projet ou dans le fichier Pmm du compo sant la th orie User_Pass puis indiquer une tactique de preuve par ligne S
87. but de sortie convienne pour l application de la r gle OrderX Y 63 Donc la commande ApplyRule va tre refus e l tat final sera Force 1 amp pr amp pr amp Next La commande ApplyRule est perdue C est pourquoi il faut imp rativement sauver la liste des commandes avant de changer de force La m thode suivre est la suivante sauver la d monstration en force 0 par sw LA PHASE DE PREUVE FORMELLE 113 revenir au d but de la d monstration par re passer en force sup rieure commande ff x prouver en force sup rieure tenter un appel au c ur de preuve pr ventuellement reprendre des commandes de l ancienne d monstration commande st en cas d chec revenir en force O par re ff 0 et refaire la d monstration pr c dente par st End D autre part si une d monstration interactive en force 1 est sauvegard e sur une obligation de preuve l acc s interactif cette obligation provoque un passage en force 1 Il faut donc viter de sauvegarder inutilement en force 1 pour ne pas ralentir sans raison les acc s 6 8 4 Les problemes de chargement v rifiez les messages de chargement apr s avoir charg le prouveur interactif et avoir acc d la premi re PO non prouv e commande Next il est possible de remonter au d but de la fen tre de commandes pour voir les messages de chargement d un ventuel fichier de r gles manuelles ou prouv es par le prouv
88. but devient 0 lt 1 nc1 nc2 2x ncl nc2 2 Comme pr cedemment nous utilisons la premi re r gle de IntDiv PRI gt ar IntDiv 1 Goal Starting Apply Rule Le but devient 0 lt 1 ncl nc2 ncl nc2 ncl nc2 mod 2 Tout est pret nous pouvons lancer la preuve automatique PRI gt pr Starting Prover Call Le but devient ncl nc2 lt 0 gt ncl ncl nc2 2 nc2 ncl nc2 2 1 1 Ce but est le deuxi me cas la preuve si ncl nc2 est positif Nous avons donc fini la moiti de la preuve principale l arbre de preuve est affich dans la zone ligne de commande Force 0 amp dd amp dc nci nc2 lt 0 amp dd amp ah nc1 nc2 mod 2 1 2 0 amp ar IntDiv 4 0nce amp pr amp pr amp pr amp pr Red amp ar IntDiv 1 Goal amp pr amp pr Red amp ar IntDiv 1 Goal amp pr amp Next Le mot clef Next est le deuxi me indent imm diatement sous la commande dc il s agit donc du deuxi me cas cette preuve par cas L hypoth se locale ncl ncl lt 0 indique que nous supposons maintenant ncl nc2 positif Nous sommes revenus en dessous de la commande ah par laquelle nous avions indiqu Vintervalle de variation du reste Cet intervalle de variation n est effectivement plus le ETUDES DE CAS 151 m me nous devons donc le pr ciser nouveau dans le cas o ncl nc2 est positif La r gle qui convient est a NATURAL amp b NATURAL amp n
89. c x lt z avec le filtre T TT z D Les nouveaux buts sont produits x lt y produit le but xx lt y y lt z produit le but y lt 5 Notons que le joker y qui n est pas instanci reste tel quel dans ces nouveaux buts Mal heureusement aucune variable du lemme d montrer ne s appelle y en une seule lettre ces buts sont donc d pourvus de sens car ils utilisent une variable non d finie La r gle consid r e ne convient donc pas pour d montrer ce lemme Pour r soudre ces cas il faut pouvoir crire des r gles qui vont rechercher directement dans les hypoth ses on utilise des fonctionnalit s sp cifiques du langage de th orie appel es gardes Le langage de th orie propose une trentaine de gardes dont la plupart ne sont pas int ressantes dans le cadre de la preuve interactive Nous nous limiterons aux gardes expos es ci apr s Le principe d une garde est d effectuer une op ration informatique apr s que le but ait co ncid avec le cons quent de la r gle mais avant la g n ration de nouveaux buts Cette op ration informatique peut avoir diff rents effets mais elle retourne toujours 68 Prouveur interactif Manuel Utilisateur VRAI ou FAUX La r gle ne s applique que si le r sultat est VRAI La liste des gardes utiles pour la preuve est la suivante binhyp permet de rechercher une hypoth se Par exemple binhyp z lt y A y lt z gt TAZ Cette r gle s applique sur l exemple suivant
90. ce Elle a deux usages principaux le contr le des cas le coeur de preuve d cide parfois de faire de la preuve par cas pas toujours judicieusement La r gle d admission permet de conna tre ces cas Par exemple pr 8 ar Admis 1 0Once ar Admis 1 0Once ar Admis 1 Once amp Next Le premier appel au coeur de preuve avait fait trois cas Voir paragraphe 6 8 1 la validation de l utilit d une hypoth se ajout e la commande AddHypothesis per met l ajout d une hypoth se d montrable partir des hypoth ses existantes Cette d monstration peut tre complexe il vaut alors mieux tre s r de l utilit de l ajout avant de la faire Par exemple ah not xx el amp ar Admis 1i 0nce pr amp Next L utilit de l hypoth se xx el tant ainsi tablie on peut revenir en arri re et faire sa d monstration L usage de la r gle d admission oblige faire des retours en arri re pour reprendre la d monstration voir paragraphe il y a quelques pr cautions prendre La r gle d admission est parfois utilis e en phase de mise au point voir paragraphe Pour des raisons de division des t ches il peut tre utile de cr er des r gles d admission r duites qui ne peuvent agir que sur certaines obligations de preuve Par exemple LA PHASE DE PREUVE FORMELLE 101 THEORY Admis IS binhyp C operationi n amp bcall WRITE bwritef A
91. cement les commandes de lecture les commandes de preuve automatique les commandes de preuve sans ajout de r gles les commandes d ajout de r gles prot g es les r gles manuelles la g n ralisation les commandes de preuves s appliquant dans des cas particuliers les autres commandes Nous allons maintenant rentrer dans le d tail de ces rubriques Les commandes de d placement Les commandes ci apr s permettent de se d placer dans les preuves Il est difficile de leur donner un ordre d importance car elles sont toutes n cessaires pour utiliser le prouveur interactif Goto go permet de se positionner sur une obligation de preuve Avec l interface LA PHASE DE PREUVE FORMELLE 61 Motif il est normalement plus simple de double cliquer sur la PO dans la liste cette commande est donc surtout employ e en mode batch voir paragraphe 6 3 2 Dans ce mode elle est absolument n cessaire Next ne passe la prochaine PO non prouv e Back ba annule l effet de la pr c dente commande interactive ayant agit sur la preuve Elle est beaucoup utilis e apr s un appel au coeur de preuve qui a chou conform ment a la m thode d crite au d but de ce chapitre Utiliser Back pour liminer les commandes inutiles ou pour replacer une action interactive avant l action courante GotowithReset gr cette commande permet d aller sur une obligation de preuve en
92. chaque obligation de preuve en utilisant la m thode du paragraphe paragraphe Ces deux tapes seront examin es en d tail dans la suite de ce chapitre Pour l instant nous allons tudier les m thodes pratiques de visualisation d obligations de preuve avec l Atelier B 5 2 M thodes de visualisation des obligations de preuve Pour faire d filer les obligations de preuve non d montr es par la force 0 du prouveur il y a deux m thodes Par le PO Viewer utiliser le PO Viewer de l Atelier accessible par le menu Status Show Print PO de la fen tre principale Le PO Viewer est un simple visualisateur d obligations de preuve sans traitement Par le prouveur entrer dans le prouveur interactif et pour chaque PO visualiser faire dd Deduction pour monter les hypoth ses locales et rp ReducedPo visualisation r duite aux hypoth ses qui ont un symbole en commun avec le but LA PHASE DE MISE AU POINT 31 Le PO Viewer est d acc s plus rapide que le prouveur interactif En effet il ne contient aucune base de r gle ou tactique de preuve c est seulement un afficheur il est donc beaucoup plus l ger que le prouveur L usage du prouveur comme visualisateur de PO s impose dans les cas suivants Hypoth ses complexes si la structure du composant est telle qu il va y avoir plus de 200 hypoth ses environ et que les hypoth ses int ressantes pour chaque obligation de preuve risquent de ne pas tr
93. che de la meilleure forme a donner aux expressions du composant pour faciliter la preuve sans se concentrer sur la justesse des obligations de preuve phase finale mise au point complete L interpr tation des buts est l une des cing tapes de l examen d une obligation de preuve que nous allons voir maintenant 5 4 L examen d une obligation de preuve Attention avant de proc der l examen d une obligation de preuve assurez vous que vous avez choisi cette obligation de telle mani re commencer par celles qui ont le plus de chances de d tecter des erreurs comme expliqu au paragraphe pr c dent Dans la phase de mise au point il faut obtenir le plus rapidement possible la d monstration intuitive de chaque obligation de preuve Nous allons commencer par pr senter les principes de l examen d une obligation de preuve puis nous verrons comment parcourir et comment visualiser ces obligations de preuve La m thode d examen d une obligation de preuve est la suivante 1 interpr tation du but examiner les diff rentes variables pr sentes dans le but 38 Prouveur interactif Manuel Utilisateur et retrouver le sens de chacune d entre elles dans son interpr tation physique voir paragraphe 5 4 1 2 justification intuitive d terminer pour quelles raisons ce but doit tre vrai dans le contexte du composant voir paragraphe 5 4 2 3 s lection des hypoth ses isoler dans l obligation de pre
94. chines vues ou incluses pour une implantation ce sont le raffinement sup rieur et les machines import es Puisque la preuve automatique a pu d charger les obligations de preuve concernant des parties enti res du composant il suffit de lire une partie res treinte du composant on se rep rera au nom de l op ration rappel e dans les barres de label des fen tres du prouveur et au but Dans les paragraphes qui suivent nous allons voquer rapidement l existence de certaines commandes du prouveur interactif sans faire une pr sentation g n rale de cet outil En effet pour la phase de mise au point il n est pas forc ment n cessaire de conna tre luti lisation compl te de toutes les commandes interactives Elles sont pr sent es en d tail au chapitre 6 qui traite de la preuve formelle Les cing tapes d examen d une obligation de preuve peuvent paraitre longues quand elles sont expos es en d tail comme dans ce qui suit En fait avec de l habitude chaque obligation se fait tr s rapidement en une ou quelques minutes sans s parer formellement chaque tape Ces tapes servent seulement attaquer les problemes dans le bon ordre Si une obligation de preuve semble fausse vous avez probablement trouv une erreur dans le source suivez les conseils du paragraphe 5 8 pour trouver et corriger l erreur INotons que m me quand le prouveur interactif est lanc il est possible d ouvrir les composants depuis V Ateli
95. d ex cutable sur une machine informatique Nous allons introduire quelques notions n cessaires pour comprendre cela Ces notions sont les fondements du langage de th orie sur lequel est bas le prouveur de l Atelier B Le langage de th orie est implant par une couche logicielle appel e Logic Solver Pour l utilisateur du prouveur il suffit de conna tre les quelques notions ci apr s pour pouvoir trouver une r gle dans la base math matique ou crire une r gle manuelle La totalit du langage de th orie est d finie dans le document LogicSolver Notion de co ncidence de formules Expliquons cette notion sur un exemple on dit que la formule aa bb cc x 12 co ncide match avec le gabarit template T YX2Z parce que le remplacement de x par aa y par bb cc et z par 12 permet d obtenir la formule partir du gabarit Dans un gabarit les identificateurs ne comportant qu une lettre ont un r le particulier elles remplacent n importe quelle formule On les appelle des jokers Ainsi aa bb co ncide avec aa x ou u v mais pas avec x aa Attention aussi aux parenth ses implicites aa bb cc coincide avec x y x sur aa bb et y sur cc car aa bb cc est compris comme aa bb cc Notion de r gle d inf rence Expliquons cette notion sur un exemple si le but prouver est bool aa 2 lt 10 bool xx lt 12 alors la r gle d inf rence suivante peut s appliquer
96. d monstration d autre obligations TryEverywhere te essai de la g n ralisation d une d monstration Elle permet d ex cuter la preuve d un ensemble d obligations de preuve en modifiant ou remplacant leurs lignes de commandes a partir d une s quence de commandes pass e en parame tre Utiliser TryEverywhere apr s le succ s d une d monstration si d autres PO semblent se prouver pareillement Les cas particuliers Les commandes suivantes s appliquent dans des cas de preuve particuliers useEqualityinHypothesis eh cette commande permet de remplacer a par A dans le but ou les hypoth ses lorsque a A ou bien a est en hypoth se Elle est utile d s que le prouveur ne fait pas un remplacement souhaitable si l galit est une hypoth se d riv e voir cette notion au paragraphe ou si on veut r crire une hypoth se ant rieure l galit et qui n a donc pas subi son action Penser useE qualityinHypothesis d s qu une galit doit tre utilis e dans le but ou une hypoth se SuggestforExist se lorsqu un but est de la forme 2x P x op rateur peut proposer des valeurs xq pour les variables x Le but devient alors P x0 s il est d montr le but existentiel initial est tabli car on a exhib une valeur qui v rifie le pr dicat En pratique c est dans 90 des cas la seule mani re de r soudre une PO existentielle Penser SuggestforExist d s que le but est existenti
97. de se localiser dans l arbre de preuve savoir ce que l on est en train de d montrer d terminer le chemin parcouru et le reste a faire minimiser la taille de la d monstration interactive Par exemple il est pr f rable d ajou ter une hypoth se avant de lancer une preuve par cas plut t que de l ajouter successi vement pour chacun de ces cas QUESTIONS FREQUEMMENT POSEES 157 r utiliser des portions de d monstrations d une obligation de preuve l autre si par exemple les m mes hypoth ses doivent tre ajout es Il ne faut pas oublier de tenter un TryEveryWhere commande te d s que l on pense que la d monstration que l on vient de r aliser peut tre appliqu e avec succ s d autres obligations de preuve de l op ration ou du composant 9 3 Comment savoir s il faut ajouter une r gle manuelle Il n est pas toujours facile de savoir si un point donn de la d monstration il est pr f rable d ajouter une r gle math matique pour d montrer ou aider d montrer le but courant ou s il est pr f rable de continuer utiliser des commandes d orientation de preuve de simplification et de r solution du prouveur Plusieurs aspects sont prendre en consid ration et c est l utilisateur en fonction du contexte du d veloppement B qu il reviendra de d cider 9 3 1 Validation de la r gle Une r gle math matique ajout e par l utilisateur va devoir tre
98. de circulation seule la fen tre de situation globale sert L op rateur regarde l indi cateur du nombre de PO non d montr es restantes qui est au dessus de la liste des PO Il peut se d placer dans les PO par les boutons qui sont autour de cette liste En mode preuve l op rateur fixe son attention essentiellement sur la zone but et sur la zone de commande C est dans la zone de commandes qu il effectue ses recherches d hypoth ses commande sh la fen tre des hypotheses tant plus r serv e une lecture rapide et moins dirig e Apr s chaque commande de preuve l op rateur doit contr ler le nouvel tat de preuve dans la zone de la ligne de commandes gauche voir paragraphe 6 4 Durant une preuve il arrive souvent que la lecture d une partie du composant ou de l un de ses niveaux adjacents soit n cessaire C est pourquoi il est conseill d avoir les fichiers correspondants en ic nes sur un bord de l cran Lorsqu une consultation est n cessaire il suffit d ouvrir ces fen tres qui viennent devant celles du prouveur apr s lecture il faut les remettre en ic ne pour ne pas interf rer avec l affichage de preuve Ces consid rations d affichage peuvent paraitre secondaires En fait elles influent sur la concentration de l op rateur et ont un impact important sur l efficacit obtenue La m thode d organisation de l affichage que nous pr sentons n est pas la seule possible l es sentiel est d
99. de d penser beaucoup de temps sur des obligations de preuve non essentielles et de d couvrir ensuite des erreurs dont la correction invalide les preuves pr c dentes Les commandes du prouveur interactif sont d crites en d tail dans le manuel de r f rence du prouveur Il n est pas n cessaire de lire cette r f rence enti rement pour pouvoir uti liser le prouveur en effet les commandes seront pr sent es dans le chapitre 6 par ordre d importance Il suffit alors de consulter le manuel de r f rence suivant les besoins Chapitre 4 M thode g n rale 4 1 Les phases de preuve Quelles sont les activit s de preuve dans le d veloppement d un projet informatique utili sant la m thode B et l Atelier B Etudions ceci sur un exemple soit un projet constitu d une seule machine abstraite la sp cification et de son implantation le programme concret Ce projet sera probablement r alis de la mani re suivante 1 Ecrire la machine abstraite en fonction du cahier des charges 2 Contr ler la formalisation correcte du besoin 3 Lancer le prouveur automatique sur cette machine abstraite 4 S il reste des obligations de preuve non automatiquement d montr es contr ler ra pidement qu elles soient justes Si certaines sont fausses la machine abstraite est incoh rente il faut la corriger Ecrire l implantation Relire cette implantation par rapport la machine abstraite Lancer le prouveur automa
100. dom tport lt taches is discharged because in hypothesis Le premier des deux sous buts est d charg Nous passons maintenant au deuxieme By applying atomic rule InPOWLeavesXY 35 binhyp ran r POW b gt ran a lt lt r POW b the goal ran tt lt lt tport lt PORTS is discharged End of trace LA PHASE DE PREUVE FORMELLE 107 Current PO is kill 5 Proved saved Proved Goal Check 4 gt tt lt lt tport taches tt lt gt PORTS End La d monstration est termin e Ces traces de preuve permettent de comprendre les d monstrations faites mais ne constituent pas une r daction math matique pour les raisons suivantes Les traitements pr liminaires sur les hypoth ses ne sont pas trac s Dans notre exemple l hypoth se ran tport P PORTS a servi Cette hypoth se ne provient pas directe ment du composant B il s agit d une hypoth se d riv e par les traitements pr liminaires qui n ont pas t trac s Les tentatives inutiles figurent dans la trace La trace part du but initial et le d compose dans l ordre d application des r gles Une d monstration math matique au contraire part des hypoth ses et arrive la conclusion par d monstration successive de r sultats interm diaires Le mode de trace est n anmoins d terminant pour faire l analyse d une preuve Il est galement possible d afficher la trace de preuve dans un graphe apr s avoir produit une t
101. e Prove ou ApplyRule qui boucle Ce bouton est invalid quand le prouveur est en attente d une commande op rateur c est le cas sur cette image D taillons les l ments de la fen tre centrale qui affiche le but et dans laquelle nous pouvons taper les commandes de preuve INTRODUCTION AU PROUVEUR 19 1 Zone du but 4 Nom du composant de l op ration et du num ro DemoExample Initialisation 3 GOAL Fa Current Goal bfalse 3 T moin de preuve es No current PO s BRI gt State of all PO Initialisation P01 Proved 3 2 3 4 P02 Proved 2 2 3 4 P03 Unproved 1 2 3 4 End No current PO PRI gt go Initialisation 3 Current PO is Initialisation 3 Unproved saved Unproved oa Check that the invariant few lt many is established by the imi tialisatton ref 3 3 1 2 3 4 n PRI gt pr Starting Prover Call Current PO is Initialisation 3 Unproved saved Unproved Goal bfalse 2 Zone des commandes en ligne wm ws An Vv Les l ments de cette fen tre sont 1 La zone du but elle contient le but courant affich dans une fen tre avec ascenseur horizontal Cette zone se colore en vert lorsque la d monstration aboutit Le t moin de preuve porte alors la mention Proved 2 la zone des commandes en ligne dans cette zone vous tapez toutes les commandes Il y a quatre sortes de commandes Les commandes d action ce sont le
102. e dans le composant il suffit de reporter dans le contexte du composant les raisons qui font que l obligation de preuve est fausse En particulier si on dispose d un contre exemple reporter les valeurs trouv es dans le composant Corriger l impact d une PO fausse varie du simple cas oubli la remise en cause du mod le math matique employ C est pourquoi la d tection des obligations de preuve fausses doit tre faite en continu il n est pas raisonnable de supposer ne plus avoir modifier les composants avant les phases de preuve Les corrections suite une PO fausse rel vent de la m thode B nous nous bornerons aux conseils suivants se demander si dans le sens physique attribu aux variables du mod le les valeurs qui rendent l obligation de preuve fausse sont possibles Si ce n est pas le cas l invariant est trop faible si on est amen renforcer un invariant trop faible s assurer que la nouvelle pro pri t est toujours vraie pour toutes les op rations En effet il arrive souvent qu une propri t physiquement vraie oubli e dans l invariant ne soit pas conserv e par des op rations dont le codage est biais par l invariant trop faible LA PHASE DE MISE AU POINT 53 avant de modifier un invariant s assurer que la modification rend juste l obligation de preuve fausse Ne pas faire de modification priori pour voir ce que cela donne dans les PO noter le r
103. e fonction les divisions par une expression potentiellement nulle size s tail s etc si s n est pas une s quence par exemple size 2 3 28 Prouveur interactif Manuel Utilisateur Chapitre 5 La phase de mise au point Les notions essentielles pr sent es dans ce chapitre sont les suivantes M thode g n rale apr s relecture et preuve en force 0 du composant parcourir et examiner les PO Les moyens de visualisation d une PO sont le PO viewer ou le prouveur interactif Avec le prouveur choisir la PO faire dd utiliser les fonctions de recherche Le parcours des obligations doit conduire en premier vers les PO difficiles Il faut parcourir la liste des obligations en remontant On peut faire plusieurs phases de parcours des obligations rapide finale ou bien rapide de simplification finale L examen d une obligation de preuve se fait en cing tapes lecture du but justification s lection des hypoth ses clefs d monstration intuitive notes et essais Lors de l examen d une obligation le composant B doit tre accessible Lecture du but il faut l interpr ter et isoler la contrainte v rifi e Justification utiliser le sens physique du composant S lection des hypoth ses chercher en remontant et utiliser les fonctions de recherche du prouveur D monstration intuitive reprendre la justification et voir les r gles employ es Notes et essais noter les simplificat
104. e limiter 5 commandes si le prouveur de pr dicats n a pas d charg l obligation tentez une d monstration partir des commandes standard du prouveur interactif Nous n allons pas expliquer comment faire ici c est l objet du chapitre 6 Nous dirons simplement que les deux commandes les plus fr quemment vues dans les d monstrations rapides sont AddHypothesis ah et DoCases dc Si vous n avez jamais utilis le prouveur interactif et si vous n avez pas encore tudi le chapitre 6 sur la preuve formelle vous ne ferez pas de d monstrations rapides lors de la mise au point de votre premier composant Dans ce cas il peut tre int ressant de faire la phase de preuve formelle juste apr s la mise au point de votre premier composant dans un but didactique m me si vous aviez pr vu une mise au point globale du projet entier En tous cas ne commencez jamais une phase de preuve formelle avant d avoir fait au moins la mise au point d un composant 5 6 2 G n raliser une d monstration La g n ralisation d une d monstration se fait par la commande TryEverywhere te Nous la d crivons ici car ce sont souvent les d monstrations rapides qui se g n ralisent Sauvez votre d monstration avant de la g n raliser par la commande Save Without question sw Sinon vous risquez de la perdre lors de la g n ralisation Utilisation de TryEverywhere te 0p 30 Replace Gen Unproved essayer d appliquer la d
105. e permet pas Plut t que de chercher une autre r gle pour changer les parenth ses nous conseillons la m thode suivante ah dom gg amp xx aa xx bb EE pr d monstration imm diate car le c ur de preuve remet la formule sous la forme qui est en hypoth se ar SimplifyRelOveXY 13 Goal notez l application en mode Goal qui signifie but l hypoth se ajout e tant encore dans le but Ce mode est r serv aux r gles de r ecriture Ainsi une transformation qui n cessite d viter les normalisations du prouveur peut elle tre faite LA PHASE DE PREUVE FORMELLE 111 6 8 Les pi ges viter L usage du prouveur interactif comporte malheureusement quelques cueils que nous al lons voir maintenant 6 8 1 Le contr le des preuve par cas Apr s chaque appel au c ur de preuve il faut contr ler que la preuve ne s est pas plac e dans un syst me de cas multiples inutiles Si cela se produit vous risquez d avoir r p ter la suite de la d monstration dans plusieurs branches de preuve ce qui est long Pour contr ler le nombre de cas le plus efficace est d utiliser une r gle d admission voir paragraphe 6 6 2 Si le c ur de preuve d marre des preuves par cas abusives utiliser la commande pr Red la place de pr ce mode propre la force O emp che les preuves par cas automatiques 6 8 2 Les num ros de r gles manuelles Les r gles d un fichier de r gles manuell
106. e preuve en moyenne pour les PO non d montr es auto matiquement est une bonne m trique Toutefois en fonction du type de modele et la mani re de mod liser il est possible d obte nir des PO complexes n cessitant l ajout de propri t s et ou la r alisation de preuve par cas Dans ce cas il est bien vident que 10 pas ne constitue pas une bonne valeur puisque sous estim e Pour certains d veloppements B il arrive que des d monstrations aient plus de 500 pas cause de preuves par cas contenant par exemple chacune de nombreuses commandes interactives presque identiques d un cas sur l autre on peut bien sur s inqui ter de la conservation de cette preuve lorsque les mod les voluent Un moyen de r duire la taille d une d monstration est de d complexifier le mod le B L autre moyen consiste ajouter une ou plusieurs r gles utilisateur Attention Elles doivent tre facilement v rifiables et ne pas tre trop sp cifiques 9 8 R gle qui ne s applique pas Lors de l utilisation de r gles par l interm diaire de la commande ar il faut se souvenir que si le but est de la forme A gt B A ne fait pas encore partie des hypoth ses il faut faire un dd pour cela Donc une r gle de la forme binhyp A gt B ne peut pas s appliquer tant que A n est pas une hypoth se Attention aussi a viter d employer des r gles bouclantes Par exemple les r gles QUESTIONS FREQUEMMENT POSEES 161 bc
107. e regroup es dans les derni res Dans ce cas les fonc tionnalit s de recherche du prouveur interactif seront utiles pour faire la s lection des hypoth ses obligations de preuve nombreuses pour une op ration si il y a plus de 100 PO pour une m me op ration alors l usage du PO Viewer risque d tre difficile car il visualise les obligations de preuve par op ration en une fois L affichage produit contient donc trop d informations 5 2 1 Visualisation avec le prouveur Si vous utilisez le prouveur interactif pour visualiser des obligations de preuve voici la m thode employer 1 Acc dez obligation choisie 2 Faites monter les hypoth ses locales 3 Utilisez les fonctions de recherche du prouveur interactif Pour expliciter ce paragraphe nous allons faire ces trois tapes en nous aidant de dessins qui repr sentent sch matiquement l cran de preuve Sur ces dessins seules les parties concern es seront repr sent es 1 Acc dez l obligation choisie choisissez l obligation de preuve lire ce choix est l objet du paragraphe suivant dans la liste de la fen tre de situation globale et cliquez deux fois dessus 32 Prouveur interactif Manuel Utilisateur INTERACTIVE PROOF HYPOTHESIS Initialisation PO1 Unproved GOAL PO2 Unproved PO3 Unproved xX Rappelons que la force influe grandement
108. el Les valeurs proposer se choisissent en regardant d o provient le but dans le composant plus que par examen de ce but qui est souvent sur plusieurs lignes FalseHypothesis fh si l une des hypoth ses est contradictoire avec les autres le but n a plus d int r t il suffit d tablir que les hypoth ses courantes tablissent la n gation de cette hypoth se L op rateur peut donc indiquer une hypoth se qu il croit contradic 64 Prouveur interactif Manuel Utilisateur toire le but devient alors la n gation de cette hypoth se Il n est pas possible de retirer Vhypoth se concern e pour qu elle n apparaisse plus que dans le but la commande fh ne le fait donc pas mais ce n est pas g nant le lemme r sultant est simplement vrai la fois par le but et par hypoth ses contradictoires Penser FalseHypothesis si la preuve d une PO vraie par hypotheses contradictoires choue Contradiction ct permet de faire de la preuve par contradiction La n gation du but monte en hypoth se et le but devient bfalse Ceci est particuli rement utile lorsque le but est de la forme not p car c est alors p qui monte en hypoth se et la pr sence de bfalse en but incite les m canismes du coeur de preuve rechercher une contradiction De plus si le but est de la forme not a b la r criture de a par b provoqu e par Vhypoth se a b peut mettre tr s facilement en vidence la contradiction Penser a Con
109. ement la m thode g n rale propos e dans ce chapitre devrait rendre implicite cette m thode puisqu elle stipule toujours l essai des commandes pr et pp avant tout autre La commande pp met 60 secondes chouer si elle ne permet pas de d montrer le but courant ce qui peut tre un peu long pour l essayer syst matiquement chaque nouveau 92 Prouveur interactif Manuel Utilisateur but C est pourquoi il arrive fr quemment qu on s apercoive apr s coup qu un sous but pouvait tre d montr par pp alors qu une autre d monstration plus complexe a t tent e Le lecteur se r ferera au paragraphe qui donne des indices pour pr voir quand pp a des chances d aboutir et aussi comment lancer pp avec un d lai plus faible ou sur des hypoth ses r duites 6 5 2 Ajout d hypoth ses et preuve par cas Les commandes d ajout d hypoth se AddHypothesis ah et de preuve par cas DoCases dc permettent d avoir une action d terminante sur la d monstration car elles donnent l op rateur la possibilit d introduire de nouvelles expressions Un exemple d ajout d hypoth ses Soit d montrer le lemme suivant cl E0 100 A c2E 0 cl A c9 E0 c2 A ch 0 CS gt cl c24 c3 c4 0 400 Le coeur de preuve en force 0 et le prouveur de pr dicats chouent sur ce lemme Conform ment a la m thode g n rale nous commencons par un appel au coeur de preuve en mode r duit PRI gt pr Red
110. en utilisant les r gles ajout es Nous ne savons pas encore comment cet l ment sera utilis mais il est clairement n cessaire Le moyen le plus simple pour indiquer cet intervalle de variation est l ajout d une hy poth se ncl nc2 mod 2 1 0 Le prouveur ne saurait pas d montrer cette nouvelle hypoth se puisque nous avons vu qu il n a pas les r gles n cessaires c est donc avec la r gle correspondante de la th orie IntDiv que nous allons le faire Cette r gle est ETUDES DE CAS 147 a lt 0 b NATURAL not b 0 gt a mod b 1 b 0 Pour pouvoir utiliser cette r gle il faut que le but prouver ait exactement la forme du cons quent de la r gle Nous allons donc ajouter hypoth se non simplifi e ncl nc2 mod 2 1 2 0 qui correspond pr cis ment notre r gle Les simplifications n cessaires seront faites apr s PRI gt ah nci nc2 mod 2 1 2 0 Starting Add Hypothesis Le but devient ncl nc2 mod 2 1 2 0 Il faut maintenant appliquer notre r gle qui est la quatri me de la th orie IntDiv Pour de telles r gles sans r ecritures la commande ApplyRule ar poss de les modes Once application une seule fois et Multi application tant que possible Ici ces deux modes sont quivalents parceque la r gle ne se r applique pas sur ses ant c dents PRI gt ar IntDiv 4 0nce Starting Apply Rule Le but devient ncl nc2 lt 0 Il s agit bien du
111. ent tablir qu aucun d passement n a lieu par exemple pour xx 2xv1 v2 il faut prouver 2xv1 INT et 2xv1 v2 INT 2 Faire plusieurs phases Il n est pas forc ment souhaitable de faire imm diatement Vexamen complet de chaque obligation en les prenant une par une souvent il vaut mieux faire plusieurs phases de mise au point Particuli rement lors de l criture des composants on fait souvent une mise au point r duite l interpr tation des buts compl t e ensuite phase de d veloppement mise au point r duite la seule interpr tation des buts phase finale mise au point complete Une autre m thode peut consister mettre l accent sur la recherche de la meilleure forme donner aux expressions du composant pour faciliter la preuve ce qui donne lieu une phase s par e En effet la retouche des composants pour faciliter la preuve peut r duire norm ment le nombre d obligations de preuve non d montr es en force 0 et diminuer ainsi le co t global de la preuve Par exemple l auteur conna t un cas o crire e a b plut t que a b e2 e1 sachant que a et b sont des l ments de e1 e2 a fait passer le nombre d obligations de preuves non d montr es en force 0 de 20 a 0 Le cycle avec retouche des composants est phase de d veloppement mise au point r duite la seule interpr tation des buts phase de simplification mise au point r duite la recher
112. ent ce qui s est pass Continuons la lecture By applying atomic rule InRelationXY 1 dom a POW s ran a POW t gt a s lt gt t the goal tt lt lt tport taches tt lt gt PORTS is now dom tt lt lt tport lt taches tt and ran tt lt lt tport lt PORTS Une r gle s est appliqu e nous avons maintenant les deux buts ci dessus 106 Prouveur interactif Manuel Utilisateur Attempt to prove not tt taches Obvious goal tt taches is discharged because in hypothesis HiddenPredicate mecanism is transforming goal not tt taches in bfalse Obvious goal Check 4 is discharged because in hypothesis After deduction goal is now bfalse Attempt to prove bfalse fails Le prouveur a de nouveau tent de prouver tt taches Goal dom tt lt lt tport lt taches tt is simplified in dom tport tt lt taches tt Le but a t simplifi par une r gle de r criture Dans le mode de trace que nous avons choisi ces r gles de r criture ne sont par trac es on peut obtenir ces traces suppl mentaires en utilisant la commande pr Ru Goal None File Simpl Attention cela produit des traces longues By applying atomic rule InPOWXY 24 a POW c b gt a b POW c the goal dom tport tt lt taches tt is now dom tport lt taches tt tt Goal dom tport lt taches tt tt is simplified in dom tport lt taches Obvious goal
113. ent la forme du cons quent de la r gle il faut voir si une autre r gle ne peut pas s appliquer INDICATIONS UTILES POUR LA PREUVE 123 le but peut tre r crit sous une autre forme acceptable qui permettra l application de la r gle Imaginons que le but contienne l expression alors que la r gle attend l expression E Il est possible de d ajouter l hypoth ses E F ah E E Cette galit peut tre d montr e par pp rp 0 ss mp ou pr Une fois cette galit d montr e elle est mont e dans la pile des hypoth ses commande dd Cette galit est ensuite appliqu e au but eh E La r gle peut alors tre appliqu e v rifier de ne vous tre pas tromp en ajoutant une hypoth se mauvaise criture Dans ce cas il faut revenir en arri re jusqu cet ajout d hypoth se qu il faut corriger puis repartir en avant jusqu au point o l on s est arr t dans la d monstration interactive De mani re syst matique il faut v rifier la bonne criture des r gles que l on ajoute Pour cela on utilise la commande sr theorieutilisateur a Toutes les r gles utilisateurs contenues dans la th orie theorieutilisateur seront alors affich es Par exemple la commande sr tt a permet d afficher toutes les r gles de la th orie tt PRI gt sr tt a Searching in tt rules with filter consequent should contain a Starting search Rule list is tt 1 binhyp s seq T gt size
114. er B il suffit d ouvrir la fen tre principale qui est en ic ne et de double cliquer sur le composant LA PHASE DE MISE AU POINT 39 5 4 1 Conseils pour l interpr tation des buts La m thode g n rale pour interpr ter un but est d isoler la partie concern e du composant g n ralement une seule ligne et de voir quelle contrainte on cherche a v rifier Il suffit g n ralement de se concentrer sur ces deux l ments pour comprendre la provenance d un but Parfois le but tient sur plusieurs lignes et sa lecture directe n est pas souhaitable Il faut alors utiliser les fonctionnalit s du prouveur interactif cela est expliqu au paragraphe Lors de la lecture d un but il y a un certain nombre de choses savoir pour une compr hension facile interpr tation des variables avec conf re le manuel d interpr tation des obligations de preuve Sans paraphraser ce document nous rappelons quelques rep res simples et approximatifs variables vv si on prouve un raffinement ou une implantation variables du niveau plus abstrait variables vv 0 dans le cas d une variable modifi e plusieurs fois boucle ou s quence valeur initiale variables vv 1 variables du raffinement ou de l implantation qu on est en train de prouver ou d une machine import e variables vv 2 variables dans le corps d une boucle variables vv 7777 variables apr s toutes les modifications de l op ration
115. eractive Le menu g n ral de lancement de l outil de preuve est donc le suivant 16 Prouveur interactif Manuel Utilisateur Prove gt D taillons ce menu Interactive Automatic Automatic Automatic Automatic Automatic Automatic Unprove fast force 0 force 1 force 2 force 3 replay LD aN TR TR TR TS Interactive lancement du prouveur en mode interactif Les diff rentes commandes d placement entre les obligations de preuve commandes de preuve sont entr es par l op rateur Automatic lancement du prouveur en mode automatique sur toutes les obligations de preuve non prouv es du composant Avec les options force 0 force 3 les m canismes du c ur de preuve sont essay s dans chacune des force successives de 0 3 jusqu au chiffre indiqu Avec l option fast la force Rapide est employ e seule Avec ces options la seule commande de preuve utilis e est donc pr Par contre avec Voption replay c est la s quence de commandes enregistr es interactivement pour chaque lemme qui est rejou e Unprove remet toutes les obligations de preuve du composant l tat Unproved 3 1 5 D tail des principales fen tres D crivons maintenant la fen tre de situation globale du prouveur interactif celle qui affiche la liste de obligations de preuve INTRODUCTION AU PROUVEUR 17 21 Nombre de PO non
116. ernent aa sh aa en mode multiple par exemple sh aa _and vv pour les hypoth ses qui contiennent la fois aa et vv avec des motifs par exemple sh a b pour les hypotheses qui contiennent des additions Les variables une lettre qui sont employ es ici remplacent n importe quelle formule ce sont des jokers la fonction de s lection des fen tres d hypoth ses et de commande du prouveur interactif dans ces fen tres presser la fois la touche de mise en majuscules de votre clavier et le bouton du milieu de la souris puis choisir Find All dans le menu qui apparait Une zone de dialogue s affiche vous permettant de saisir une chaine de caract res pour mettre en vid o inverse toutes les occurrences de celle ci C est tr s utile par exemple pour rep rer rapidement toutes les occurrences d une expression dans les hypoth ses Pour illustrer tout ceci nous pr sentons ci apres l cran de preuve correspondant a notre exemple de maximum entre 0 et vv aa De plus nous avons utilis la fonction de s lection pr c demment d crite dans la fen tre des hypoth ses pour rechercher aa et dans la fen tre de commande pour rechercher vv 36 Prouveur interactif Manuel Utilisateur Uy basic_train pilote 1 INTERACTIVE PROOF Ap basic_train pilote 1 HYPOTHESIS 4 Font Mode lt gt Asdi Math Quit Add Hyp A ASA ny Global Interrupt EE lt 2147483647_A Situation
117. ervalle de variation du reste d une telle division Nous nous placerons dans le cas o le prouveur n a aucune connaissance math matique sur les restes La preuve se fera donc avec ajout de r gles manuelles nous allons voir comment l usage des fonctionnalit s permet de r duire ces r gles au minimum Consid rons l obligation de preuve suivante Included imported and extended machines invariants A c1 1 0 150 A c2 1 0 150 A nmesure l eN A ntransfert l N A btrue A 0 lt c1 1 A c1 1 lt 150 A 0 lt c2 1 A c2 1 lt 150 A Previous components invariants A c1 1 0 120 A c2 1 0 120 A c1 1 c2 1 1 1 A Component invariant A c2 c2 1 A cl c1 1 A nmesure 1 ntransfert 1 A ncycle ntransfert 1 A c1 1 lt 120 A c2 1 lt 120 A 0 lt 1 c1 1 c2 1 A 1 lt cl 1 c2 1 A 0 lt 1 c1 14 c2 1 A c1 1 c2 1 lt 1 A equi_l cycle 20 A Local hypotheses A nel 0 150 A nc2 0 150 A cl l ncl 4 4 A c2 1 nc2 4 4 A ncl nc2 lt c1 1 c2 1 A nel nel nc2 2 0 150 A nc2 ncl nc2 2 0 150 A nmesure 1 1 N A ntransfert 1 1 N A Check operation refinement ref 11 gt ncl ncl nc2 2 nc2 ncl nc2 2 1 1 Il est facile de v rifier intuitivement que cette obligation de preuve est juste En effet si l expression consid r e tait un calcul dans l ensemble des nombres r el nous aurio
118. es 7 obligations de preuve ayant m me forme se fait par une seule commande TryEveryWhere te eh 0 mod 2 amp eh 1 mod 2 pr Tac func Replace Loc Unproved On v rifie alors que ces obligations de preuve sont effectivement d montr es Begin TryEveryWhere t t Summary op op op op op op op 25 24 23 22 21 20 19 transformed transformed transformed transformed transformed transformed transformed End TryEveryWhere Unproved Unproved Unproved Unproved Unproved Unproved Unproved Proved Proved Proved Proved Proved Proved Proved eh 0 eh 0 eh 0 eh 0 eh 0 eh 0 eh 0 mod mod mod mod mod mod mod 2 2 2 2 2 2 2 er 2P amp 2 2P EE amp eh 1 eh 1 eh 1 eh 1 eh 1 eh 1 eh 1 mod mod mod mod mod mod mod 2 2 2 2 2 2 2 2 2 2P EE 2 2 2 pr Tac func pr Tac func pr Tac func pr Tac func pr Tac func pr Tac func pr Tac func 136 Prouveur interactif Manuel Utilisateur Chapitre 8 Etudes de cas Dans ce chapitre nous allons pr senter quelques preuves interactives Apr s chacune de ces preuves nous r sumerons l esprit de la m thode employ e 137 138 Prouveur interactif Manuel Utilisateur 8 1 Preuve simple par contradiction Nous allons pr senter un exemple de preuve interactive sans aucune r gle manuelle Le but initial est bfalse ce qui indique que la preu
119. es de l hypoth se P c est dire d apr s nos conventions HYP P Ceci est connu sous le nom de r gle de d duction On dit aussi que P monte en hypoth se pour d montrer P sous les hypoth ses HYP nous disposons de la r gle suivante s il existe un pr dicat Q tel que sous les hypoth ses HYP P on puisse d montrer la fois Q et Q alors P est d montr sous les hypoth ses HYP Intuitivement en supposant P nous avons abouti une contradiction Notons que si P est toujours faux alors P Q est toujours vrai Ceci d coule de la r gle de d duction et rejoint la remarque du paragraphe 2 2 sur les hypoth ses fausses Pour faciliter la manipulation des pr dicats dont le statut vrai ou faux est connu introduisons les notations suivantes e btrue est le pr dicat toujours vrai e bfalse est le pr dicat toujours faux Il nous reste introduire les deux derni res notations propositionelles qui se d finissent partir des pr c dentes e P V Q P ou Q est d fini comme P gt Q e P amp Q P quivalent Q est d fini comme P gt Q A Q gt P La d finition du ou disjonction n cessite quelques commentaires Intuitivement elle indique la chose suivante dire que P ou Q est vrai revient a dire que si P est faux Q est forc ment vrai traduction de P gt Q Cette d finition n est pas sym trique en P et Q 6 Prouveur interactif Manuel Utilisateur bien que l
120. es ne doivent pas tre supprim es si il y a des r gles plac es apr s dans la m me th orie qui sont utiles En effet ces r gles changent alors de num ro d ordre ce qui fait que les adressages par ApplyRule sont d cal s Par exemple supposons qu un fichier pmm contienne trois r gles THEORY MyRules IS ri r2 r3 END Si Pop rateur s apercoit la fin de la preuve du composant que ri ne sert pas il peut tre tent de la supprimer Mais dans ce cas les commandes concernant la troisieme r gle ar MyRules 3 sont refus es message MyRules 3 no such rule et celles concernant la deuxi me r gle n utilisent plus la bonne r gle Ces commandes ont pu tre m moris es comme d monstration d obligations de preuve ces derni res sont consid r es comme prouv es On ne s apercoit du probleme que si l tat de ces obligations de preuve revient non prouv et que l on tente de rejouer la preuve Pour cette raison il est toujours souhaitable de Remettre l tat non prouv toutes les obligations de preuve d un composant et rejouer les d monstrations Pour faire ceci utiliser l option Unprove du menu Prove de la fen tre principale puis l option Prove replay du m me menu Il faut le faire quand les modifications sur les r gles manuelles deviennent importantes et en tous cas la fin de la preuve d un composant Cette pr caution n est inutile que si aucune r gle manuelle n a t em
121. eur de pr dicats ce sont les messages Loading theory Les erreurs ventuelles sont cit es ce niveau Juste apr s ces messages il y a aussi la trace de la commande gs mise par l interface pour obtenir la liste des obligations 114 Prouveur interactif Manuel Utilisateur Chapitre 7 Indications Utiles pour la preuve 7 1 Poursuite de la preuve en fonction de la forme du but Dans la plupart des cas la forme du but n est pas suffisante pour d terminer le type de d monstration appliquer Ce sont souvent en fait les hypoth ses locales qui permettent de d terminer le type de d monstration appliquer On peut toutefois tablir une classification des buts et associer des commandes tenter pour chacun d eux 2x P en g n ral la commande se SuggestForExist est obligatoire moins que l on ait un but du style Jzz xe 0 Dans ce cas la commande mp pr pp r ussit P gt Q il est possible d utiliser dd pour monter directement P dans la pile des hypoth ses sans traitement simplifi cation normalisation sur celles ci dd 0 pour monter P dans la pile des hypoth ses apr s normalisation et application des simplifications de la force 0 mp pr pour simplifier le but et r soudre pp pour r soudre pp rp 0 si Q peut se d montrer avec uniquement les hypoth ses P Va P x Q x il est possible d utiliser mp pr p
122. euves par cas exploratoires il faut donc revenir en arri re ba et utiliser une commande de preuve r duire pour progresser dans la preuve sans risque Etape 4 La commande pr c dente utilise les tactiques et les r gles de la preuve automa tique il est possible que la direction prise ne soit pas celle souhait e par lop rateur Nous devons donc juger cette tape si il faut continuer partir du but simplifi par la preuve r duite ou revenir en arri re En pratique il suffit de juger la simplicit de ce nouveau but 58 Prouveur interactif Manuel Utilisateur Etape 5 Retour en arri re si le but simplif n est pas jug b n fique Etape 6 C est bien str l tape la plus d licate il s agit de trouver la bonne commande interactive pour faire progresser la preuve vers son aboutissement La suite de cette section traite principalement ce probl me Par exemple soit d montrer l obligation de preuve suivante Local hypotheses A ntt TACHES A ntt taches A tt 0 taches U ntt A Check that gt tconnait U ntt x tconnait tt tt 0 pass tident ntt gt tident tt tt 0 Volontairement nous ne montrons que les hypoth ses locales telle que pr sent e ci dessus cette obligation est incompl te et donc ind montrable Mais ce n est pas notre propos de relire les hypoth ses ici normallement nous disposons d une d monstration intuitive provenant de la
123. fich 1 2 3 4 car est le symbole ASCII pour l appartenance Les symboles ASCII sont essentiels pour pouvoir saisir des formules sur un clavier traditionnel m me si l interface peut afficher en police math matique Dans la zone interactive tapez pr et retour chariot derri re le marqueur PRI gt La preuve de cette obligation d marre et choue sur le but toujours faux bfalse Par la commande pr vous avez lanc le coeur de preuve dans la force courante force 0 ce qui revient ce que nous avions d ja fait en mode automatique Le coeur de preuve est toujours disponible en mode interactif simplement ce n est plus la seule commande possible Il y a d autres commandes de preuve possibles qui permettent d appliquer sp cifiquement une r gle de faire de la preuve par cas etc Toutes ces commandes ont deux lettres et sont d sign es dans la documentation par un mot clef plus explicite Il y a par exemple la commande DoCases dc ou bien ApplyRule ar et ainsi de suite INTRODUCTION AU PROUVEUR 15 commandes de preuve ce sont les commandes qui pilotent la preuve Elles peuvent tre soit des appels au coeur de preuve commande Prove pr soit des actions directes de preuve par exemple appliquer une d duction commande Deduction dd Les com mandes de preuve applicables chaque obligation de preuve sont m moris es par l outil nous allons voir comment Ce que l on d signe par prouveur automatique
124. gations de preuve Il faut pour cela que l op rateur apr s avoir lanc la preuve automatique Prove User Pass appuie sur le bouton Interrupt Next PO a chaque fois qu il consid re que le temps de preuve est trop long 120 Prouveur interactif Manuel Utilisateur 7 3 Application de regles manuelles Pour application de r gles manuelles plusieurs conseils peuvent tre utiles ne pas oublier de normaliser correctement les r gles les r gles des fichiers Pmm sont normalis es par le prouveur au chargement les r gles du fichier PatchProver doivent tre normalis es par le r dacteur de ces r gles avant toute utilisation a lt b est normalis par le prouveur en a 1 lt b Aussi la garde btest a lt b sera r crite en btest a 1 lt b et ne r ussira jamais dans le cas d expressions complexes n h sitez pas surparenth ser les termes de votre r gle v rifiez que vous n utilisez que des jockers variables une seule lettre La r gle binhyp xx 0 gt ne s appliquerar qHeck le but est strictement xx mod 2 0 mais pas s il s agit de yy mod 2 0 v rifiez que vous n introduisez pas de jockers morts non instanci s dans votre r gle En pratique tous les jockers apparaissant dans le cons quent d une regle Backward sont instanci s Il faut s assurer dans le cas du remplacement d un but par un but quivalent
125. h es automatiquement les preuves par cas multiples conduisant des temps de preuve longs Nous d clenchons cette preuve par cas par une commande DoCases pr c d e par un appel r duit au c ur de preuve conform ment la m thode g n rale PRI gt pr Red Starting Prover Call Current PO is Initialisation 1 Unproved saved Unproved Goal xx 1 End LA PHASE DE PREUVE FORMELLE 95 Inutile de chercher d o vient le nouveau but g n r il faut clairement lancer la preuve par cas PRI gt de xx 7 6 5 4 3 2 1 Do Cases on Enumerated 7 6 5 4 3 2 1 Current PO is Initialisation 1 Unproved saved Unproved Goal XX 7 gt xx Il bE End Nous avons utilis la deuxi me syntaxe de de voir manuel de r f rence du prouveur c est dire dc v E o v est une variable appartenant l ensemble enum rable E Le prouveur doit alors d montrer v E ici c est directement une hypoth se puis se place dans chaque cas v e pour chaque l ment e de E Dans notre exemple chaque cas se d montre directement PRI gt pr Starting Prover Call Current PO is Initialisation 1 Unproved saved Unproved Goal XX 6 gt xx Il bE End PRI gt pr Starting Prover Call Current PO is Initialisation 1 Unproved saved Unproved Goal XX D gt xx Il bE End PRI gt pr Starting Prover Call Current PO is Initialisation 1 Unproved saved Unproved Goal xx 4 gt xx
126. ing Prover Call Avec la disparition du dernier sous but le but initial de l obligation de preuve r appara t color en vert la preuve est finie Il suffit de quitter l obligation de preuve pour provoquer la sauvegarde de la d monstration L arbre de preuve final est le suivant 154 Prouveur interactif Manuel Utilisateur Force 0 dd amp dc nci nc2 lt 0 amp dd amp ah nci nc2 mod 2 1 2 0 amp ar IntDiv 4 0nce amp pr amp pr amp pr amp pr Red amp ar IntDiv 1 Goal amp pr amp pr Red amp ar IntDiv 1 Goal amp pr amp dd amp ah nci nc2 mod 2 0 2 1 amp ar IntDiv 2 0nce amp ah not nci nc2 lt 0 amp pr amp pr amp pr amp pr Red amp ar IntDiv 1 Goal amp pr amp pr Red amp ar IntDiv 1 Goal amp pr amp Next Les deux cas principaux de la preuve apparaissent clairement dans l indentation de cet arbre Pour faire cette d monstration nous n avons utilis que cinq r gles crites dans un format presque purement math matique Ces r gles sont presque des d finitions leur validation sera facile et elles seront probablement r utilisables Nous avons vit l usage de r gles trop sp cifiques grace l utilisation des fonctionnalit s du prouveur interactif C est ce principe consistant employer des r gles simples par des fonctionnalit s volu es du prouveur qui permettent de garder minimales les r gles ajout es Nous
127. ing in tmp lastfrm StationUnix but interrupted The Predicate Prover went out of time Current PO is fork 6 84 Prouveur interactif Manuel Utilisateur Unproved saved Unproved Command line is Force 0 amp dd amp Next Saved line pos 2 Force 0 amp dd New Hypothesis since last command Goal tconnait ntt tconnait tt tt o pass tident lt ntt gt tident tt tt 0 End Nous allons maintenant refaire rapidement la d monstration qui a t pr sent e au para graphe 6 1 Nous nous remettons tout au d but par une commande Reset PRI gt re Resetting PO Current PO is fork 6 Unproved saved Unproved Command line is Force 0 amp Next Saved line pos 1 Force 0 amp dd Hypothesis Goal Local hypotheses amp ntt TACHES amp not ntt taches amp tt 0 taches ntt amp Check that the invariant tt tt gt tconnait ntt tconnait tt tt 0 pass tident lt ntt gt tident tt tt 0 End La d monstration pr c demment vue peut commencer PRI gt pr Red Starting Prover Call Current PO is fork 6 Unproved saved Unproved LA PHASE DE PREUVE FORMELLE 85 Command line is Force 0 pr Red amp Next Saved line pos 1 Force 0 dd New Hypothesis since last command Goal tconnait ntt tconnait tt tt o pass tident lt ntt gt tident tt tt 0 End PRI gt dc ntt tt 0 St
128. ion lire le chapitre 6 5 5 La simplification des expressions des composants B Certains composants produisent trop d obligations de preuve ou bien produisent des obli gations de preuve tres compliqu es Il arrive m me que le nombre d obligations de preuve qu il faudrait g n rer pour un composant soit tellement grand que le g n rateur sature sans aboutir Dans tous ces cas c est sur les composants eux m mes qu il faut agir pour choisir la forme des expressions qui facilite la preuve D autre part simplifier les expressions des sp cifications formelles permet souvent de mieux appr hender le probl me car le logiciel envisag est alors mieux mod lis dans une forme qui facilite le raisonnement comme elle facilite la preuve L esprit de la m thode B est de construire le logiciel comme la preuve qu il satisfait le besoin consid r lire la pr face du B Book Il doit tre clair que tout projet juste n est pas forc ment d montrable La preuve est une v rification de tr s haut niveau qui ne peut se faire que si certains imp ratifs de d coupage sont respect s Divide and Conquer Un exemple classique de probl me de cet ordre est l examen des obligations de preuve concernant des op rations plac es en s quence apr s un IF ces PO sont d doubl es n fois n tant le nombre de branches du IF La transformation des composants pour revenir des expressions facilitant la preuve est un sujet m thodologique comp
129. ions envisag es et tenter une d monstration rapide La simplification des expressions d un composant peut faciliter sa preuve Tout projet juste n est pas forc ment d montrable sous une forme maladroite le projet peut produire des preuves trop compliqu es Red couper un projet pour simplifier sa preuve Mettre les expressions sous la forme normalis e du prouveur Chercher faire appara tre des galit s litt rales Chercher mettre les expressions arithm tiques sous forme canonique La preuve rapide d une PO doit tre tent e en se donnant une limite de temps Essayer en premier le prouveur de pr dicats Ne pas tenter de d monstration de plus de 5 commandes Tenter de g n raliser une d monstration rapide d autres obligations Les obligations avec des expressions complexes peuvent se lire en utilisant le prouveur comme simplificateur Les buts existentiels simples se traitent avec SuggestforExists ils traduisent parfois un exc s d ind terminisme dans le composant Les buts existentiels abstraits traduisent l expression impr cise d une constante abstraite Les buts non d coup s sont souvent dus des disjonctions Si une obligation de preuve fausse est d couverte il faut corriger le composant avant de poursuivre 29 30 Prouveur interactif Manuel Utilisateur Il faut v rifier que l obligation est bien fausse ce n est pas vident Chercher un contre exemple est un bon moyen de s a
130. l au c ur de preuve l essentiel tant de voir comment pour suivre sur le prochain but Dans la plupart des cas une trace produite au cours d une d monstration non aboutie est une perte de temps C est pourquoi nous avons choisi dans l exemple qui va suivre de tracer une obligation qui se d montre par un seul appel au c ur de preuve en force 1 la trace de preuve est ainsi pr sent e dans son vrai r le d information apr s coup Soit d montrer le lemme suivant PORTS F Z PORTS CZ A PORTS taches C TACHES A tport taches gt PORTS A dom tport C taches ran tport C PORTS A dom tport C TACHES A dom tport taches tt taches A tt dom tport A tt TACHES A TACHES taches gt tt lt tport taches tt gt PORTS Pour obtenir la trace de la d monstration il suffit de lancer le prouveur interactif d acc der cette PO on est alors en force 1 et de taper pr Ru Goal None File Il s agit d une commande pr avec des arguments pour indiquer que nous d sirons une trace de preuve pr sentant les buts et les r gles pr sent s sur le terminal et recopi s dans un fichier L affichage de la trace est le suivant Starting Trace in mode Ru Goal None File LA PHASE DE PREUVE FORMELLE 105 Starting Prover Call After deduction goal is now tt lt lt tport taches tt lt gt PORTS La d duction permet de faire monter les hypoth ses locale
131. le attendue Il ne faut pas oublier en effet que les r gles contenues dans un fichier Pmm sont normalis e lors de leur chargement 9 6 Ajout d hypoth se fausse Lors d un ajout d hypoth se il faut prendre garde ne pas ajouter une hypoth se fausse car bien entendu la d monstration de validit de cette hypoth se sera impossible et sera source de crises de nerfs de la part de l utilisateur Comme on sait si P est le but courant et que la commande ah H est appliqu e alors le but devient H H P L erreur consiste mal orthographier le nom de l identificateur B ou inverser 2 noms de variables ou mal parenth ser une expression les risques d erreur sont nombreux Le prouveur ne signale pas d anomalie et l utilisateur ne sera pas averti de son erreur Seule une lecture attentive peut lui indiquer ot se situe son erreur Il peut arriver que depuis l ajout d hypoth se plusieurs commandes de preuve ont t saisies ce qui peut g ner la relecture et la d tection de l erreur Veuillez donc faire bien attention lorsque vous ajoutez une hypoth se 160 Prouveur interactif Manuel Utilisateur 9 7 Nombre de pas n cessaires une preuve Parfois si une preuve est trop longue on se dit qu on a fait une erreur et on recommence alors que c est juste Il faut savoir qu en moyenne les preuves sont petites mais que cer taines peuvent tre beaucoup plus longues On peut consid rer que 10 pas d
132. le du but et des hypoth ses locales Au cours de cette inspection l on doit tre capable de d terminer les l ments qui per mettent de d montrer cette obligation de preuve c est dire quels sont les hypoth ses n cessaires Si besoin est ces l ments seront couch s sur papier afin de pouvoir facile ment les retrouver par la suite Si l obligation de preuve est complexe et est d une lecture difficile il est recommand d utiliser l analyseur logique de formule afin d avoir une vi sion plus synth tique de l obligation de preuve Si par contre l obligation de preuve vous parait fausse il faut absolument exhiber un contre exemple c est dire une valuation particuli re des variables d finies en hypoth se qui permette de d montrer la contrapos e du but courant Le plan de preuve peut contenir le type d monstration a r aliser preuve par cas preuve par contradiction d composition du but La d termination du type de d monstration est tabli par Putilisateur en fonction du r sultat de l inspection visuelle de obligation de preuve et de son exp rience en mati re de preuve interactive avec l Atelier B la liste ordonn e des hypoth ses ajouter Cette liste peut tre compl t e avec les commandes interactives utilis es pour la d monstration de chaque hypoth se l tat de la preuve courante c est dire quel endroit de l arbre de preuve est on arriv Ce plan de preuve permet
133. les expressions complexes 124 Prouveur interactif Manuel Utilisateur auront t squel tis es on remplace ces expressions par des variables La r gle doit tou jours tre simple car elle devra tre d montr e par la suite Lors de l ajout de r gles il faut se poser certaines questions quant la r daction de la regle ma r gle n est elle pas trop sp cifique faut il crire une r gle complexe ou plusieurs plus simples yat il une r gle de la base de r gles qui peut tre utilis e sous une forme un peu diff rente 7 5 Faciliter la preuve en ajoutant des informations dans le mod le B Il est possible d ajouter des informations dans le mod le B qui peuvent faciliter le travail de preuve Il s agit des clauses ASSERTIONS PROPERTIES et ASSERT Ces 3 clauses ont des port es diff rentes substitution op ration pour ASSERT composant pour ASSERTIONS et PROPERTIES PROPERTIES permet de caract riser les constantes utilis es typage expression de pro pri t s ASSERTIONS permet de caract riser les variables du composant une assertion doit pou voir tre d montr e sous l hypoth se que l invariant et les assertions pr c dentes sont vraies Il y a diff rentes mani res d exprimer ces propri t s Certaines sont facilement d montrables d autres moins En fait l ajout d une assertion A correspond ajouter syst matiquement l hypoth se A toutes les
134. les manuelles plus simple que la validation de la preuve elle m me Il faut donc que le nombre et la complexit de ces r gles soient petits devant la taille de la preuve initiale En pratique cela s obtient en utilisant les r gles manuelles de mani re occasionnelle conjointement avec les m canismes s curitaires du prouveur Les r gles manuelles ne r solvent alors que des sous buts Les r gles manuelles sont crites dans un langage appel langage de th orie dans le fichier composant pmm Ce fichier est totalement crit par l op rateur l outil ne le cr e pas par d faut afin que son absence ventuelle valide la preuve Pour expliquer le principe de la preuve interactive nous avons du aborder tr s rapidement les notions de r gle de commande d application de r gle sans les d tailler C est l objet du chapitre 6 3 3 Conclusion Vous savez maintenant faire fonctionner le prouveur dans l Atelier B et par quels prin cipes les obligations de preuves dont la d monstration automatique choue peuvent tre d montr es interactivement La suite de ce manuel insiste sur la m thodologie de la preuve plut t que sur la pr sentation des diff rentes commandes En effet la preuve d un projet B doit tre conduite avec m thode Avant d utiliser le prouveur interactif pour d montrer les obligations de preuve de votre projet lisez le chapitre 1 En commen ant directement par la preuve formelle vous risque riez
135. les pr sentent des risques de bouclage accrus Elles sont donc uniquement r serv es un usage interactif 6 5 4 Les r gles manuelles La derni re des techniques l mentaires de preuve est l ajout de r gles manuelles Il faut viter de l employer si c est possible car les r gles ajout es devront tre prouv es ext rieurement La m thode pour ajouter et utiliser une r gle manuelle est d crite au paragraphe 6 2 3 avec un exemple d application Le lecteur se reportera ce paragraphe 6 6 Utilisation avanc e Nous allons pr senter maintenant divers l ments qui permettent une meilleure utilisation du prouveur interactif La v rification finale de la preuve L usage d une r gle d admission L optimisation des d placements dans la preuve Le choix d une force sup rieure en preuve interactive La trace d une d monstration LA PHASE DE PREUVE FORMELLE 99 6 6 1 La v rification finale de la preuve En phase de preuve formelle l op rateur travaille sur chaque obligation de preuve une une pendant un temps parfois long Chaque obligation dont la preuve aboutit est marqu e Proved dans les fichiers de gestion du composant et sa preuve n est plus rejou e Bien que ne pas rejouer les preuves d j faites soit essentiel pour permettre un bon rendement il y a des situations o des preuves ne peuvent plus tre rejou es Par exemple une d monstration peut abouti
136. lexe que nous n aborderons que tr s partiellement ici Nous allons simplement donner un certain nombre de recettes 5 5 1 Red couper les composants Les obligations de preuve trop nombreuses ou trop complexes traduisent souvent un mau vais d coupage des composants Les s quences d instructions sont alors trop longues voir ci dessus il y a des boucles imbriqu es etc Le re d coupage est la premi re m thode envisager pour diminuer la difficult de la preuve Penser en particulier Cr er des machines import es pour s parer les parties complexes d une implantation dans des op rations import es Ins rer des raffinements si la preuve d une implantation est trop complexe 46 Prouveur interactif Manuel Utilisateur 5 5 2 Tenir compte des normalisations du prouveur Le prouveur effectue un certain nombre de normalisations d une mani re parfois partielle pour des problemes de performance En phase de mise au point il peut tre utile de changer les expressions du composant pour retrouver les normalisations du prouveur ce qui peut influer de facon tr s importante sur ses performances La m thode est la suivante 1 interroger le prouveur appliquer le prouveur sur l obligation de preuve non d montr e en force 0 pour examiner le but et les hypoth ses en chec et voir sous quelle forme il a mis les expressions du composant attention faire pr sans faire dd avant sinon les hypoth ses locales
137. line is Force 0 amp Next Saved line pos 1 Force 0 dd LA PHASE DE PREUVE FORMELLE 81 End Hypothesis Component properties amp pass IDENTITES gt PASSWORDS amp pass PASSWORDS gt IDENTITES amp dom pass IDENTITES amp ran pass PASSWORDS amp TACHES FINCINTEGER amp not TACHES Y IDENTITES FINCINTEGER amp not IDENTITES Y PASSWORDS FIN INTEGER amp not PASSWORDS amp PORTS FINCINTEGER amp not PORTS Y btrue amp Component invariant amp taches lt TACHES amp tconnait taches lt gt PASSWORDS amp tident taches gt IDENTITES amp dom tident taches amp tport taches lt gt PORTS amp dom tport taches amp Itt tt taches gt tconnait tt pa fork preconditions in this component amp tt taches amp not TACHES taches amp tconnait tt pass tident tt Y StationUnix fork 6 Local hypotheses amp ntt TACHES amp not ntt taches amp tt 0 taches ntt Check that the invariant tt tt gt tconnait ntt tconnait tt tt L obligation de preuve est affich e avec les autres informations d tat en particulier la ligne de commandes Nous pouvons tenter une commande Prove PRI gt pr Starting Prover Call Current PO is fork 6 Unproved saved Unproved Command line is Force 0 pr amp 82 Prouveur interac
138. locales et l invariant du composant s lection manuelle des hypoth ses INDICATIONS UTILES POUR LA PREUVE 117 On s lectionne les hypoth ses par la commande ah H Les hypotheses sont d ja pr sentes dans la pile des hypoth ses Le but B devient H B Lorsque toutes les hypoth ses sont incluses dans le but de cette mani re le but est de la forme H gt Hn gt seb on fait pp rp 0 Par ailleurs il est important de ne pas oublier d inclure les hypoth ses de bonne d finition du lemme d montrer Ces hypoth ses permettent souvent la d monstration du lemme en question Par exemple si le but contient expression f x on ajoutera les 2 hypoth ses x dom f fEA gt B 7 2 2 Limitation du temps de calcul Il est possible de r gler le temps de coupure de pp temps de calcul maximum allou pp Une bonne valeur du temps de coupure est 10 s Cette valeur permet par la commande te TryEvery Where de tester rapidement pp sur de nombreuses obligations de preuve Uti liser de mani re syst matique une valeur plus lev e par exemple 300 s est envisageable mais le gain en taux de preuve restera certainement modeste Ce temps de coupure n est pas utilisable en preuve automatique lors de l utilisation de la User_Pass 7 2 3 Utilisation de pp bon escient L utilisateur est parfois amen a se poser la question dois je utiliser pp ou ajouter une regle Il n y a pas de r ponse a
139. lons maintenant pr senter les notions fondamentales pour comprendre le fonctionnement du prouveur Cela nous permettra de l utiliser pour les d monstrations interactives base de r gles c est l ensemble des r gles qui constituent la connaissance math matique du prouveur Grossi rement ces r gles sont des instructions permettant au prouveur de transformer des formules Par exemple une r gle indique que toute formule de la forme a b peut tre remplac e par b a commutativit de l addition m canisme de preuve Dans une situation donn e plusieurs r gles peuvent s appliquer et le choix influe sur le cheminement de la d monstration En reprenant l exemple 12 Prouveur interactif Manuel Utilisateur pr c dent nous savons que a b peut tre r crit en b a mais cela ne nous dit pas s il est b n fique de faire cette transformation pour la d monstration en cours Les m canismes de preuve sont les proc dures heuristiques qui permettent de faire de tels choix Un exemple repr sentatif est le m canisme de r duction des galit s capable quand plusieurs variables sont gales entre elles de choisir un lot minimal de variables pour exprimer l obligation de preuve c ur de preuve c est un ensemble constitu de la base de r gles math matiques et des m canismes de preuve Les obligations de preuve qui ont directement abouti ont t d montr es par le c ur de preuve force Rapide 0
140. m riques bnot G vraie si G est faux Attention pour bnot btest a b le test ne porte que sur la valeur litt rale de a et b Donc cette garde peut r ussir si a et b sont litt ralement diff rents mais tre identiquement valu s On pourrait avoir par exemple valu vrai PMP don binhyp b 1 bnum a vrai si a est un entier naturel plus petit que MAXINT bgoal G vrai si le but courant est de la forme G AP vraie si x n a pas d occurrence libre dans P x x 3 est faux A vr re E gt P x est vrai blvar Q Q est instanci avec la liste des variables actuellement quantifi es Ces 2 derni res gardes sont n cessaires pour la r daction de r gles de r critures non atomiques En effet il faut faire attention ne pas capturer de variable Par exemple si l on fait appel un binhyp il faut v rifier que les variables instanci es sont non libres dans la liste des variables quantifi es grace la combinaison des gardes blvar Q et Q z Par exemple soit l obligation de preuve fausse ax NAT A zx 0 A xr 1 1 A xx 2 2 gt Vax xx 1EN gt 21 2 N et la r gle binhyp a b c gt a b c qui remplace a b par c L application de cette r gle sur le but va transformer celui ci en Var 1eN gt 2 N 122 Prouveur interactif Manuel Utilisateur qui est vrai L erreur vient de la confusion entre la variable xx dans la pile des hypoth
141. m thodes formelles est d utiliser des notions math matiques pour repr senter le comportement des programmes informatiques c est pourquoi on parle de mod lisation formelle Les notions math matiques sont donc les l ments fondamentaux dont dispose Putilisateur pour construire un modele correspondant a ses besoins Mieux il connait ces notions meilleure sera son utilisation du langage Utiliser un langage formel permet d ex primer des nonc s d montrables et bien connaitre ces notions math matiques permet de conduire efficacement ces d monstrations Le langage B est fond sur la th orie des ensembles Cette th orie et toutes les notions qui en d coulent sont construites dans le B Book de J R Abrial chapitres 1 2 et 3 Si vous n tes pas familier avec ces notions math matiques nous vous recommandons vivement la lecture de ces trois chapitres qui vous donneront une connaissance structur e du sujet D autre part le Manuel de r f rence du langage B donne pour chaque symbole sa d finition et ses propri t s essentielles dans un format proche de celui d un dictionnaire N anmoins la connaissance de chaque symbole pris s parement ne remplace pas la compr hension des concepts math matiques Il est donc important d tudier la construction de la th orie dont ils sont issus Nous allons donc exposer les diff rentes notions math matiques dans l ordre dans lequel elles sont construites Attention ce chapitre n est
142. minal non graphique et d obtenir un affichage dans votre environnement de commande habituel par exemple affichage dans un xterm Nous allons pr senter ci apr s l enregistrement d une session de preuve en mode batch correspondant la d monstration qui a servi d exemple au paragraphe Pour les dis tinguer les commandes entr es par l op rateur seront soulign es La commande pour lancer l Atelier B en mode batch est lanceBB PRVB lanceBB Beginning interpretation bbatch 1 gt spl Printing Projects list LIBRARY passwd End of Projects list Nous n insisterons pas sur les commandes de l Atelier B en mode batch celle ci sont d crites dans le manuel utilisateur de l Atelier B Nous allons entrer dans le projet passwd bbatch 2 gt op passwd bbatch 3 gt sml Printing machines list StationUnix End of machines list Nous pouvons maintenant entrer dans une session de preuve interactive de la machine Station Unix bbatch 4 gt b StationUnix No current PO Nous retrouvons la pr sentation de la fen tre de commandes du prouveur interactif Une commande GlobalSituation permet de connaitre la liste des obligations de preuve 80 Prouveur interactif Manuel Utilisateur PRI gt gs State of all PO Initialisation PO1 P02 P03 P04 PO5 login PO1 P02 P03 P04 PO5 P06 fork PO1 P02 P03 P04 PO5 P06 kill PO1 P02 P03 P04 PO5 PO6 PO7 open PO1 P02 End Proved Proved Proved Pr
143. montent non normalis es 2 normaliser mettre les expressions du composant dans les formes quivalentes donn es par le prouveur 3 tester repasser le prouveur en force 0 voir paragraphe 4 2 et constater le gain ou la perte En plus de ce proc d assez exp rimental nous allons donner ci apr s un certain nombre de pr cautions prendre syst matiquement Les normalisations du prouveur sont expliqu es au chapitre Normalisation du manuel de r f rence du prouveur 5 5 3 Rechercher les galit s litt rales Le prouveur tant m canique son principe de base est de faire co ncider des formules entre elles Pour cette raison il faut viter de changer gratuitement la forme des expressions du composant Par exemple si dans l invariant on a lacb e f gt P Et que dans une pr condition on veut se placer dans le cas o a gt b f il ne faut surtout pas crire PRE a dom f gt b Mais plut t PRE a b E f L exemple ci dessus est volontairement exag r Ce genre de probl me peut n anmoins se produire lors de l criture d un composant surtout si ce dernier a subi beaucoup de mo difications successives Il faut aussi viter de passer par des constantes interm diaires qui vont obliger le prouveur faire des remplacements Utiliser plut t la clause DEFINITIONS qui fait un remplacement litt ral Par exemple ne pas crire CONSTANTS card_ens PROPERTIES card_ens card e
144. mposant pmm pmm Proof Methods Manual o composant est le nom sans extension du composant il doit se trouver dans le r pertoire bdp correspondant au projet Ce fichier n est pas cr par d faut par l Atelier on peut ainsi s assurer facilement de l absence de r gles manuelles pour un composant La syntaxe respecter est la suivante placer les r gles dans des th ories d clar es par THEORY name IS liste de r gles END s parer les r gles par des points virgule s parer les th ories par le caract re amp Voici un exemple de fichier de r gles 70 Prouveur interactif Manuel Utilisateur THEORY MyRules IS binhyp a lt b gt b 1 1 a b a lt b gt a 1 b 1 lt 0 END amp THEORY NatCalc IS a NATURAL amp b NATURAL gt a b NATURAL END Notons que les r gles de ce fichier ne sont pas forc ment des quivalences Par exemple examinons la r gle suivante a NATURAL amp b NATURAL gt atb NATURAL Cette r gle n est pas une quivalence Si elle est appliqu e sur le but 1 2 N elle produit bien les deux buts vrais 1 N et 2 N qui impliquent le but initial mais sur le but 1 2 N cette r gle produit le but faux 2 N et provoque l chec de la preuve Il s agit donc d employer de telles r gles bon escient Le fichier des r gles manuelles d un composant n est pas lu automatiquement par le pr
145. n anmoins tre vraies par hypoth ses contradictoires Par exemple dans un IF ELSIF sans ELSE mais dont la conjonction des cas est toujours vraie l obligation de preuve correspondant au ELSE absent peut concerner une variable qui n aura pas t initialis e sous l hypoth se contradictoire que la conjonction des cas est fausse Cette obligation de preuve est correcte elle ne d tecte aucune faute dans le composant Chapitre 6 La phase de preuve formelle Les notions essentielles pr sent es dans ce chapitre sont les suivantes M thode g n rale utliser autant que possible les appels au prouveur Utiliser pr ou pp pour terminer un but pr Red pour avancer D marrer en force 0 et avec une d monstration intuitive Les commandes se classent en commandes de d placement de visualisation et preuve de divers niveau Il est souhaitable de conna tre l existence de toutes les commandes environ 35 Le prouveur utilise des r gles d inf rence bas es sur la coincidence de formules Les jokers sont les variables une lettre qui repr sentent n importe quelle formule Les r gles de r criture permettent de transformer une partie d une expression Les gardes permettent d effectuer des tests lors de l application d une r gle Les r gles manuelles doivent tre crites dans le fichier pmm elles s utilisent avec pc et ar et sont prouv es l aide de la commande vr Le prouveur de pr dicats travaille en
146. n es Le but apparait avec les hypotheses locales pour des raisons de logique de preuve Voici un exemple d affichage d une obligation de preuve dans lequel la seule hypoth se locale est un commentaire entre guillemets INTERACTIVE PROOF HYPOTHESIS 0 lt 2147483647 aa A 2147483647 lt aa A aa lt amax A basic_train pilote 1 GOAL 7 gt max 0 vv aa N Notez l hypoth se de localisation basic_train pilote 1 Nous sommes donc sur la premi re obligation de preuve de l op ration pilote du composant basic_train Prouveur interactif Manuel Utilisateur 2 Faites monter les hypoth ses locales dans la pr sentation du prouveur inter actif les hypoth ses locales apparaissent avec le but Il faut les faire monter avec dd Deduction pour faciliter la lecture du but ces hypoth ses ne servant que pour la preuve formelle Attention ne pas sauver cette commande quand on quitte l obli gation de preuve Le prouveur vous posera la question quand vous quitterez cette obligation il suffira de r pondre non Pour faire monter les hypoth ses locales il suffit donc de taper dd dans la fen tre de commande INTERACTIVE PROOF HYPOTHESIS GOAL PRI gt dd Le but est maintenant isol INTERACTIVE PROOF HYPOTHESIS
147. n Add Hyp en haut de la fen tre et appuyer sur OK la commande ah voulue est g n r e automatiquement 6 7 3 Instancier p gt q si p est presque en hypoth se Sip gt q est en hypoth se et si une hypoth se est quivalente p une normalisation pr s alors le prouveur n aura pas produit q cause de la diff rence de forme sur p Pour le faire nous conseillons la m thode suivante faire un ajout de l hypoth se p telle qu elle appara t dans p gt q d montrer cette hypoth se Cette preuve devrait se faire facilement le prouveur com men ant par normaliser le but ce qui devrait ramener p dans sa forme en hypoth ses le but initial B devient p B faire dd pour monter p en hypoth se tel quel utiliser ph pour g n rer q 110 Prouveur interactif Manuel Utilisateur 6 7 4 Penser ah plut t que r gle par l avant Les r gles par avant sont des r gles particuli res qui permettent de g n rer de nouvelles hypoth ses partir d hypoth ses existantes Par exemple la r gle a b gt a b peut g n rer l hypoth se d riv e zz 3 partir de l hypoth se zx 3 Dans ce manuel nous n abordons pas l tude de ces r gles dont l usage est plus rare en interactif et qui provoquent facilement des bouclages Quand une r gle par l avant semble manquer c est dire quand une hypoth se d riv e par une r gle simple serait souhaitable il es
148. n du nombre d obligations de preuve pour le com posant consid r Dans ce cas pr cis la d monstration interactive pr c dente peut tre consid r e comme perdue car associ e d sormais une autre obligation de preuve cause du d callage des obligations de preuve qui a a priori bien peu de chance d tre d montr e par cette d monstration interactive 126 Prouveur interactif Manuel Utilisateur 7 6 Utilisation de la commande Do Cases La commande dc est indispensable lorsque P x doit tre d montr avec x E E est un intervalle commande dc x E P x doit tre d montr sous les hypoth ses A gt Q x A not A gt R x et Q et R permettent de r soudre P x dc A Cette commande doit tre appliqu e si mp pr pp n a pas r ussi ou ne r ussira visiblement pas a r soudre Attention La commande pr peut d clencher des preuves par cas en fonction du but et de certaines hypoth ses Ces preuves par cas peuvent ne pas tre fond es et n cessiter de prouver plusieurs fois le m me but du au fait que les heuristiques de pr sont g n rales et peuvent tre sous optimales dans certains cas Exemple soit l obligation de preuve ETATS EO El E2 xx ETATS amp Local hypotheses amp xx EO gt xx 1 E0 E1 amp xx El gt xx 1 E0 E1 E2 amp xx E2 gt xx 1 E1 E2 amp Check that the invariant xx ETATS is preserved by the operation ref
149. n effet les preuves sur des nombres n gatifs sont souvent plus difficiles Nous choisissons donc ncl nc2 lt 0 pour P Le lecteur aura remarqu que nous utilisons de pr f rence le symbole lt plutot que gt lt gt En effet lt est un symbole de base du prouveur les autres symboles tant ramen s a lui Malgr la pr sence d un syst me automatique de normalisation il est conseill d utiliser ces symboles de base en priorit La liste de ces symboles est indiqu e dans le Manuel de r f rence du prouveur PRI gt dc nci nc2 lt 0 Starting Do Cases Le but devient nel nc2 lt 0 nel ncl nc2 2 nc2 ncl ne2 2 1 1 L hypoth se de preuve par cas est une hypoth se locale elle appara t dans le but Les consid ration pr c dentes sur le chargement des hyptoh ses locales tant toujours valides nous chargeons cette hypoth ses par dd PRI gt dd Starting Deduction Le but devient nc1 nc1 nc2 2 nc2 nc1 nc2 2 1 1 Nous n avons d charg aucun but jusque l l arbre de preuve est donc une mont e r guli re Nous pouvons le contr ler dans la zone de ligne de commande fen tre de situa tion globale dont l affichage est le suivant Force 0 dd amp dc nci nc2 lt 0 amp dd amp Next Nous nous sommes plac s dans le cas o ncl nc2 est n gatif Nous pouvons maintenant introduire l intervalle de variation du reste de la division par 2 de ncl nc2
150. nd une minute Dans cet exemple pr cis il vaudrait mieux liminer les buts interm diaires par admission au lieu de rejouer leur d monstration mais on concoit ais ment qu une telle optimisation n a rien de g n ral Autrement dit une commande Back peut provoquer le rejeu de parties enti res de d monstration pour recr er un but disparu Ces rejeux sont d ailleurs d nonc s par les messages de d but de chaque commande rejou e Starting Prover Call etc Par contre la commande Back est imm diate si il n y a rien recr er c est a dire si elle remonte un but dont le but courant est le fils Dans l exemple pr c dent il est imm diat de remonter juste avant la commande DoCases La commande ba Node permet de remonter au plus proche but parent elle est tou jours imm diate car elle ne rejoue aucune commande Dans l exemple pr c dent ba Node permet de remonter directement avant la commande DoCases En fait une commande ba Node remonte toujours au pr c dent niveau d indentation dans la ligne de commande Par exemple si l tat avant la commande est le suivant LA PHASE DE PREUVE FORMELLE 103 ah not xx e1 amp dc zz ENUM amp pr amp pr amp ah ww 5 amp pr amp pr amp Next Pour trouver le nouvel tat apr s une commande ba Node il suffit de placer Next a la place de la plus proche commande d indentation directement inf rieure en remontant ah not
151. ndice de parcours de chaque pompe et on 1 repr sente l tat d un appareil de mesure Nous consultons le composant l op ration contient une boucle dont l indice est indice_l La pr sence de 7777 indique que cette obligation concerne l tat apr s la sortie de la boucle Nous sommes donc en train de v rifier que cette boucle a bien construit ce qui tait pr vu dans la sp cification Le commentaire du but est Check that the invariant pumpon pumpon 1 is preserved by the operation Dans la sp cification de cette op ration nous avons effectivement crit pumpon 1 NB_PUMP x FALSE lt TRUE gt l_wpok gt TRUE FALSE gt on 1 Ce qui indique que cette variable doit tre construite partir du tableau ot toutes les pompes sont FALSE en ajoutant si on TRUE le tableau _wpok L interpr tation du but est finie L interpr tation correcte du but n cessite la connaissance du composant et de ses niveaux adjacents Nous conseillons de garder ces fichiers ouverts en ic nes dans un coin de l cran pendant les phases de preuve Attention ne pas les laisser affich s les fen tres de preuve doivent rester toutes visibles en juxtaposition Il vaut souvent mieux faire une relecture de ces composants au d but de la session de preuve Le sens de beaucoup de PO apparait alors clair sans m me avoir regarder nouveau les fichiers Notons que lorsque le prouveur interactif est lanc il est possible d
152. ng Prover Call Current PO is Initialisation 1 Unproved saved Unproved Goal c3 lt 100 gt 0 lt 400 c1 c2 c3 c4 End PRI gt pr Starting Prover Call Current PO is Initialisation 1 Proved saved Unproved 94 Prouveur interactif Manuel Utilisateur Goal Check gt c1 c2 c3 c4 0 400 End Apr s l ajout de l hypoth se sur c3 le c ur de preuve a pu finir seul la d monstration comme nous le voyons dans la derni re commande pr le nouvel tat est Proved saved Unproved ce qui veut dire que l tat courant est Proved et que nous n avons pas encore sauv L arbre de preuve final est Force 0 amp pr Red amp ah c2 lt 100 amp pr amp dd amp ah c3 lt 100 amp pr amp pr amp Next Dans cette d monstration nous avons guid le prouveur en lui proposant des expressions interm diaires d montrer Nous avons pu ainsi faire aboutir cette d monstration sans chercher aucune r gle Un exemple de preuve par cas Soit d montrer le lemme suivant Local hypotheses at 7 6 5 4 3 2 1 A Check ref 3 3 gt ax 1 2 3 4 5 6 7 Le c ur de preuve en force 0 et le prouveur de pr dicats chouent sur ce lemme En effet la seule mani re de d montrer ceci est de v rifier l galit de chacun des ensembles 17 6 5 4 3 2 1 et 1 2 8 4 5 6 7 ce qui revient faire sept cas sur la valeur de zz De telles preuves par cas sont rarement d clenc
153. ns THEORY ModProps IS x NATURAL gt x mod 3 0 2 END Puis nous utilisons la commande PmmCompile pc pour charger le fichier dans le prou veur PRI gt pc Loading theory ModProps Apr s avoir charg les hypoth ses locales par une commande Deduction dd nous allons utiliser la r gle ajout e dans notre d monstration Cette r gle ne convient pas directement pour le but cc mod 3 0 100 elle conviendrait pour le but cc mod 3 0 2 Nous allons donc ajouter cette derni re expression comme une nouvelle hypoth se commande AddHypothesis ah Le prouveur nous demande de la d montrer ce que nous pouvons faire avec la r gle ajout e il faut employer la commande ApplyRule ar La r gle produit le but cc N que le c ur de preuve d montre directement commande pr l hypoth se nouvelle est alors accept e et le but devient ce mod 0 2 gt cc mod 3 0 100 Ce dernier but est directement d montr par le c ur de preuve la d monstration est termin e Le d roulement de cette d monstration est montr ci dessous tel qu il appara t dans la fen tre de commandes du prouveur interactif 72 Prouveur interactif Manuel Utilisateur PRI gt ah cc mod 3 0 2 Starting Add Hypothesis Current PO is Initialisation 1 Unproved saved Unproved Goal cc mod 3 0 2 End PRI gt ar ModProps 1 0nce Starting Apply Rule Current PO is Initialisation 1 Unproved saved Unproved Goal
154. ns ETUDES DE CAS 143 ncl ncl nc2 2 nc2 ncl nc2 2 0 Si ncl nc2 est divisible par 2 le calcul entier est indentique au calcul r el il donne donc 0 Si ncl nc2 n est pas divisible par 2 le reste est 1 donc l expression consid r e vaut 1 ou 1 Ceci n est pas une d monstration bien entendu mais une mani re de comprendre pourquoi cette obligation de preuve est juste C est la d monstration intuitive voqu e dans ce document Commen ons la preuve formelle Apr s chargement de l obligation de preuve la zone d affichage du but contient la formule suivante Local hypotheses A nel 0 150 A nc2 0 150 A cl l ncl 4 4 A c2 1 nc2 4 4 A ncl nc2 lt c1 1 c2 1 A ncl ncl nc2 2 0 150 A nc2 ncl nc2 2 0 150 A nmesure 1 1 E N A ntransfert 1 1 N A Check operation refinement ref 11 gt ncl ncl nc2 2 nc2 ncl nc2 2 1 1 En effet les hypoth ses locales ne sont pas encore charg es La premi re chose a faire est de lancer la preuve pour voir ot elle s arr te conform ment la m thode d crite au paragraphe Il suffit de lancer la commande pr et d observer le but qui apparait 0 lt 1 ncl nc2 2x nel nc2 2 Nous constatons que le prouveur cherche d montrer que l expression apr s simplification est inf rieure ou gale 1 Ceci est une moiti de la preuve initiale consistant d montrer Vappartenance
155. ns LA PHASE DE MISE AU POINT 47 Mais plut t DEFINITIONS card_ens card ens 5 5 4 Rechercher les formes canoniques des expressions arithm tiques Toutes les forces du prouveur utilisent le Solveur arithm tique qui met les expressions arithm tiques dans une forme canonique avec un ordre constant des variables entre elles Ainsi les chances de succ s par correspondance litt rale sont augment es En force 0 pour des raisons d efficacit seuls les pr dicats enti rement arithm tiques a b ou a lt b sont transform s par le Solveur arithm tique Il se peut donc que la forme brute apparaisse dans l obligation de preuve m lang e avec la forme canonique produisant des asym tries g nantes Par exemple jj 1 lt ii jj 1 0 sera vu par le prouveur comme 1 jj lt ii gt ti jjt 1l o La normalisation du prouveur a provoqu l inversion des termes j7 et 1 La r gle simple 1 amp j 1 lt i ne peut dons pas s appliquer directement Il n est pas possible de mettre toujours les expressions arithm tiques directement dans la forme canonique Nous nous contenterons de conseiller de mettre les constantes num riques gauche et de classer les variables dans l ordre d apparition du composant c est a dire l ordre dans lequel ces variables apparaissent dans l invariant 5 6 La preuve rapide Nous d signons par le terme preuve rapide les d monstrations interactives trouv es en quelques minutes au
156. ns le cycle de d veloppement lors de l criture de l implantation du composant car c est seulement ce moment que l Atelier B peut savoir que la constante ne sera pas implant e Le but sera Jfact facte N N A Vnn nn N fact nn 1 nn 1 xfact nn A fact 0 1 Un telle d monstration nous oblige exprimer la factorielle sous forme d une d finition directe puisque le seul moyen de prouver un but existentiel est de proposer une valeur Ici fact Ann nn N ii ii 1 nn 21 Comme nous sommes oblig s d crire cette d finition autant la faire figurer dans le com posant Il est toutefois utile de laisser les propri t s pr c demment crites afin de les avoir en hypoth se pour la preuve cela remplace la connaissance math matique de la factorielle qui n est pas dans le prouveur Bien str il faudra prouver ces propri t s Nous pouvons crire ABSTRACT CONSTANTS fact PROPERTIES fact EN NA Vnn nn EN gt fact nn 1 nn 1 xfact nn A fact 0 1 A fact Ann nn e N ii ii 1 nn ii Dans ce cas nous devrons prouver les propri t s de la factorielle lors de l implantation du composant ou bien ABSTRACT_CONSTANTS fact PROPERTIES fact Ann nn N ii ii 1 nn ii ASSERTIONS 52 Prouveur interactif Manuel Utilisateur fact EN NA Vnn nn EN fact nn 1 nn 1 xfact nn A fact 0 1 A Dans ce cas nous ferons la
157. ntions il n en n est rien La coh rence globale de la th orie nous impose de consid rer que Tout nonc est VRAI sous des hypoth ses fausses Nous verrons plus loin des exemples dans lesquelles cette n cessit apparait Cette notion premi re RAPPELS DE PREUVE FORMELLE 5 vue tr s abstraite est souvent employ e dans la mise en ceuvre du langage B La g n ration des obligations de preuve d un composant B dans certains cas peut et doit produire des obligations de preuve contradictoires voir paragraphe 5 8 Ces derni res sont JUSTES et participent la preuve du composant 2 3 Le calcul propositionnel Intuitivement une proposition logique peut tre d finie comme une affirmation vraie ou fausse Par exemple la maison est blanche est une proposition logique car la question cette phrase est elle vraie ou fausse a un sens Par contre la maison n est pas une proposition logique Une proposition logique est d sign e par le terme de pr dicat Soient P et Q deux pr dicats On d finit les notations suivantes eP A Q Pet Q e P gt Q P implique Q e P n gation de P Ces notions sont utilis es en preuve formelle par les r gles suivantes pour d montrer P A Q sous les hypoth ses HYP il suffit de d montrer P sous HYP puis de d montrer Q sous les m mes hypoth ses pour d montrer P Q sous les hypoth ses HYP il suffit de d montrer Q sous les hypoth ses HYP augment
158. ntr es paraissent justes Y non v rification compl te oui Y PREUVE FORMELLE ch 6 faire la d monstration formelle des PO non automatiquement d montr es Y oui il reste des PO fausses A non Y 4 FIN Attention ce que nous appelons mise au point d signe implicitement la mise au point du point de vue preuve nous n abordons pas dans ce manuel les m thodes g n rales pour crire et contr ler des projets en langage B Faut il avoir fini la phase de mise au point de tous les composants du projet avant de passer en phase de preuve formelle Faut il finir compl tement la mise au point d un composant avant d crire le composant suivant Nous resterons volontairement impr cis sur ce sujet qui d pend de la taille et de la structure du projet Tout au plus peut on dire qu il ne faut pas attendre d avoir crit tous les composants du projet avant d aborder les probl mes de preuve et qu il ne faut pas entreprendre trop t t la preuve formelle d un composant Durant la phase de preuve formelle on suppose ne plus avoir retoucher les composants sauf si une obligation de preuve suppos e juste est en fait fausse Dans ce cas l impact des modifications sur les d monstrations d j faites peut provoquer des pertes de temps C est pourquoi la phase de mise au point est tr s importante Les changements de phase de pre
159. obligations de preuve du composant L ajout de telles propri t s est une cons quence du travail de preuve et n cessite une bonne exp rience du prouveur et de son fonctionnement ceci afin d viter d ajouter des assertions qui ne seront d aucune utilit car mal exprim es ou ne modifiant pas le chemin de preuve Il faut toutefois faire attention lors de la modification de ces assertions car il est possible de provoquer des r gressions de preuve Supposons qu une obligation de preuve P soit d montr e de mani re interactive sous les hypoth ses H et les assertions A Que se passe t il si une assertion B est ajout e En toute logique si INDICATIONS UTILES POUR LA PREUVE 125 HAA P est vrai on a obligatoirement HAAAB P L obligation de preuve est donc toujours d montr e et sa d monstration interactive est conserv e Si maintenant une assertion est supprim e car jug e inutile soit l assertion B et que l on avait HAAAB P alors on ne peut plus conclure a priori sur HAA P Le g n rateur d obligations de preuve consid re que cette obligation de preuve n est plus prouv e mais n efface pas la d monstration interactive sauvegard e Dans ce cas le d clenchement du prouveur automatique en mode Prove Replay permet de reprouver cette obligation de preuve Supposons que cette suppression d assertion est coupl e d autres modifications du com posant qui induisent une modificatio
160. oir par exemple le composant tests dont le fichier pmm associ contient la th orie User_Pass THEORY User_Pass IS mp pp rp 0 dd 0 amp ap END Cette th orie d finit les d monstrations interactives que l op rateur d sire voir essay es On voit que pp rp 0 sera essay apr s dd 0 amp ap Chaque ligne du bas de la th orie vers le haut sera alors appliqu e tant qu il reste une obligation de preuve non prouv e On obtient alors par s lection du bouton Prove User_Pass une trace d ex cution comme suit Loading theory User_Pass Proving tests Proof pass User_Pass 1 still 8 unproved PO clause Initialisation clause AssertionLemmas Spe clause op Proof pass User_Pass 2 still 6 unproved PO clause Initialisation clause AssertionLemmas clause op Proof pass User_Pass 3 still 5 unproved PO clause Initialisation clause AssertionLemmas clause op INDICATIONS UTILES POUR LA PREUVE 119 On s apercoit que dd 0 amp ap User_Pass 1 permet de d montrer 2 obligations de preuve pp rp 0 User_Pass 2 permet de d montrer 1 obligation de preuve mp User_Pass 3 permet de d montrer 3 obligations de preuve Par contre le param tre de coupure du prouveur de pr dicats ne peut plus tre utilis dans ces conditions Il est toutefois possible de superviser le temps de calcul du prouveur de pr dicats et Vemp cher de passer trop de temps sur certaines obli
161. on de variable e Variable tout identifiant non pr d fini constitu avec certaines r gles de lettres chiffres et _ est une variable Pour des raisons d implantation de l Atelier B les variables une lettre ne sont pas au toris es ce sont des Jokers voir paragraphe 6 2 2 La notion de variable nous permet d introduire une notion essentielle le pr dicat universellement quantifi Si v est une va riable et P un pr dicat on a la construction suivante e Vu P lire pour tout v P Nes r gles syntaxiques pr cises d finissant une variable sont donn es dans le manuel de r f rence du langage B RAPPELS DE PREUVE FORMELLE 7 On dit que le pr dicat P est quantifi par la quantification universelle Vv On dit aussi que la port e de la variable quantifi e v est le pr dicat P Donnons quelques exemples de pr dicat quantifi VarlareN A xx lt 10 gt xx lt 100 Vvar var 10 gt var lt 100 Remarquons que pour des raisons de typage on impose que tout pr dicat universelle ment quantifi soit mis sous la forme Ww P gt Q Une autre remarque essentielle est que le nom de la variable quantifi e n importe pas On dit que la variable quantifi e est une variable muette Par exemple Vax xx 10 gt xx lt 100 est quivalent a Vyy yy 10 gt yy lt 100 La port e de la variable muette x dans Vx P est le pr dicat P uniquement En particulier une variable de m me nom peut
162. ot b 0 gt a mod b 0 b 1 Comme pr c demment nous devons introduire cet intervalle de variation avant l appari tion des deux sous buts Il faut d j charger l hypoth se locale ncl ncl lt 0 actuelle ment dans le but elle est en effet n cessaire pour pr ciser l intervalle de variation du reste Nous devons faire ce chargement sans utiliser le prouveur PRI gt dd Starting Deduction Le but devient nc1 nc1 nc2 2 nc2 nc1 nc2 2 1 1 Nous proc dons comme pour le premier cas de la preuve PRI gt ah nci nc2 mod 2 0 2 1 Starting Add Hypothesis Le but devient nci nc2 mod 2 0 2 1 La r gle qui convient est la deuxi me de la th orie IntDiv PRI gt ar IntDiv 2 0nce Starting Apply Rule Le but devient ncl nc2 N Nous essayons naturellement de d charger ce but par un appel au prouveur pr Malheu reusement cette preuve choue malgr la pr sence de l hypoth se clef ncl nc2 lt 0 Cette hypoth se n a manifestement pas t utilis e c est loccasion d employer le proc d consistant faire repasser des hypoth ses dans le prouveur voir paragraphe 6 7 2 PRI gt ah not nci nc2 lt 0 Starting Add Hypothesis Le but devient ncl nc2 lt 0 gt ncl nc2 N L hypoth se existant d j telle quelle il n est pas demand de refaire sa d monstration Nous pouvons relancer la preuve 152 Prouveur interactif
163. ou veur apr s chaque modification ce serait trop lourd Pour que les modifications soient prises en compte il faut utiliser la commande PmmCompile pc Nous allons maintenant pr senter un exemple complet d utilisation Soit d montrer le lemme suivant Local hypotheses A cece ENA cc lt 2147483647 N Check that gt LA PHASE DE PREUVE FORMELLE 71 ec mod 3 0 100 Le coeur de preuve ne contient aucune r gle concernant le modulo ce dont nous pouvons nous rendre compte par la commande SearchRule PRI gt sr All a mod b Searching in All rules with filter consequent should contain a mod b Starting search Found O rule s for this filter Il est donc clair qu il ne peut pas d montrer ce lemme Le prouveur de pr dicats commande PredicateProver pp choue galement La seule mani re de r soudre ce probleme est d ajouter une r gle qui introduira la connaissance math matique manquante Il suffit d ouvrir le fichier composant pmm dans le r pertoire de base de donn e projet pour ajouter la r gle Vous pouvez diter ce fichier avec votre diteur pr f r ou bien choisir l option Edit PO methods dans le menu Show Print de la fen tre de situation globale du prouveur interactif Ce choix provoque louverture en dition du fichier de r gles correspondant au composant en cours de preuve de plus ce fichier est cr s il n existait pas Dans ce fichier de r gle nous tapo
164. our simplifier le but en P y gt Q y avec y variable s fraiche s et le r soudre pp pour r soudre pp rp 0 si le but peut se d montrer sans hypoth ses A Vv Bl il est possible d utiliser mp pr pour simplifier le but et r soudre pp pour r soudre ar SplitOr 1 Once si l on veut orienter la preuve vers not b ar SplitOr 2 Once si l on veut orienter la preuve vers not a A A By il est possible d utiliser y gt a gt b 115 116 Prouveur interactif Manuel Utilisateur mp pr pour simplifier le but d composer et r soudre la E il est possible d utiliser ss pour simplifier tout pr dicat ensembliste mp pr pour simplifier le but et le r soudre pp pour r soudre pp rp 0 si le but peut se d montrer sans hypoth ses a b il est possible d utiliser ap pr mp pp pour r soudre eh si a et b apparaissent dans d autres galit s la lt b a lt b a gt b a gt b il est possible d utiliser ap pr mp pp pour r soudre bfalse il est possible d utiliser fh H avec H hypoth se contradictoire P x avec x E et E ensemble num r ou intervalle r duit dc x E pour tenter de d montrer P x pour toutes les valeurs possibles de x Toutes ces indications sont g n rales et n entendent pas prendre en com
165. oved Proved Proved Proved Proved Proved Proved Unproved Proved Proved Proved Proved Proved Unproved Proved Proved Proved Proved Proved Proved Proved Proved Proved No current PO lt TACHES lt gt PASSWORDS gt IDENTITES dom lt gt PORTS tconnait tport pp ntt ww tident lt ntt gt pass ww taches ntt dom tident lt ntt gt pass ww taches ntt tport ntt gt pp taches ntt lt gt PORTS dom tport ntt gt pp taches ntt tconnait tport pp ntt ww tt tconnait ntt tconnait tt taches ntt tident lt ntt gt tident tt taches ntt gt dom tident lt ntt gt tident tt taches ntt tport ntt tport tt taches ntt lt gt PORTS dom tport ntt tport tt taches ntt tconnait ntt tconnait tt tt 0 taches tt lt TACHES tt lt lt tconnait taches tt lt gt PASSWORDS tt lt lt tident taches tt gt IDENTITES dom tt lt lt tident taches tt tt lt lt tport taches tt lt gt PORTS dom tt lt lt tport taches tt tt lt lt tconnait tt 0 pass tt lt lt tport tt gt pp taches lt gt PORTS dom tport tt gt pp taches Nous d cidons de d montrer la sixi me obligation de fork PRI gt go fork 6 Current PO is fork 6 Unproved saved Unproved Command
166. ples qui aident le prouveur Suivre les conseils du paragraphe 5 5 Tenter ventuellement une d monstration rapide En cas de succ s l obligation est limin e et sa d monstration peut se g n raliser liminant ainsi d autres obligations Attention il ne faut surtout pas d marrer une phase de preuve formelle Suivre les conseils du paragraphe 5 6 Dans l exemple que nous avons trait chaque tape nous pouvons faire certaines re marques sur la forme de l expression qui appara t dans le but 1 NB_PUMP x FALSE amp TRUE l_wpok gt TRUE FALSE gt on 1 Il serait peut tre plus naturel de faire appara tre explicitement les deux cas suivant la valeur de on 1 Nous aurions alors deux expressions plus simples 1 NB_PUMP x FALSE lt l_wpok gt TRUE et 1 NB_PUMP x FALSE En fait la premi re expression se simplifie puisque _wpok est une fonction totale de 1 NB_PUMP dans BOOL Elle devient _wpok tout seul Faut il reporter ces simplifications ce n est pas vident Mais si nous d cidions de faire une phase de simplification des expressions ces id es trouveraient s rement leur emploi il faut donc les noter Nous pouvons galement tenter une d monstration rapide de cette obligation L examen de cette PO nous incite faire deux cas suivant la valeur de on 1 En fait en d marrant cette preuve par cas avec une commande DoCases on aboutit directement Avec de l
167. ploy e 112 Prouveur interactif Manuel Utilisateur Il est n anmoins souhaitable de pouvoir liminer une r gle inutile pour limiter le travail de validation des r gles manuelles Nous conseillons de remplacer la r gle par une r gle inapplicable par exemple THEORY MyRules IS empty_rule places 1 et 2 vides empty_rule a a b a mod b r gle num ro 3 END Dans l exemple ci dessus le mot empty_rule ne peut coincider avec un but math matique valide 6 8 3 Le changement de force en cours de preuve Normalement une d monstration manuelle se fait en force 0 voir paragraphe 6 1 Il se peut toutefois qu au cours d une d monstration interactive l op rateur ait l intuition que la difficult de la PO correspond a une particularit de l une des forces du prouveur voir paragraphe Il faut alors essayer la force en question avec un simple appel au coeur de preuve sans perdre la d monstration interactive en cas d chec La commande ff permet de se replacer dans la m me position dans une force diff rente Par exemple si la d monstration actuelle est Force 0 amp pr amp ar OrderXY 63 0nce amp pr amp Next La commande ff 1 cette tape indique qu il faut refaire le chargement des hypoth ses en force 1 puis refaire toutes les commandes Le premier appel au coeur de preuve a un effet tr s diff rent en force 1 c est pourquoi il est peu probable que le
168. poth ses en commun avec les premi res et le traitement de ces hypoth ses est factoris Les performances sont tr s indicatives elles sont indiqu es en pourcentage d obligations de preuve d montr es sur un projet standart enti rement juste Les performances des forces 1 2 et 3 sont indiqu es en gain par rapport a la force pr c dente parce que les 26 Prouveur interactif Manuel Utilisateur forces 1 2 et 3 s emploient toujours en s quence a partir de la force 0 Ainsi les forces les plus lev es ne peuvent traiter des lemmes d montr s dans une force inf rieure ce qui conomise le temps de calcul et limite le risque de d clencher des boucles infinies La force Rapide s emploie seule La force O est consid r e comme l optimum entre l efficacit et le temps de calcul C est cette force qui doit tre utilis e pour tenter de d montrer les obligations de preuve avant m me de les lire afin de limiter leur nombre Elles sont en effet tr s nombreuses on compte en moyenne une obligation de preuve par ligne de code ex cutable produite La force Rapide n a pas des performances suffisantes pour cet emploi Les forces 1 2 et 3 s emploient plut t en parall le durant les phases de mise au point et de preuve formelle en esp rant que certaines obligations de preuve seront d montr es automatiquement avant d avoir t trait es manuellement Les principes d utilisation des forces du prouveur de
169. ppel au c ur de preuve pour traiter le premier but fils l op rateur a encore fait un appel au c ur de preuve pour traiter le deuxi me but fils le mot clef Next n est d cal que par rapport Force 0 ce qui signifie que le prochain but a traiter n est plus un fils du but initial de la PO Autrement dit la preuve de cette PO est finie ce qui est signal par la couleur verte de la zone du but Dans cet exemple la d monstration aboutit L interface signale ce succ s en colorant en vert pomme la zone du but et en interdisant les autres commandes de preuve L arbre de preuve de notre exemple est Chargement de la force et de la PO commande DoCases commande pr commande pr Le lecteur l aura compris l objectif en d monstration interactive est de ramener gauche le mot clef Next La position de ce mot clef permet de savoir si le but courant est un but fils du pr c dent Un cas typique o le rep rage par la ligne de commande est n cessaire est celui o une commande pr Red a cr plusieurs sous buts Par exemple Force 0 pr Red ah not EE pr amp pr amp Next Ici Pop rateur a commenc par lancer le c ur de preuve en mode r duit Celui ci choue LA PHASE DE PREUVE FORMELLE 91 sur l un de ses sous buts l op rateur l aide en lui rajoutant une hypoth se commande AddHypothesis qu il d montre par pr un deuxi me pr lui permet alors de d
170. principe de la preuve interactive 3 3 Conclusion yeah ias ae TERT 5 4 1 Conseils pour l interpr tation des buts 1 10 10 10 12 15 16 20 21 22 23 23 25 26 ii TABLE DES MATIERES eid de a Oe ates eh Al ee eee 41 a eg we EG eee SS 42 5 4 5 Notes et essais ee 44 e fe ee A 44 aa or 45 AAA BE dan 45 o 46 a a a as 46 47 J kree Sct a atest Tent Se eo Theo ak ke ee oR he ee ee A7 5 6 1 Trouver une d monstration rapide 47 D od P he SN en ee D 48 HG a Rare di Hi sue res dei 48 5 7 1 Les buts existentiels particularisables 49 5 7 2 Les buts existentiels abstraits 51 pura Fk She de 8 a 52 A Ooo 52 Porc 53 55 Oe de o a oe ee 56 bios Riad Mo Reds o 60 6 2 1 Les commandes du prouveur interactif 60 beg bw pie RR A D ER wd 4 RAT RE 64 RUE a pa Rw 69 A gi His bn ees a Seo Se 72 de Choe De ae ds HA Oe Done rd hae 74 6 3 L utilisation de interface du prouveur interactif 76 sadia Res we GOR wi Ga ee DRA oe de eS 76 ee 48e 4 78 os Oe ee ee ee ee ee Ge ree 89 Ce ee or te eg ee ae ee E E aye ee 91 6 5 1 Prouveur et prouveur de pr dicats 91 Sa GS eee RR ERE REDS ES 92 AA 96 a a ee aoe dl e ee te a a 98 6 6 Utilisation avanc el 4 444440 98 TABLE DES MATIERES iii 6 6 1 La v rification finale
171. pte toutes les sp cificit s des projets de preuve imaginables N oubliez pas avant de vous lancer de la preuve interactive de v rifier que l obligation de preuve que vous voulez d montrer est juste 7 2 Quand et comment utiliser le prouveur de pr dicats 7 2 1 R duction du nombre d hypoth ses Le prouveur de pr dicats s utilise lorsque mp et ou pr ont chou Ces 3 prouveurs ont des domaines qui se recouvrent partiellement Contrairement 4 mp ou pr pp ne fonctionne correctement qu avec un jeu r duit d hypoth ses On peut estimer que le temps de calcul suit une loi exponentielle en fonction du nombre d hypoth ses Aussi il n est pas envisageable d utiliser pp tel quel pour d montrer une obligation d un projet surtout si le composant en question voit et ou importe d autres composants Il faut alors r duire le nombre d hypoth ses Trois techniques sont utilisables s lection des hypotheses ayant un symbole en commun avec le but La principale limitation est que l on ne peut pas contr ler finement la s lection et que si un des symboles du but appara t dans beaucoup d hypoth ses pp va s av rer inefficace Exemple pp rp 1 pour s lectionner les hypoth ses qui ont un symbole en commun avec le but s lection des d hypoth ses en fonction de leur origine Les hypoth ses sont s lectionn es par paquets sans qu il soit possible d en retirer Exemple pp rp loctinv pour s lectionner les hypoth ses
172. qu un r sum destin faciliter l uti lisation de l Atelier B il ne s agit en aucun cas d un cours de math matique dont il n a d ailleurs pas la rigueur Les notions suivantes sont pr sent es de mani re intuitive et informelle dans l ordre de la construction du B Book 4 Prouveur interactif Manuel Utilisateur 2 1 Les symboles L criture math matique est tres riche en symboles inhabituels en informatique Nous utilisons par exemple l implication la surcharge lt etc Ces symboles n cessaires pour une criture synth tique des formules ne sont pas disponibles sur un clavier d ordinateur Pour cette raison ils sont repr sent s par des combinaisons de caracteres ASCII par exemple gt est repr sent par gt Dans tous les documents il est pr f rable d utiliser la notation symbolique qui facilite la lecture plut t que la notation ASCII En particulier nous n utiliserons pas la notation ASCII dans ce manuel Pour chaque symbole la correspondance ASCII est donn e dans le manuel de r f rence du langage B vous en aurez besoin pour toute manipulation de lV Atelier B 2 2 Le raisonnement formel Un raisonnement formel consiste a d montrer un nonc sous un ensemble d hypoth ses a Vaide d une collection de r gles d inf rences Par exemple nous nous proposons de d montrer 8 gt 0 sous l hypoth se 8 gt 5 Notre nonc est donc 8 gt 0 et l ensemble des hypoth ses
173. r ce la commande pc On v rifie ensuite que cette r gle a bien t charg e en m moire gr ce la commande SearchRule PRI gt pc Loading theory func PRI gt sr func a Searching in func rules with filter consequent should contain a Starting search Rule list is func 1 Backward bnum a amp bnum c amp bnot btest a c Y f c d gt f lt al gt b c d End of rule list Elle peut maintenant tre utilis e notamment au sein d un appel tendu au prouveur automatique Dans ce cas particulier la th orie func va tre utilis e en compl ment des regles et m canismes natifs du prouveur Le mode trace du prouveur est utilis afin de visualiser l action de la r gle func 1 Il faut noter d ailleurs que si la r gle n tait pas quip e du syst me de trace terme bcalll BackwardRule func 1 son d clenchement ne serait pas visible dans ce mode PRI gt pr Tac func Ru Goal None INDICATIONS UTILES POUR LA PREUVE 131 Starting Trace in mode Ru Goal None NoFile NoSimpl Starting Prover Call After deduction goal is now tab 1 lt 0 gt 0 lt 1 gt 1 lt 2 gt 1 lt 3 gt 0 lt 4 gt 1 lt 5 gt 0 lt 6 gt 1 lt 7 gt 0 0 0 By applying atomic rule func 1 bnum a amp bnum c amp bnot btest a c f c d gt f lt al gt b c d the goal tab 1 lt 0 gt 0 lt 1 gt 1 lt 2 gt 1 lt 3 gt 0 lt 4 gt 1 lt
174. r ApplyRule Nous allons voir un exemple de ce proc d Consid rons le lemme suivant LA PHASE DE PREUVE FORMELLE 97 FEN NA f10 50 C 0 100 A ff 51 100 0 100 gt ff 0 50U51 100 0 100 Rappelons que l image fonctionnelle f E d signe l ensemble des images par f des l ments de E L image fonctionnelle d une r union d ensembles est gale la r union des images fonctionnelles de chaque sous ensemble Bien que cette r gle semble claire pour l utiliser dans une d monstration il faudrait la d montrer rigoureusement Heureusement comme nous allons le voir cette r gle existe dans la base de r gles Cette r gle permettrait de r crire le but en H10 50 U 51 100 C 00100 ce qui est plus directement li aux hypoth ses Nous avons l intuition que ce but plus simple serait d montr pour le v rifier nous pouvons ajouter cette expression par une commande ah ah ff 0 50 ff 51 100 lt 0 100 Une simple commande pr d montre cette hypoth se Nous avons utilis la commande AddHypothesis pour tester si un but se d montre facilement Nous pouvons revenir au d but de l obligation et rechercher la r gle qui convient PRI gt sr Rewr f a b Analysons la syntaxe de cette commande SearchRule le mot clef Rewr indique que nous cherchons une r gle de r criture afin de pouvoir transformer ff 0 50 U 51 100 qui est une sous formule du but Le filtre f aUb
175. r en utilisant une r gle si op rateur change cette r gle lors de la d monstration d une autre obligation de preuve il se peut que la d monstration initiale ne marche plus Comme elle n est pas rejou e l tat de la PO reste quand m me Proved De plus en cours de preuve l op rateur peut avoir ajout des r gles provisoires dont il n est pas s r Si ces r gles sont supprim es la fin de la preuve il faut v rifier que les d monstrations peuvent tre refaites quand m me De tels rejeux de preuve se font la fin ou plus rarement de temps en temps sur des composants dont la preuve interactive prend plusieurs jours Pour effectuer ces rejeux de preuve la m thode suivre est la suivante 1 Dans l Atelier B au niveau du projet hors du prouveur interactif choisir le com posant concern et s lectionner l option Unprove dans le menu Prove Ceci remet toutes les obligations dans l tat non prouv 2 Dans ce m me menu Prove choisir l option Automatic Replay Ceci provoque le rejeu de toutes les d monstrations telles qu elles ont t enregistr es c est dire qu une PO d montr e en force 0 est rejou e en force 0 une PO d montr e en force 2 est rejou e en force 2 une PO d montr e en force 1 avec des commandes interactives est rejou e en force 1 avec ces commandes etc 3 V rifier qu on a bien retrouv l tat de preuve de d part avec le m me nombre d obliga
176. race dans un fichier mode File de la commande pr pr c dente utiliser l option Show Proof Tree du menu Show Print dans la fen tre de situation globale du prouveur L affichage produit pour notre exemple est le suivant VCG homeb DS minitry passwd bd p StationUnix kill 5 vcg ARGED f tt lt lt Itport taches tt lt gt PORTS not tt taches Rule InRelationxy 1 Rule InRelationxY 1 HiddenPredicate mecanig dom tt lt lt Itport lt taches tt A port taches ran tt lt lt ltport lt PORTS Ha Simplify new goal HiddenPredicate mecanism dom tport tt lt taches tt Haii HARGED gt bfalse Rule InPOWXY 24 dom tport lt taches tt tt Haii Simplify new goal dom tport lt taches p lt 108 Prouveur interactif Manuel Utilisateur 6 7 Les recettes de preuve Il existe un certain nombre de m thodes adapt es des situations de preuve qui peuvent faciliter le succ s Ces m thodes consistent souvent savoir conduire la preuve vers des m canismes du prouveur pour viter d avoir a faire soi m me la preuve Un tel ensemble de m thodes est toujours perfectible avec la pratique l op rateur se constituera ses propres techniques Dans ce chapitre nous tenterons de regrouper le plus grand nombre possible de recettes efficaces 6 7 1 Les commandes par situation
177. rateur max qui n est d fini que pour un ensemble d entiers au moins non vide De telles expressions posent des probl mes concernant la preuve automatique par r gles d inf rence Nous n aborderons ces probl mes que du point de vue de leurs cons quences pratiques L outil mdelta permet de v rifier a posteriori la validit d un projet B au sens de sa bonne d finition voir Outil mdelta Manuel Utilisateur en g n rant des lemmes de bonne d finition Dans la plupart des cas ces lemmes de bonne d finition sont triviaux il suffit de les lire rapidement pour les v rifier Si l un de ces lemmes est faux alors Soit il y a des expressions mal typ es dans les composants en cours de preuve en principe cela provoque toujours l apparition d une obligation de preuve fausse que le prouveur ne d montre pas METHODE GENERALE 27 Soit l une des expressions ajout es en cours de preuve interactive est d pourvue de sens Attention dans ce cas la preuve n est pas valide il est n anmoins tr s rare qu elle puisse aboutir Le contr le de type des composants B carte la plupart des possibilit s d expressions mal form es Les problemes restants rel vent de la preuve ce sont card E si E n est pas un ensemble fini les expressions max E min si E est vide ou si E n admet pas de maximum ou de minimum les expressions f x si x n est pas dans le domaine de f ou si f est une relation mais pas un
178. rd e PRI gt sw PO op 11 saved Enfin puisque 7 des 8 obligations de preuve restantes se ressemblent cette d monstration est appliqu e commande TryEveryWhere toutes les obligations de preuve non prouv es te op 11 Begin TryEveryWhere Summary op 17 transformed Unproved gt Proved pr Tac func op 16 transformed Unproved gt Proved pr Tac func op 15 transformed Unproved gt Proved pr Tac func 132 Prouveur interactif Manuel Utilisateur op 14 transformed Unproved gt Proved pr Tac func op 13 transformed Unproved gt Proved pr Tac func op 12 transformed Unproved gt Proved pr Tac func End TryEveryWhere Consid rons maintenant la derni re obligation de preuve non prouv e tab 1 lt 0 gt 0 lt 1 gt 1 lt 2 gt 1 lt 3 gt 0 lt 4 gt 1 lt 51 gt 0 lt 61 gt 1 lt 71 gt 0 0 7 gt 0 1 Encore une fois aucune r gle du prouveur ne permet de simplifier efficacement le but Une nouvelle r gle est ajout e apres avoir v rifi sa validit grace aux outils de preuve de regles PRI gt vr Back b A gt B amp f A gt B gt f lt b A gt B The rule was proved Cette r gle est alors ajout e au fichier M1_i pmm dans la th orie simpl cette fois THEORY simpl IS bcalli BackwardRule func 1 f A gt B amp b A gt B gt f lt b A gt B END Cette r gle est alors charg e en m moire
179. rt La fen tre qui appara t a l allure suivante INTRODUCTION AU PROUVEUR 13 DemoExample INTERACTIVE PROOF Initialisation PO1 Proved PO2 Proved PO3 Unproved End Sur ce dessin nous ne montrons que l essentiel le titre DemoExample INTERACTIVE PROOF et la liste des obligations de preuve les diff rentes zones et boutons de cette fen tre sont expliqu s plus loin Une premi re remarque est que l tat Proved ou Unproved de chaque obligation de preuve est enregistr c est bien s r essentiel pour savoir quand la preuve est finie Il suffit de cliquer deux fois sur la ligne PO3 Unproved pour positionner la preuve interactive sur cette obligation de preuve Deux autres fen tres apparaissent l cran a maintenant l allure suivante 14 Prouveur interactif Manuel Utilisateur DemoExample Initialisation 3 DemoExample Initialisation 3 HYPOTHESIS hypoth ses DemoExample Initialisation 3 GOAL liste des PO but zone interactive commandes Dans la zone du but nous lisons au bout de la ligne 1 2 3 4 le d but est un commentaire C est le but faux qui d nonce l erreur et d une mani re assez analytique c est cause de l l ment 1 que 1 2 3 n est pas inclus dans 2 3 4 Attention si vous avez choisi le mode ASCII par d faut le but 1 2 3 4 est af
180. s Attempt to prove not tt taches Le but contenant des expressions qui se simplifient si tt n est pas dans taches le prouveur tente de d montrer cette proposition Obvious goal tt taches is discharged because in hypothesis HiddenPredicate mecanism is transforming goal not tt taches in bfalse Obvious goal StationUnix kill 5 is discharged because in hypothesis Obvious goal Check 4 is discharged because in hypothesis After deduction goal is now bfalse Attempt to prove bfalse fails La d monstration de tt taches choue En effet le pr dicat tt taches est en hy poth se il est donc remplac par btrue dans la proposition prouver C est le m canisme HiddenPredicate qui fait ce remplacement Avant de conclure a l chec les deux derni res hypoth ses StationUnix kill 5 et Check 4 ont t repass es dans le prouveur pour tenter de les simplifier En r sum le prouveur a fait un cycle complet pour s apercevoir que la proposition tt taches est fausse et qu il n est donc pas possible de simplifier le but en lutili sant Dans une telle trace de preuve tout ce que le prouveur a tent est trac De plus les noms des m canismes utilis s sont cit s moins d tre sp cialiste des m canismes du prouveur il n est pas question de connaitre tous ces noms Nous conseillons donc de ne pas s attarder sur chaque tape dans la trace l essentiel est de comprendre globalem
181. s 0 s End of rule list Il ne faut pas oublier que les r gles ajout es dans un pmm en cours de preuve interactive ne sont prises en compte qu apr s avoir ex cut la commande pc De m me n oubliez pas que si vous supprimez une r gle au milieu d une th orie l ordre des regles va tre modifi et donc la commande ar regle n Once peut ne plus s appliquer car du fait du d calage des r gles la r gle regle n n est plus celle que l on croit De plus si vous ajoutez retirez modifiez une ou plusieurs r gles de votre th orie la commande ar theorieutilsateur peut ne plus s appliquer D une maniere g n rale lors de modifications de vos th ories utilisateurs il est prudent de d prouver le composant consid r puis de lancer un Prove Replay pour v rifier qu il n y a pas de r gression de preuve Pour le fichier PatchProver n oubliez pas que si vous le modifiez en cours de preuve il ne sera pas recharg m me si vous quittez le prouveur interactif Il faut pour cela quitter le projet puis rouvrir le projet et lancer nouveau le prouveur interactif On ajoute une r gle lorsque les prouveurs et solveurs n arrivent pas r soudre ou a simpli fier de mani re satisfaisante le but courant Il peut s agir d une proposition logique simple mais contenant des expressions complexes qui vont g ner la mise en ceuvre efficace des heuristiques de pp Dans ce cas on ajoute une r gle correspondant au but dont
182. s appliquent aussi pour la lecture des hypoth ses Puisque la liste des hypoth ses est souvent tr s longue il faut savoir ce que l on cherche avant toute lecture c est par la justification intuitive de l obligation de preuve que la recherche des hypoth ses significatives est dirig e Si la recherche a lieu dans le prouveur interactif utiliser au maximum les fonctions de recherche qui ont t d crites dans le paragraphe 42 Prouveur interactif Manuel Utilisateur Lorsque les hypotheses significatives sont localis es il faut noter les informations n cessaires pour les retrouver Cela sera utile pour la phase de d monstration intuitive Exemple continuons toujours l exemple pr c dent Nous cherchons Vhypoth se indiquant que l indice est nul l hypoth se indiquant le type de l_wpok Nous pouvons essayer la commande ReducePo rp Si peu d hypoth ses sont s lectionn es nous aurons trouv celles que nous cherchons car elles contiennent au moins le nom de la variable concern e en commun avec le but Effectivement la commande rp retourne NB_PUMP 4AM l_wpok 1 4 BOOL A dom 1_wpok 1 4 A on 1 BOOL A on 1 TRUE gt off 1 FALSE A on on 1 A indice_1 7777 0 A indice_187777 0 NB_PUMP Nous avons trouv toutes les hypotheses utiles Nous notons que les hypoth ses utiles se trouvent par une simple commande rp 5 4 4 Conseils pour la d monstration intuitive
183. s commandes de preuve proprement dites Les plus courantes sont Prove pr appel au c ur de preuve AddHypothesis ah ajout d une hypoth se d montrable partir des hypoth ses courantes ApplyRule ar utilisation directe d une r gle du prouveur ou ajout e DoCases dc d clenchement de preuve par cas useEqualityinHypothesis eh utilisation d une galit en hypoth se SuggestforErist se proposition pour un but de la forme 3x P ParticularizeHypothesis ph instantiation d une hypoth se de la forme Vx P FalseHypothesis fh d nonciation d une hypoth se contradictoire Les commandes de position sans permettre d avancer la preuve elles servent reculer ou rejouer des commandes enregistr es 20 Prouveur interactif Manuel Utilisateur Les commandes d information sans aucune action sur la preuve elles permettent de chercher et d afficher les informations n cessaires pour progresser dans la d monstration de la PO Les commandes les plus importantes de ce type sont Search Hypothesis qui permet la recherche d une hypoth se en fonction d un certain filtre et Search Rule qui permet la recherche d une r gle dans la base de r gles Les commandes de finalisation g n ralisation d une d monstration interrup tion d une preuve qui boucle demande de la sortie d une d monstration apr s succ s etc Tous les changes entre le pro
184. s les hypoth ses Nous Vappliquons au but PRI gt ar IntDiv 1 Goal Starting Apply Rule Le but devient 0 lt 1 nc1 ne2 ncl nc2 ncl nc2 mod 2 Maintenant il ne manque priori plus rien pour que la preuve de ce sous but puisse aboutir Nous pouvons donc tenter un appel au prouveur complet PRI gt pr Starting Prover Call Le but devient ncl ncl nc2 2 nc2 ncl nc2 2 lt 1 Il s agit du deuxi me sous but n cessaire pour d montrer l appartenance l intervalle 1 1 Nous voyons que ce but n a pas t simplifi en effet le prouveur s est arr t avec l chec du premier sous but L arbre de preuve est maintenant le suivant Force 0 dd amp dc nci nc2 lt 0 amp dd amp ah nci nc2 mod 2 1 2 0 amp ar IntDiv 4 0nce amp pr amp pr amp pr amp pr Red amp ar IntDiv 1 Goal amp pr amp Next Le mot clef Next est le deuxi me tre indent imm diatement sous pr Red ce qui indique qu il s agit du deuxi me sous but g n r par cette commande celui qui correspond a la deuxi me borne de l intervalle Nous savons comme pr cedemment que la preuve de ce but ne pourra pas aboutir sans utiliser la premi re r gle de IntDiv Pour proc der a sa simplification il faut donc utiliser pr Red au lieu de pr qui tenterait des preuves par cas nuisibles 150 Prouveur interactif Manuel Utilisateur PRI gt pr Red Starting Prover Call Le
185. s obligations de preuve conduit s apercevoir tr s tard des erreurs et oblige a relire plusieurs fois les m mes obligations Les conseils essentiels sont 1 Commencer par les obligations de preuve qui semblent difficiles ce sont celles qui risquent le plus d tre fausses Bien que cette d marche soit psychologique ment difficile car l op rateur cherche souvent se d barrasser d un grand nombre de PO simples pour avancer elle nous parait souhaitable Pour trouver ces obligations difficiles Parcourir les obligations de preuve d une op ration en remontant du plus grand num ro vers le plus petit En effet le g n rateur d obligations de preuve engendre g n ralement les obligations de preuve les plus compliqu es en dernier Chercher les obligations de preuve qui concernent les parties com LA PHASE DE MISE AU POINT 37 pliqu es de Pop ration En se guidant sur la structure du composant on peut pressentir ce qui va poser probl me L ordre dans lequel les obligations de preuve apparaissent dans la liste d pend de la forme du composant N anmoins les obligations de preuve concernant les pr conditions des op rations appel es dans l op ration prouver apparaissent g n ralement au d but m me si ces appels sont la fin de l op ration D autre part dans une im plantation les obligations de preuve de non d bordement des calculs interm diaires sont au d but ces obligations serv
186. s obligations de preuve du composant tri es par clause avec leur indication d tat Un double clic sur une obligation de preuve est quivalent un Goto sur cette obligation de preuve 24 Les boutons de d placement principaux permettent le positionnement Le bouton Next permet d aller la prochaine obligation de preuve non prouv e le bouton 18 Prouveur interactif Manuel Utilisateur Goto permet l acc s l obligation de preuve d sign e dans la liste Le bouton Mathematical Demo permettra d crire dans un fichier la d monstration d une obligation de preuve 3 la zone de gestion de l obligation de preuve courante regroupe tout ce qui est sp cifique la preuve en cours c est dire l obligation qui a fait l objet du pr c dent Goto Elle contient 31 L tat de la PO courante c est dire son tat Prouv e non prouv e dans la d monstration en cours et son tat dans la d monstration sauv e 32 La fen tre de la ligne de commande contient toutes les commandes de preuve effectu es sur la PO courante indent es en fonction de l arbre de preuve 33 La d monstration sauv e contient la ligne de commande sauv e pour cette obli gation de preuve 4 Le bouton d aide lance la documentation en ligne du prouveur 5 Le bouton de fin arr te le prouveur 6 Le bouton d interruption stoppe la derni re commande de preuve interactive Son emploi le plus courant est l interruption d une command
187. s sp cifiques sont cr s en fonction des expressions trouv es dans le but Par exemple si le but contient un produit a x b avec 0 lt a et qu il existe une variable c telle que c lt b alors l hypoth se a x c lt a x b est ajout e Force 3 les r gles tentatives sont employ es Par exemple si le but prouver est a lt bet si a lt cest en hypoth se alors une sous preuve sera lanc e pour tenter de d montrer c lt b 104 Prouveur interactif Manuel Utilisateur 6 6 5 La trace de preuve Nous d signons par trace de preuve les informations fournies lors d une d monstration qui permettent de savoir comment elle s est faite Cette trace est particuli rement utile avec Vemploi de prouveurs automatiques car elle constitue la justification de la d monstration Il y a deux sortes de traces de preuve qui ont t envisag es dans le cadre de l Atelier B la production de la d monstration math matique r dig e d une obligation d montr e ou bien la trace pas pas d un appel au c ur de preuve Ce dernier type de trace sert comprendre les nouveaux buts qui peuvent appara tre apr s un appel au c ur de preuve Sur un exemple nous allons examiner la trace d un appel au c ur de preuve Avant d aborder l exemple insistons sur le fait que le tra age est rarement employ pour faire aboutir une preuve En effet le plus souvent il est inutile de comprendre exactement ce qu a fait le dernier appe
188. se du prouveur contrairement Z Pour indiquer qu une variable doit tre un entier n gatif nous crivons simplement a lt 0 sans pr ciser a Z En effet si a n est pas un entier par exemple a TRUE alors l expression a mod b est mal typ e et n a pas pu appara tre dans une obligation de preuve provenant d un composant dont le contr le de type est correct Nous vitons ainsi le symbole Z Le modulo que nous avons d crit ici est l extension Z x Z de la d finition sur N x N Si a et b sont deux entiers naturels et si b est non nul alors il existe un et un seul couple q r tel que a bq r et r lt b Par d finition q a b et r a mod b Cette d finition peut tre tendue Z x Z1 de mani re non ambig e de telle mani re que a bx a b a mod b reste vrai et que les r gles de simplification des signes d un ETUDES DE CAS 145 quotient soient naturelles C est cette d finition du modulo qui est utilis e dans Atelier B Elle est constitu e de cette galit et des r gles d appartenance du reste nous l avons donc enti rement d crite dans IntDiv La premi re r gle b a b a a mod b n a pas une forme quelconque Nous avons choisi une r gle de r ecriture qui permet d liminer une division en fabriquant un modulo ce qui nous permettra de remplacer les divisions dans le but ou dans une hypoth se De plus l criture choisie est bx a b au lieu de a b x
189. se r duit 8 gt 5 Nous supposons que nous avons tout oubli c est dire que nous voulons utiliser seulement les r gles et les hypoth ses que nous pr sentons explicitement Nous supposerons disposer des deux r gles d inf rence si 5 gt 0 et si 8 gt 5 alors 8 gt 0 r gle 1 5 gt 0 est toujours vrai r gle 2 En appliquant la r gle 1 pour d montrer 8 gt 0 comme nous supposons savoir 8 gt 5 c est notre hypoth se il ne nous reste plus qu d montrer 5 gt 0 Notre nouvel nonc est donc 5 gt 0 Nous appliquons alors la r gle 2 qui nous dit que 5 gt 0 est toujours vrai L application de cette r gle ne produit pas de nouveau but donc la preuve est finie Ces notions de preuve sont tr s intuitives et naturelles Il est n anmoins utile de bien les saisir a partir des l ments que nous venons de voir c est dire e d monstration d un nonc sous certaines hypoth ses e collection des r gles d inf rences autoris es Conventionnellement nous repr senterons l ensemble de nos hypoth ses par le mot HYP Pour indiquer que nous ajoutons une hypoth se H cet ensemble nous crirons HYP H Que se passe t il si l une des hypoth ses que nous supposons est toujours fausse Par exemple doit on consid rer que 8 lt 0 est valide sous l hypoth se fausse 5 lt 0 Intui tivement cela revient s interroger sur un cas impossible La r ponse peut sembler une affaire de conve
190. se_project create_doc_ileaf ctrans edit edit_pmm get_project_xref hiatrans infos_component lchecker_project navigator po_view pov_print_framemaker pov_print_latex pov_show_framemaker pov_show_latex pretty_print_file print_doc_latex project_status prove_patchprover remake set_native show_doc_latex show_vcg_file status_global unprove Pour guider l op rateur dans sa d monstration le prouveur fournit une information qui repr sente l arbre de preuve sous forme d une liste indent e la ligne de commandes Cette information est visible dans la zone de la ligne de commande de la fen tre de situation globale L indentation des commandes dans cette zone est capitale elle repr sente les diff rentes branches de l arbre de preuve Nous allons expliquer son usage sur des exemples Supposons que l affichage de la ligne de commande soit le suivant 90 Prouveur interactif Manuel Utilisateur Force 0 dc var TRUE amp pr amp pr amp Next Cela indique que le d roulement de la preuve a t le suivant le prouveur a t mis en force 0 dans cette force l op rateur a acc d une PO Cet acc s n est pas repr sent mais cela a cr un but sous l action de la force 0 sur ce but initial op rateur a lanc une commande DoCases dc pour faire deux cas soit var TRUE soit var TRUE la commande DoCases dc a cr des buts fils op rateur a fait un a
191. ses et la variable quantifi e xx muette La regle devrait tre gard e comme suit binhyp a b c A blvar Q A Q a b c gt a b c Concernant ce type de r gle il faut bien faire attention ce que l on fait Par exemple la r gle binhyp a b A blvar Q gt a b est fausse En effet le symbole est vu comme un op rateur Donc aa 0 qui est un identificateur parfaitement acceptable peut tre d compos en aa et 0 Supposons que les hypoth ses suivantes sont dans la pile des hypoth ses aa 1 0 xx En appliquant la r gle ci dessus 2 fois il devient possible de transformer l identificateur aa 0 en 1 xx Il faut dans ce cas manipuler le pr dicat complet Par exemple la r gle binhyp a b A blvar Q gt Oleqa Oleqb est parfaitement valide 7 4 Ajout de r gles utilisateur Il est possible qu une r gle ne s applique pas lors de l utilisation de la commande ar Il faut savoir que la recherche de r gles pouvant s appliquer sur le but commande sr propose des r gles pouvant EVENTUELLEMENT s appliquer Il faut ensuite v rifier que les gardes de ces r gles sont effectivement valu es vraies Une r gle peut ne pas s appliquer car elle est mal normalis e r gle utilisateur Il faut alors la corriger les gardes ne se d clenchent pas une hypoth se n existe pas au pr alable et v rifier que les gardes soient vraies le but n a pas exactem
192. set Repeat rr r p te la derni re commande entr e Quit qu quitte le prouveur interactif Avec l interface Motif l utilisateur peut aussi utiliser les boutons pr vus cet effet Les commandes de lecture Les deux commandes suivantes permettent la lecture des obligations de preuve SearchHypothesis sh cette commande d information permet la recherche de toutes les hypoth ses qui v rifient un certain filtre Son utilisation la plus courante est la re cherche de toutes les hypoth ses concernant une variable Utiliser SearchHypothesis d s que la recherche d hypoth ses dans la liste g n rale devient difficile showReducedPo rp cette commande affiche l obligation de preuve r duite c est a dire avec seulement les hypoth ses qui ont un symbole en commun avec le but C est ce qu il faut regarder en premier pour contr ler rapidement la justesse d une PO ou d un sous but Utiliser showReducedPo pour retrouver une d monstration intui tive ou conjointement avec SearchHypothesis Les commandes de preuve automatique 62 Prouveur interactif Manuel Utilisateur Pr sentons maintenant les deux commandes de preuve automatique Prove pr c est l appel au c ur de preuve son usage doit tre contr l en parti culier concernant les preuves par cas parasites voir paragraphe 6 8 1 Mais il ne faut pas d montrer manuellement ce que le cceur de preuve sait d montrer
193. simplifie en btrue
194. ssurer qu une obligation est fausse Reporter le contre exemple dans le composant permet de localiser l erreur 5 1 La m thode g n rale de mise au point La m thode g n rale de mise au point d un composant par la preuve consiste parcourir les obligations de preuve pour v rifier qu elles sont toutes justes A chaque obligation de preuve fausse d couverte le composant est modifi De facon a limiter le nombre de lemmes lire la phase de mise au point doit tre faite apres le passage du prouveur en force 0 La force 0 du prouveur a t pr vue pour cet usage au contraire des forces plus lev es qui sont beaucoup plus cotiteuses en temps La force 0 est le compromis id al entre la performance et le temps pour assurer la correction priori des composants voir paragraphe 4 2 La phase de mise au point par la preuve ne doit commencer que si il n y a plus de corrections visibles par la seule lecture du composant Autrement dit le composant doit avoir t relu avant la phase de mise au point par la preuve En effet il n est pas n cessaire de passer par le contr le de tr s haut niveau que repr sente la preuve si les erreurs se d tectent par simple lecture En r sum la m thode g n rale en phase de mise au point est la suivante Apr s relecture du composant et apr s avoir appliqu la preuve automatique en force 0 Parcourir les obligations de preuve restantes voir paragraphe 5 3 Examiner
195. str ceci est vident Il se trouve n anmoins que ce lemme choue en force 0 car il n y a pas de m canisme pour reconna tre une hypothese dans un but disjonctif Comment LA PHASE DE PREUVE FORMELLE 75 se d barrasser de ce but facile Une solution simple est d ajouter une r gle prot g e avec la commande Validation of Rule vr Nous pouvons ajouter la r gle b a V b V c par exemple dans la th orie NonEqui la r gle est par exemple NonEqui 1 dans le fichier Pmm du composant et en effectuer la d monstration en preuve interactive PRI gt vr Back b gt a or b or c The rule was proved Dans la commande ci dessus le mot clef Back indique qu il s agit d une r gle d inf rence normale par opposition aux r gles par l avant Le second param tre est l nonc de la regle Le prouveur signale en retour que la r gle a t d montr e avec succ s par le prouveur de pr dicats Cette regle peut tre employ e avec une commande ApplyRule PRI gt ar NonEqui 1 Once Starting Apply Rule Current PO is Initialisation 1 Unproved saved Unproved Goal 22 20 30 End Il suffit alors d un seul appel au coeur de preuve pour terminer la d monstration Il n y a aucune v rification compl mentaire faire sur cette r gle ajout e elle a t d montr e par le prouveur de pr dicats 76 Prouveur interactif Manuel Utilisateur 6 3 L utilisation de l interface du prouveur interactif L in
196. t 0 lt 2 card ens card ens N ee C est a dire que la preuve se r sume maintenant d montrer la n gation de cette formule Pour des raisons de coh rence de la preuve il est impossible de supprimer une hypoth se c est pourquoi la formule est toujours en hypoth se Ce n est pas g nant car l hypoth se P west pas employ e pour d montrer P Nous pouvons tenter la preuve PRI gt pr Starting Prover Call Le but devient 0 lt card v1 1 N v2 1 card v1 1 v2 1 N v3 1 card v1 1 v2 1 v3 1 N ee 140 Prouveur interactif Manuel Utilisateur C est bien compliqu Il faut encore aider le prouveur avant de lancer cette preuve Reve nons en arri re PRI gt ba Le but redevient 0 lt 2 card ens card ens N ee Relancons la preuve en mode r duit pour que le but soit simplifi sans preuves par cas ou remplacements exploratoires Nous appliquons ainsi pr cis ment la m thode d crite au chapitre PRI gt pr Red Starting Prover Call Le but devient 0 lt 3 card ens card ens N ee Comment aider la preuve cette tape L expression ens N ee repr sente l ensemble vide une telle simplification dans le but est s rement b n fique Nous pouvons essayer d attirer l attention du prouveur sur ceci PRI gt ah ens ee Starting Add Hypothesis Le but devient ens N ee Y Tentons de d montrer ceci PRI gt pr Starting Prover Call Le bu
197. t guider l op rateur pour savoir quelle commande appliquer et pourquoi La lecture de ce manuel n cessite la connaissance du langage B et quelques notions sur Atelier B La preuve est une activit difficile n cessitant une bonne disponibilit de l information Nous conseillons d quiper tout poste de travail de preuve des documents suivants le manuel de r f rence du langage B Il contient la d finition de chaque sym bole math matique les propri t s essentielles et des exemples significatifs de plus l quivalent ASCII de chaque op rateur y est indiqu le B Book chapitres 1 2 et 3 Il contient la construction logique de toutes les notions math matiques utilis es en preuve le manuel de r f rence du prouveur interactif il d crit la syntaxe des commandes de preuve le manuel utilisateur du prouveur interactif le pr sent manuel il indique la marche suivre dans le cadre de la m thode de preuve que nous proposons 2 Prouveur interactif Manuel Utilisateur En plus de ces documents l op rateur pourra utiliser la carte m mo du prouveur inter actif pour un acc s rapide aux commandes et le manuel d utilisation des obligations de preuve qui indique comment interpr ter chaque obligation de preuve Plan g n ral Le chapitre 2 est une introduction la preuve formelle math matique telle qu elle est ap pliqu e dans Atelier B Si vous n tes pas familier avec les
198. t tre telle que toutes les pompes sont contr l es En regardant l op ration on voit que cet indice parcourt les num ros de pompes en d croissant il est nul quand la boucle est finie Donc l intervalle 7777 1 NB_PUMP est gal 1 NB_PUMP cet intervalle sert restreindre la partie droite de l expression qui est manifestement une fonction de 1 NB_PUMP dans BOOL Cette restriction peut donc tre enlev e et le but devient une galit litt rale Nous notons remplacer l indice par sa valeur pour liminer la restriction dans le terme de gauche Ici nous n avons pas eu besoin d un raisonnement par contradiction La phase de justification intuitive de l obligation de preuve est peut tre la plus impor tante c est ce moment que l on per oit toutes les cons quences de la mod lisation B choisie Maintenant nous comprenons pourquoi l obligation de preuve doit tre vraie dans le contexte du composant Ce contexte doit se retrouver dans les hypoth ses nous allons donc les examiner 5 4 3 Conseils pour la s lection des hypoth ses Le point le plus important est le suivant lire les hypoth ses en remontant Les hypoth ses les plus significatives pour le but sont g n ralement dans les dix derni res Les hypoth ses de contexte du d but de la liste sont g n ralement des propri t s de constantes n ayant souvent rien voir avec le but D autre part les conseils concernant la lecture d un but
199. t nous demandons au prouveur de commencer la preuve en mode r duit pr Red Le but devient Jee ee C NAT A Vuu uu ee gt uumod3 0 A 9 ee Ce qui revient prouver que 9 est dans NAT et que 9 est divisible par 3 En pr sence de ce type d ind terminisme gratuit il faut changer la sp cification Nous remplacons la sp cification de l op ration par xx xx NAT A xamod3 0 Cette fois ci tout se d montre en force 0 sans intervention manuelle Conclusions Dans le cas o un but existentiel peut se r soudre par une valeur triviale ou une valeur particuli re issue de la sp cification il faut mesurer si l ind terminisme qui produit cet existentiel est bien n cessaire Si c est le cas il faut d montrer l obligation de preuve en utilisant la commande SuggestforExists sinon il faut liminer l ind terminisme inutile LA PHASE DE MISE AU POINT 51 5 7 2 Les buts existentiels abstraits Ce sont les buts existentiels qui apparaissent par des constantes abstraites math matiques Supposons par exemple que vous avez besoin de la notion de factorielle dans une sp cification Vous pouvez d crire cette notion comme une constante abstraite ABSTRACT CONSTANTS fact PROPERTIES fact EN NA Vnn nn EN gt fact nn 1 nn 1 xfact nn A fact 0 1 Comme cette constante ne sera naturellement jamais implant e il faudra prouver qu elle existe L obligation concern e va apparaitre assez tard da
200. t dans la preuve Le syst me de pilotage de la preuve permet les retours en arri re Il est ainsi possible de faire des d monstrations tr s longues chaque nouvelle commande le prouveur poursuit partir de l tat pr c dent sans tout rejouer et en cas d erreur il suffit de faire des retours en arri re Cette conduite de preuve est bas e sur les fonctionnalit s natives du Logic Solver Le syst me gestion de preuve du Logic Solver sous jacent a une influence sur la perfor mance des d placements En particulier les retours en arri re sur des branches de preuves termin es est plus long Par exemple 102 Prouveur interactif Manuel Utilisateur dc xx f el e2 e3 e4 e5 e6 amp pr amp pr amp pr amp pr amp pr amp Next Ceci correspond l arbre de preuve de r r pE pr pr Next Si l op rateur utilise la commande Back ba le syst me doit retrouver le but pr c dent de la preuve par cas lequel a t d charg par la commande pr Le Logic Solver retient tous les buts pr c dents de la branche courante de preuve uniquement Retenir les branches de preuve termin es prendrait beaucoup trop de m moire Donc la seule mani re de retrouver ce but est de remonter jusqu la commande DoCases non comprise puis de se d barrasser des buts interm diaires en refaisant les appels au c ur de preuve Il y a donc 4 appels au coeur de preuve faire on voit le probl me si chaque appel pre
201. t de la phase de preuve tant alors nul L op rateur pourrait n anmoins demander voir une d monstration math matique r dig e de chaque obligation de preuve pour faire certifier le logiciel pro duit mais il ne le ferait s rement pas pour toutes les obligations En r sum l activit de preuve est parfois compl tement automatique Dans notre cas il reste une obligation non d montr e donc soit le composant est juste mais le prouveur n a pas trouv lune des d monstrations soit le composant est faux et l obligation fausse restante localise l erreur Nous sommes bien entendu dans le deuxi me cas puisque notre composant est volontairement faux l obligation fausse restante doit videmment d couler de ce que 1 2 3 n est pas inclu dans 2 3 4 Pourquoi le prouveur n affirme t il pas que cette obligation est clairement fausse En fait il se trouve qu infirmer une obligation de preuve est un probl me th oriquement beaucoup plus difficile que de la d montrer car il faut choisir des valeurs v rifiant les hypoth ses mais pas les conclusions Pour cette raison il n y a actuellement aucun outil automatique qui d tecte les obligations de preuve fausses en particulier le prouveur n est pas pr vu pour cela Il nous faudra donc visualiser cette PO pour s apercevoir qu elle est fausse ce que nous allons faire par la suite Comment la preuve automatique des deux premi res obligations a t elle pu se faire Nous al
202. t devient ens N ee gt 0 lt 3 card ens card ens N ee La preuve de cette nouvelle hypoth se a donc r ussi Grace a elle la preuve principale va peut tre aboutir PRI gt pr Starting Prover Call Le but devient 0 lt card v1 1 N v2 1 card v1 1 v2 1 N v3 1 Ce n est pas suffisant Revenons en arri re pour remplacer pr par pr Red conform ment la m thode g n rale PRI gt ba Le but devient ETUDES DE CAS 141 ens N ee gt 0 lt 3 card ens card ensM ee PRI gt pr Red Starting Prover Call Le but devient 3 lt card ens Ce but est vident puisque card ens taille 1 et que taille 1 3 Le prouveur choue car il ne remplace pas l expression card ens par taille 1 Sans chercher comprendre pourquoi il suffit de le faire menuellement PRI gt eh card ens taille 1 Goal Starting use Equality in Hypothesis Le but devient 3 lt taille 1 Tentons la preuve PRI gt pr Starting Prover Call Le but initial r apparait en vert la preuve est termin e L arbre de preuve est le suivant Force 0 pr Red fh 0 lt 2 card ens card ens ee pr Red ah ens ee pr pr Red eh card ens taille 1 Goal pr Next 142 Prouveur interactif Manuel Utilisateur 8 2 Preuve arithm tique avec divisions L exemple pr sent ici est une preuve concernant les divisions enti res et n cessitant de conna tre l int
203. t souvent meilleur d ajouter cette hypoth se par AddHypothesis Dans la plupart des cas le prouveur devrait r ussir d montrer cette hypoth se qui d rive simplement des hypoth ses courantes il suffit alors de la faire monter par dd ou pr Dans l exemple pr c dent si d aventure l hypoth se xx 3 venait man quer alors que zx 3 est en hypoth se il suffirait d ajouter zx 3 par une commande AddHypothesis L usage sp cifique d une r gle est ainsi vit le temps de recherche de cette r gle est conomis 6 7 5 Probl mes de normalisation parenth ses Il arrive assez souvent que l op rateur d sire faire des transformations qui imposent de passer par des formes l encontre des normalisations du prouveur Il peut alors se produire une sorte de conflit entre l op rateur et le c ur de preuve chacun d faisant au pas suivant ce que l autre a fait Nous allons exposer des solutions pour viter ces conflits Par exemple supposons que l op rateur d sire transformer l hypoth se dom gg xx aa 4 xx gt bb EE On suppose que la simplification des deux surcharges sur le m me l ment n a pas t faite parce que le prouveur n a pas regroup les deux termes de droite L op rateur a trouv la r gle suivante par une commande SearchRule ar b amp a c atc SimplifyRelOveXY 13 Mais il ne peut pas l appliquer car le parenth sage implicite de l hypothese concern e ne l
204. terface Motif du prouveur interactif permet un affichage Multi fen tre de la preuve Nous allons voir comment l utiliser 6 3 1 Organisation de l cran L interface Motif du prouveur interactif est pr vue pour faciliter le travail de l op rateur dans une philosophie multi fen tre c est dire que chaque sujet d attention de l op rateur est repr sent par une fen tre les deux ou trois sujets en traitement tant en juxtaposition l cran et les sujets environnants tant rang s en ic ne sur les bords de l cran La juxta position de deux fen tres d bordant l une sur l autre permet de mettre plus d informations l cran que ce que permet sa taille la fonctionnalit Front Back tant utilis e pour ramener imm diatement en avant la fen tre lue Cette approche Multi fen tre n cessite une installation ad quate du syst me En particu lier les commandes suivantes doivent tre accessibles directement ic nifier ou d sic nifier une fen tre partir d un endroit quelconque de sa surface faire passer une fen tre devant ou derri re partir d un endroit quelconque de sa surface La position normale du prouveur interactif est la suivante hypoth ses cette fen tre est utilis e pour chercher des hypoth ses visuellement ou pour afficher une hypoth se ind pendemment d une recherche faite dans la fen tre de contr le Zone de situation globale s utilise quand on a
205. teur est souvent tent de consid rer les preuves comme des programmes corriger et optimiser tat d esprit qui cause beaucoup de perte de temps 3 1 2 La preuve automatique Lancez le contr le de types et la g n ration d obligations de preuve relatives ce compo sant Ensuite lancez le prouveur automatique en force 0 Atelier B composant de Prove ON Automatic force 0 INTRODUCTION AU PROUVEUR 11 Observez les messages qui s inscrivent dans la fen tre de lancement Les indiquent des preuves r ussies les les preuves chou es A la fin de la session le prouveur imprime l tat final de preuve Proving DemoExample Proof pass 0 still 3 unproved PO clause Initialisation End of Proof Initialisation Proved 2 Unproved 1 TOTAL for DemoExample Proved 2 Unproved 1 Vous venez de lancer le prouveur automatique en force 0 nous expliquerons plus loin ces termes Deux des obligations de preuve parmi les trois g n r es pour ce composant ont t d montr es automatiquement vous n avez plus vous pr occuper de ces obliga tions ni de ce qu elles v rifient Si toutes les obligations de preuve de notre composant taient ainsi automatiquement d montr es il n y aurait rien de plus faire le com posant serait enti rement prouv sans intervention de l op rateur le co
206. thm tiques S il y a peu d hypoth ses pp preuve sur le lemme com plet maximum 60s Si les hypoth ses n cessaires pp rp 1 preuve sur le lemme r duit sont celles qui ont un sym maximum 60s bole commun avec le but Il y a un grand nombre ramener les hypoth ses preuve sur lemme avec hy d hypoth ses mais celles int ressantes dans le but poth ses choisies maximum n cessaires sont peu nom avec la commande ah et 60s breuses utiliser pp rp 0 Comme nous l avons vu depuis le d but de ce chapitre la commande pp s utilise seule ou au milieu d une d monstration utilisant d autres commandes Nous allons pr senter un court exemple de l utilisation de PredicateProver avec des hypoth ses r duites Soit d montrer le lemme suivant EE F Z A BE A cc EE gt card EE U cc card EE 74 Prouveur interactif Manuel Utilisateur Conform ment au grand principe d utilisation du prouveur interactif nous commencons par faire un appel au coeur de preuve en mode r duit puis nous examinons le but restant PRI gt pr Red Starting Prover Call Current PO is Initialisation 2 Unproved saved Unproved Goal card EE 1 1 card EE End Comment se fait il que le prouveur choue sur ce but En fait il s agit d un probl me de parenth sage c est dire que l expression card EE 1 1 est analys e comme l expres sion card EE 1
207. ti re Les r gles de calcul sont beaucoup plus r duites que sur la division r elle Par exemple on n a pas a b c aje b c contre exemple a b 1 c 2 Ou encore on n a pas 0 lt a 2 gt 0 lt a contre exemple avec a 1 confusions de niveaux dans les fonctions de fonctions les fonctions de fonctions donnent souvent des pr dicats plus compliqu s que pr vu Par exemple soit fo INDEX NAT NAT que l on veut raffiner par fi INDEX gt NAT gt NAT L invariant de liaison n est pas fo dom fo lt f mais Vx x INDEX gt fo x dom fo x lt f1 x extensions avec des variables Si les l ments d un ensemble en extension ne sont pas des expressions litt rales il se peut que ces l ments soient gaux entre eux L oubli de ce fait conduit des erreurs par exemple xx yy zz n est pas gal xx yy en particulier si zz yy xx c est l ensemble vide 44 Prouveur interactif Manuel Utilisateur 5 4 5 Notes et essais Au cours des quatre tapes pr c dentes l op rateur imagine des simplifications sur les expressions qu il examine et des d buts de d monstrations interactives Avant de quitter une obligation de preuve il est donc conseill de Remettre en cause la forme des expressions en particulier lancer une fois le prouveur en force 0 pour voir quel est le premier but en chec Cela aide trouver des expressions sim
208. tif Manuel Utilisateur Next Saved line pos 1 New Goal Force 0 amp dd Hypothesis since last command Local hypotheses amp ntt TACHES amp not ntt taches amp tt 0 taches ntt amp Check that the invariant tt tt taches not tt ntt amp not ntt dom tport amp not ntt dom tident amp not ntt tt amp pass tident lt ntt gt tident tt tt 0 ran pass amp pass tident lt ntt gt tident tt tt 0 PASSWORDS amp 0 lt 0 amp O NATURAL amp O INTEGER tt TACHES amp tt dom tport amp tt dom tident amp tident tt ran tident amp tident tt IDENTITES amp tident tt dom pass amp tident taches lt gt IDENTITES amp pass IDENTITES lt gt PASSWORDS amp tconnait tt lt ran tconnait amp tconnait tt lt PASSWORDS amp dom tident lt taches amp ran tident lt IDENTITES amp dom pass lt IDENTITES amp ran pass lt PASSWORDS amp pass tident tt lt ran tconnait amp pass tident tt lt PASSWORDS amp dom tident lt TACHES amp ntt gt tident tt TACHES dom pass amp ntt gt tident tt TACHES IDENTITES amp ntt gt tident tt TACHES ran tident pass tident tt ran pass amp pass tident tt PASSWORDS amp ntt tt 0 amp not tt tt 0 not tt 0 tt amp tconnait tt 0 lt ran tconnait amp tconnait tt 0 lt PASSWORDS
209. tions prouv es Cette manipulation doit galement tre faite pour contr ler la preuve d un projet lors de sa r ception Attention ce peut tre tr s long le rejeu complet de quelques milliers d obligations de preuve pouvant n cessiter beaucoup de temps machine 6 6 2 L usage d une r gle d admission Une r gle d admission est une r gle manuelle qui permet de prouver n importe quoi Il suffit dans le fichier des r gles manuelles lt composant gt pmm d ajouter THEORY Admis IS bcall WRITE bwritef A gt p END Le cons quent de cette r gle est le joker p qui co ncide avec n importe quel but Une telle r gle est videmment fausse A la fin de toutes les phases de preuve il faut la retirer et rejouer les d monstrations pour s assurer qu aucune d entre elles ne l utilise plus voir paragraphe 100 Prouveur interactif Manuel Utilisateur L ant c dent bcal1 est une directive de langage de th orie qui permet d crire A comme admis juste avant le qui signale le succ s en preuve automatique ce qui permet de trahir l utilisation de ces r gles lors d un rejeu de preuve On peut aussi crire sur le terminal le but qui a t admis bcall WRITE bwritef admis n p gt p L usage d une regle d admission est vivement recommand pour conduire effica cement la preuve La r gle d admission s emploie par ApplyRule ar Admis 1 On
210. tique sur implantation CON Q Ot S il reste des obligations de preuve non d montr es controler qu elles soient justes Si certaines sont fausses l implantation n est pas correcte il faut la corriger 9 Faire la d monstration formelle des obligations de preuve restantes dans la machine abstraite et dans l implantation l aide du prouveur interactif Dans le processus de d veloppement ci dessus les tapes 3 4 7 8 et 9 sont les tapes de preuve Nous voyons que la preuve formelle complete est faite la fin il faut viter les d monstrations longues tant que les composants risquent de devoir tre modifi s C est pourquoi il y a deux phases bien distinctes dans l activit de preuve en B la mise au point des composants par v rification des obligations de preuve et la preuve formelle finale Cette distinction se retrouve toujours quelle que soit la m thode de d veloppement utilis e Notons que dans les tapes 3 et 7 il faut utiliser le prouveur automatique configur pour 23 24 Prouveur interactif Manuel Utilisateur tre assez rapide force 0 voir paragraphe suivant car nous devrons attendre qu il termine pour passer a l tape suivante Savoir si on se place en phase de mise au point ou en phase de preuve finale est essentiel Cette m thode par phase peut se repr senter par le sch ma suivant MISE AU POINT ch modifier pour que les PO non automatiquement d mo
211. tradiction si le but est de la forme not p et particuli rement s il est de la forme not a b Autres commandes Enfin les commandes suivantes sont plus rarement employ es ParticularizeHypothesis ph pour une hypoth se de la forme Vx P x Q x l op rateur peut proposer une liste de valeurs xo il devra alors prouver le sous but P x0 pour que l hypoth se Q xo apparaisse Penser ParticularizeHypothesis si le c ur de preuve n arrive pas instancier lui m me une hypoth se Vx P x gt Q x En particulier si P xo n est pas directement en hypoth se le prouver comme un sous but permet d utiliser toutes les fonctionnalit s du prouveur pour le faire appara tre ModusponensonHypothesis mh permet de g n rer Q si P gt Q et P sont en hypoth ses Le c ur de preuve le fait syst matiquement sauf pour des hypoth ses d j d riv es voir paragraphe 6 7 2 showLitteralPo lp cette commande permet d afficher une obligation de preuve telle qu elle est d finie dans les fichiers du composant sans m me avoir charger la PO concern e Ceci est parfois utile pour retrouver plus facilement le lien entre une obligation de preuve et le source du composant GlobalSituation gs cette commande retourne la liste des obligations de preuve avec leur tat et leur but Avec l interface Motif l op rateur ne devrait jamais avoir l utiliser elle n est utile qu en mode batch voir p
212. u add_project_user arc archive crp create_project epr edit_project_res glfa get_list_from_archive ip infos_project op open_project rdd remove_definitions_directory rp remove_project rpl remove_project_lib rpu remove_project_user res restore sdd1 show_definitions_directory_list s11 show_libs_list sp11 show_project_libs_list sprl show_project_readers_list spul show_project_users_list spl show_projects_list Machine level commands available after open_project aa ada_all a adatrans af add_file ani animator bOc bOcheck b browse c a c all c t c trans LA PHASE DE PREUVE FORMELLE 89 cc ccompile clp cdf create_doc_framemaker cdi cdr create_doc_rtf ct dg dep_graph Ce 1ce edit_clc ep fg formula_graph gpx hiaa hia_all hia hg homonymy_graph ic 1cm lchecker_mach cp m make_all nav ocg op_call_graph pov po pogenerate ppf ppi pov_print_ileaf ppl ppr pov_print_rtf psf psi pov_show_ileaf psl psr pov_show_rtf ppfi pdi print_doc_ileaf pal pchk project_check ps pr prove ppp ppmm prove_pmm r rc remove_component sn spp set_print_params sdl sml show_machines_list svf s status sg t typecheck Cu bbatch 7 gt clp bbatch 8 gt q End of interpretation 8 lines PRVB 6 4 La ligne de commandes clo
213. ur les va riables qui interviennent dans le but Ne pas chercher contr ler si l obligation de preuve est vraie par hypoth ses contradictoire en cherchant le contre exemple c est trop compliqu obligations de preuve d pourvues de sens il est parfaitement possible qu une obligation de preuve soit d pourvue de sens De telles obligations signalent bien une erreur dans le composant mais elles peuvent surprendre en particulier parce qu il n y a pas clairement un contre exemple Par exemple uu EN A uu lt 10 gt uu 2 eN Un contre exemple est uu 2 TRUE et uu 0 La recherche de ce type de contre exemple peut tre d routante En particulier le contre exemple pr c dent ne serait pas accept par I Atelier B cause d un probl me de typage il est n anmoins math matiquement valide Ceci est bien une obligation de preuve trahissant une erreur dans le composant qu il faut absolument modifier avant de poursuivre Dans le cas d obligations de preuve fausses par absence d information sur une variable penser a un invariant de boucle trop faible Rappelons que dans un invariant de boucle il faut au moins typer toutes les variables utilis es dans le corps de la boucle un invariant de liaison manquant entre une variable abstraite et la ou les variables import es qui la r alisent 54 Prouveur interactif Manuel Utilisateur Les obligations de preuve apparemment d pourvues de sens peuvent
214. uve en 2 cat gories commandes de haut niveau pp pr mp qui correspondent l ex cution d un grand nombre de r gles et de m canismes Ce sont des commandes r solutoires c est dire que leur application est n cessaire pour d montrer n importe quel but m me btrue commandes de bas niveau dd ah ar ce sont des commandes qui s ex cutent en pas a pas Il n y a pas de r solution Leur combinaison permet d orienter la preuve QUESTIONS FREQUEMMENT POSEES 159 Contrairement aux commandes de la cat gorie ci dessus ces commandes n cessitent une bonne connaissance exp rience du prouveur interactif 9 5 Utilisation de SearchRule La commande SearchRule peut tre utilis e dans 2 situations diff rentes lorsque le prouveur automatique ne parvient pas d montrer le but courant La re cherche des r gles pouvant s appliquer permet de d terminer quelle est la meilleure can didate et pour quelle raison cette r gle ne s applique pas Par exemple une hypoth se peut manquer Il suffit dans ce cas d ajouter cette hypoth se afin que cette r gle puisse s appliquer Il faut bien avoir l esprit que la commande SearchRule affiche toutes les r gles suscep tibles de s appliquer et non pas celles qui s appliquent lors de l ajout de r gles manuelles La commande SearchRule permet alors de v rifier que la r gle qui est charg e en m moire correspond bien la r g
215. uve les hypoth ses cor respondantes ces raisons voir paragraphe 5 4 3 4 d monstration intuitive faire une d monstration intuitive de l obligation de preuve r duite ces hypoth ses voir paragraphe 5 4 4 5 notes et essais la d monstration intuitive faite peut donner des id es pour la d monstration formelle sur les causes de l chec de la d monstration automatique etc Dans cette derni re tape on cherche profiter de ces id es ventuellement une d monstration formelle rapide sera recherch e et g n ralis e d autres obligations permettant ainsi de r duire le nombre d obligations lire voir paragraphe B 4 5 Cette liste d crit la m thode pr conis e pour la phase de mise au point Nous conseillons de suivre ces tapes pour chaque obligation de preuve en s aidant des paragraphes cor respondants L id e ma tresse de cette m thode en cinq tapes consiste interpr ter obligation de preuve dans le contexte du composant prouver On b n ficie ainsi de toute la d marche intellectuelle qui a t faite pour comprendre ou construire le composant et qui deviendra terme un ensemble de d monstrations rigoureuses Cette m thode n cessite la lecture du composant prouver ainsi que celle des composants r f renc s Nous conseillons donc de garder en fen tres ic nifi es le fichier compo sant concern et les composants associ s Pour une machine abstraite ce sont les ma
216. uve sont des tapes d licates Lors de ces changements attention aux pi ges suivants METHODE GENERALE 25 S assurer que les composants ont bien leur forme d finitive avant la phase de preuve formelle Il est en effet courant d crire les composants dans une version r duite ou incompl te pour une mise au point rapide en pr voyant une tape de finition Cette finition doit tre faite avant la preuve formelle En phase de preuve formelle s assurer que toutes les obligations de preuve peuvent tre pr sum es justes En effet si une obligation de preuve fausse est d couverte durant la phase de preuve formelle l op rateur est tent de poursuivre cette phase apr s avoir modifi un composant alors qu il est imp ratif de refaire une phase de mise au point 4 2 T utilisation des forces du prouveur L op rateur ne s attend jamais ce qu un ordinateur concoive et r alise les programmes sa place parce que l ordinateur ne peut pas deviner ce qu il faut obtenir Dans le domaine de la preuve au contraire ce qu il faut obtenir est clair nous voulons des d monstrations des nonc s prouver a partir d un ensemble de r gles connues Il n existe malheureusement pas d algorithme qui produise la d monstration de tout nonc correct les d monstrateurs automatiques et en particulier celui de l Atelier B appliquent donc un ensemble de tactiques plus ou moins heuristiques qui peuvent chouer ou aboutir Si
217. uveur et son interface apparaissent dans cette zone de commandes en ligne Nous allons examiner de plus pr s cette notion essentielle dans le paragraphe suivant 3 Le t moin de preuve il porte la mention Proved quand la d monstration courante aboutit 4 Le titre barreau de la fen tre pr cise le nom du composant le nom de l op ration dont est issue l obligation de preuve et le num ro de cette derni re 3 1 6 Echanges avec le prouveur interactif L outil de preuve interactive est form de deux parties le prouveur interactif propre ment dit et son interface homme machine Le prouveur effectue les commandes commandes de preuve ou d information L interface homme machine vous affiche les r sultats et transmet vos commandes au prouveur Tout le dialogue avec le prouveur se ram ne des interactions de type commande vers l outil r ponse de lPoutil Cette interaction en mode ligne est enti rement visible dans la zone des commandes en ligne Par exemple si vous appuyez sur le bouton Next de la fen tre de situation globale l interface met une commande ne qui veut dire Next vers le prouveur de la m me mani re que si vous aviez tap ne dans la zone de commandes en ligne Le prouveur effectue alors la commande puis renvoie l tat courant sous la forme de lignes de texte que l interface r partit dans ses fen tres tout en laissant une trace de la r ponse visible dans la zone des commandes en ligne L interf
218. ve ne peut tre vraie que par hypoth ses contradictoires Le prouveur choue parcequ il ne sait pas isoler l hypoth se contradictoire nous allons voir comment la lui indiquer Previous components invariants A ens lt NAT A card ens lt 3 A Component invariant A vI 1EN A v1 1 lt 2147483647 A v281 EN A v2 1 lt 2147483647 A v3 1 EN A v3 1 lt 2147483647 A taille 1 EN A taille 1 lt 2147483647 A taille 1 card ens A taille 1l 0 gt ens A taille 1 1 gt ens v1 1 A taille 1 2 ens v1 1 v2 1 A taille 1 3 gt ens v1 1 v2 1 v3 1 A btrue A enter preconditions in previous components A ee En A ee lt 2147483647 A 111 1 enter 30 A enter preconditions in this component A Local hypotheses A taille 1 0 A taille 1 1 A taille 1 2 A v1 1 ee A v2 1 ee A v3 1 ee A taille 1 3 A card ens U ee lt 3 A Check that the invariant ov 1 ov is preserved by the operation ref 8 gt bfalse a Comme taille 1 3 nous savons que ens v1 1 v2 1 v3 1 D autre part taille 1 card ens donc les trois vi 1 sont diff rents Or ee est diff rent de chaque vi 1 donc card ensU ee 4 C est donc l hypoth se card ensU ee lt 3 qui est contradictoire Le but initial qui apparait dans le prouveur interactif contient les hypoth ses locales Local hypotheses A taille 1 0 A
219. vironnement 6 3 2 Le prouveur interactif en mode batch Comme tous les outils composant l Atelier B le prouveur interactif est accessible en mode Batch Rappelons que le mode Batch se lance par la commande lanceBB au lieu de lanceAB Le prouveur automatique s acc de alors par la commande pr composant force et le prouveur interactif par br Le mode Batch est d crit dans le manuel utilisateur de lV Atelier B Apr s le lancement du prouveur interactif en mode batch commande br la preuve se d roule exactement comme depuis la fen tre de commandes de l interface Motif mais les hypoth ses et la ligne de commande sont uniquement dans les messages r ponse du prouveur Les difficult s d utilisation du mode Batch par rapport l interface Motif sont LA PHASE DE PREUVE FORMELLE 79 Comme il n y a pas de fen tre de situation globale il faut utiliser la commande Global Situation gs pour obtenir la liste des obligations de preuve Les informations longues comme la liste des hypoth ses d filent dans la fen tre de com mande au lieu d tre affich es dans des fen tres s par es Concernant les hypoth ses notons toutefois que lorsqu il n y a que des hypoth ses en plus le prouveur ne renvoie pas la liste complete mais seulement les nouvelles hypoth ses Le bouton d interruption n est pas disponible en mode Batch Par contre l utilisation du mode Batch permet d employer un ter
220. xx e1 amp Next Dans cet exemple l op rateur aurait pu taper cing fois ba ou faire ba 5 pour obtenir le m me r sultat Ce serait une tr s mauvaise m thode beaucoup plus longue 6 6 4 Le choix d une force sup rieure Le choix d une force sup rieure pour faire une tentative de preuve en fonction de la forme d une PO est toujours tres sp culatif En effet il n est pas question de pr voir exacte ment ce que va faire le coeur de preuve dans telle ou telle force il faudrait pour cela connaitre toutes les r gles et tous les m canismes De telles tentatives sont donc guid es par l intuition et l exp rience Les forces sup rieures sont les forces 1 2 et 3 Chacune contient tout les m canismes de la force pr c dente ce qui n est pas le cas de la force O dont les m canismes ne sont pas syst matiquement dans la force 1 Les forces sup rieures ont galement des constantes de dimensionnement croissantes la force 2 a le droit de cr er plus de sous cas que la force 1 de d river plus d hypoth ses etc Pour se guider dans le choix d une force sup rieure il est raisonnable de ne retenir que les sp cificit s de chaque force Celles ci sont Force 1 les hypoth ses sont trait es par passage dans le prouveur Elle sont donc plus d compos es qu en force 0 par exemple toute hypoth se de la forme x a b sera syst matiquement transform e en a lt x et x lt b Force 2 des hypoth se
221. z lt 10 Nous supposons que les m canismes du coeur de preuve ne suffisent pas d montrer ceci Pour d montrer ce lemme il faut faire trois cas suivant que le maximum est rx yy ou zz L op rateur peut d clencher un premier cas par une commande DoCases dc max xzx yy 22 xx La preuve se poursuit alors pour max x2 yy zz xx puis pour max xx yy zz xx Il est possible que ces deux cas soient directement d montr s par les m canismes du coeur de preuve c est ce que nous supposerons dans ce cas la preuve aboutit une action op rateur d clenchant une preuve par cas a suffi pour permettre la d monstration Le but de cet exemple est de faire comprendre comment une interaction dans une preuve peut faire aboutir celle ci par les m canismes du coeur de preuve sans que vous n ayez introduit la moindre connaissance math matique non valid e En fait vous pilotez la preuve en ajoutant votre intuition puis en relancant le prouveur jusqu au nouvel chec ou jusqu au succ s d apr s une expression tr s imag e de F Mejia l op rateur joue au billard avec les m canismes du prouveur Il est clair qu une bonne intuition de ce que les m canismes vont faire est utile pour ce style de preuve interactive Par exemple soit prouver zx EN A yyEN A yy lt 10 A rz 1 8 lt yy gt zx 1 8 lt 10 Les m canismes du c ur de preuve peuvent chouer sur un tel lemme car ils cherchent

Download Pdf Manuals

image

Related Search

Related Contents

SRW01 - Manual del Usuario  Descargar  Manuel d`utilisation de ANGE 1D  GA-945P-DS3/S3  3181 ECLIPSE Digital Bath Scale OPERATING INSTRUCTIONS  - RM Support    Winner4 OSD Manual - 2 Geek Tech Support Services  

Copyright © All rights reserved.
Failed to retrieve file