Class PreuveAB_tmp

java.lang.Object
  ConfigurationGeneSyst
      MethodesNonFonctionnelles
          PreuveAB_tmp

public class PreuveAB_tmp
extends MethodesNonFonctionnelles

Field Summary

interfacageAB	AB Interface permettant d'interagir avec l'atelier B
private java.lang.String	ClausesNonTraitees
private java.lang.String	ClausesNonTraiteesSaufVarEtInv
private java.lang.String	ExtensionComposantTraite
private int	Force
private java.lang.String	NatureComposantTraite
private java.lang.String	NomDossierCalcul
private java.lang.String	NomDuProjet
private java.lang.String	NomFichierTraite
java.lang.String	NomMachineProduite
private boolean	QueGenererOp

Fields inherited from class MethodesNonFonctionnelles

AffichageMinimum, CstImplementation, CstMachine, CstRefinement, Debugage, NbPreuvesAvantRedemarrage, NbPreuvesFaitesDepuisDemarrage, NbPreuvesFaitesParBoB, NbPreuvesFaitesParTactiques, Nettoyer, parallele, Path, QueGenererOP, SymboleDefaut, SymboleNonPr, SymboleProuve, TabClauseNature, TabExtensions, TactiquesInteractives, TempAttenteAuRedemarrage, terminal, VerifierOracle

Fields inherited from class ConfigurationGeneSyst

AdresseDossierBDB, AppelAtelierB, Cst_FaireExistentielle, FormatDot, FormatGxl, FormatHtml, NbFormatsSortie, NomDossierDeBase, NomDossierResultat, NomFichierHtml, NomFichierTraces, NomProjetDeBase, PathDot, TabFormatsSortie, TabFormatsSortiePossibles, TactiquesUtilisateur

Constructor Summary

PreuveAB_tmp(java.lang.String DossierCalc, java.lang.String FichierTraces, java.lang.String NomProjet, java.lang.String NomDossierBDP, java.lang.String NomDossierLANG, int F, boolean QGOP)
Constructeur de cette classe, il permet de configurer un certain nombre de variables indispensables à son bon fonctionnement.

Method Summary

void	AjouteMachinePourDependances(java.lang.String NomFichierAvecExtension) Cette méthode recopie (sans la clause opérations) la machine spécifiée par NomFichierAvecExtension dans le dossier de travail courant et l'intègre dans le projet B en cours.
void	CopieMachineDansDossierTravail(java.lang.String NomFichierAvecExtension) Cette méthode permet de recopier une machine, un raffinement ou une implantation B dans le dossier de travail courant.
private java.lang.String	CreationDeFichierB(int NumOp, int NumEtat1, int NumEtat2, int TypeOP, bob.predicat.TPredicat AssertionPerso) CreationDeFichierB créé un fichier B de nom NomFichier dans le dossier NomDossier en y inscrivant toutes les clauses mises de coté précédemment, ainsi que l'assertion Assertion & AssertionPerso.
boolean	EffaceFichierTrace() Efface, le cas échéant le fichier de trace créé lors l'utilisation de l'atelier B en parallèle.
void	FinUtilisation() Cette méthode permet de clore les différents fichiers ouverts et les processus lancés.
void	InitClausesNonTraitee(java.util.Vector<bob.composant.TClause> LCVI, java.util.Vector<bob.composant.TClause> LCNT) Permet de configurer la valeur des variables ClausesNonTraitees et ClausesNonTraiteesSaufVarEtInv qui sont des chaines de caractères représentant l'ensemble des clauses Non traitées du composant B courant.
void	InitComposantTraite(bob.composant.TComposant composantB) Permet de mettre à jour les valeurs du nom du composant B traité son Type
void	InitQueGenererOp(boolean QGO) Permet de mettre à jour la valeur de la variable QueGenererOp
private boolean	ProuveMachine(java.lang.String NomFichier) Prouve une machine se trouvant dans un fichier donné à l'aide de l'atelier B.
boolean	ProuvePredicat(int NumOp, int NumEtat1, int NumEtat2, int TypeOP, bob.predicat.TPredicat AssertionPerso) Methode permettant d'effectuer la preuve d'une OP.
void	Reset() Dans le cas où l'atelier B est en parallèle, cette méthode permet de relancer le processus.

Methods inherited from class MethodesNonFonctionnelles

AfficheStatistiques, AfficheTabInt, AfficheTabInt, AppelCommandeExterne, AppelCommandeExterneAvecScript, Conjonction, Disjonction, DonneExtension, Donner_Extension, EnleveExtension, FusionneTabOfInt, GestionNomDeProjet, IntNonPresent, inverseVecteur, LanceScriptExterne, NouveauNomDeFichier, RechercheElement, replaceAll, replaceAll, SansChemin, SysAfficher

Methods inherited from class ConfigurationGeneSyst

initTactiquesInteractives

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

AB

public interfacageAB AB

Interface permettant d'interagir avec l'atelier B

NomDuProjet

private java.lang.String NomDuProjet

NomDossierCalcul

private java.lang.String NomDossierCalcul

Force

private int Force

QueGenererOp

private boolean QueGenererOp

ClausesNonTraitees

private java.lang.String ClausesNonTraitees

ClausesNonTraiteesSaufVarEtInv

private java.lang.String ClausesNonTraiteesSaufVarEtInv

NomFichierTraite

private java.lang.String NomFichierTraite

NatureComposantTraite

private java.lang.String NatureComposantTraite

ExtensionComposantTraite

private java.lang.String ExtensionComposantTraite

NomMachineProduite

public java.lang.String NomMachineProduite

Constructor Detail

PreuveAB_tmp

public PreuveAB_tmp(java.lang.String DossierCalc,
                    java.lang.String FichierTraces,
                    java.lang.String NomProjet,
                    java.lang.String NomDossierBDP,
                    java.lang.String NomDossierLANG,
                    int F,
                    boolean QGOP)
             throws ErreurException

Constructeur de cette classe, il permet de configurer un certain nombre de variables indispensables à son bon fonctionnement.

Parameters:

DossierCalc - Nom du dossier temporaire de calcul. Celui-ci doit déjà avoir été créé.

FichierTraces -

NomProjet -

NomDossierBDP -

NomDossierLANG -

F - Force de la preuve (0..3)

QGOP - si vrai alors on ne fait que générer les obligation de preuve, sans les prouver.

Throws:

ErreurException

Method Detail

InitClausesNonTraitee

public void InitClausesNonTraitee(java.util.Vector<bob.composant.TClause> LCVI,
                                  java.util.Vector<bob.composant.TClause> LCNT)

Permet de configurer la valeur des variables ClausesNonTraitees et ClausesNonTraiteesSaufVarEtInv qui sont des chaines de caractères représentant l'ensemble des clauses Non traitées du composant B courant. Ces clauses seront remises telles quelles dans les composants générer pour vérifier les obligations de preuve.

Il est nécessaire de conserver 2 ensembles différents, car dans le cas du calcul de l'existence d'une transition, alors les variables abstraites son sous quantificateur existenciel.

Optimisation du 16/4/7 : Les variables sont changée en constantes pour ne pas perdre de temps de preuve avec l'initialisation.

Parameters:

LCVI - Vecteur de TClauses contenant les clauses variables, invariant et initialisation.

LCNT - Vecteur de TClauses contenant la liste des clauses non traitées (Toutes sauf opération, Assertion, variables, invariant et initialisation).

InitComposantTraite

public void InitComposantTraite(bob.composant.TComposant composantB)

Permet de mettre à jour les valeurs du nom du composant B traité son Type

Parameters:

composantB - Composant B que l'on veut traiter.

InitQueGenererOp

public void InitQueGenererOp(boolean QGO)

Permet de mettre à jour la valeur de la variable QueGenererOp

Parameters:

QGO - Valeur à donner à QueGenererOp

Reset

public void Reset()

Dans le cas où l'atelier B est en parallèle, cette méthode permet de relancer le processus. Dans le cas contraire, rien ne se passe.

CopieMachineDansDossierTravail

public void CopieMachineDansDossierTravail(java.lang.String NomFichierAvecExtension)

Cette méthode permet de recopier une machine, un raffinement ou une implantation B dans le dossier de travail courant. Pour ce faire, cette méthode parse intégralement le composant, le charge en mémoire, puis le réécrit.

Optimisation du 16/4/7 : Les variables sont changée en constantes pour ne pas perdre de temps de preuve avec l'initialisation.

Parameters:

NomFichierAvecExtension - Nom (avec son extension et son éventuel chemin d'accès) du fichier à recopier.

AjouteMachinePourDependances

public void AjouteMachinePourDependances(java.lang.String NomFichierAvecExtension)
                                  throws ErreurException

Cette méthode recopie (sans la clause opérations) la machine spécifiée par NomFichierAvecExtension dans le dossier de travail courant et l'intègre dans le projet B en cours. Cette méthode sert principalement dans le cas où l'on s'intéresse à un raffinement et que l'on a besoin d'avoir la machine présente dans le projet courant.

Parameters:

NomFichierAvecExtension - Nom (avec son extension et son éventuel chemin d'accès) du fichier à recopier.

Throws:

ErreurException

FinUtilisation

public void FinUtilisation()
                    throws ErreurException

Cette méthode permet de clore les différents fichiers ouverts et les processus lancés.

Throws:

ErreurException

EffaceFichierTrace

public boolean EffaceFichierTrace()

Efface, le cas échéant le fichier de trace créé lors l'utilisation de l'atelier B en parallèle. Sinon, rien ne se passe.

Returns:

Renvoie true ssi tout c'est passé sans erreur.

ProuvePredicat

public boolean ProuvePredicat(int NumOp,
                              int NumEtat1,
                              int NumEtat2,
                              int TypeOP,
                              bob.predicat.TPredicat AssertionPerso)
                       throws java.io.FileNotFoundException,
                              java.io.IOException,
                              ErreurException

Methode permettant d'effectuer la preuve d'une OP. Cette méthode commence par essayer de simplifier l'OP avec la BoB avant d'appeler un prouveur.

Parameters:

NumOP - Numéro de l'opération (Sert à calculer le commentaire et le nom du fichier de SVG)

NumEtat1 - Numéro de l'état de départ (Sert à calculer le commentaire et le nom du fichier de SVG)

NumEtat2 - Numéro de l'état d'arrivée (Sert à calculer le commentaire et le nom du fichier de SVG)

TypeOP - Type d'obligation de preuve générée (Sert à calculer le commentaire et le nom du fichier de SVG)

AssertionPerso - Prédicat à prouver

Throws:

java.io.FileNotFoundException

java.io.IOException

ErreurException

CreationDeFichierB

private java.lang.String CreationDeFichierB(int NumOp,
                                            int NumEtat1,
                                            int NumEtat2,
                                            int TypeOP,
                                            bob.predicat.TPredicat AssertionPerso)
                                     throws java.io.FileNotFoundException,
                                            java.io.IOException

CreationDeFichierB créé un fichier B de nom NomFichier dans le dossier NomDossier en y inscrivant toutes les clauses mises de coté précédemment, ainsi que l'assertion Assertion & AssertionPerso. Les numéros d'opération et de découpage de l'assertion ne sont là que pour la génération du commentaire.

Parameters:

NumOp - Numéro de l'opération motivant l'obligation de preuve

NumEtat1 - Numéro de l'état de départ

NumEtat2 - Numéro de l'état d'arrivée // * @param OPDefaut Information pour les commentaires produits et le choix du nom de fichier. Vrai ssi on cherche à prouver la nom propriété

TypeOP - Donne le type d'OP contenu dans le fichier.

AssertionPerso - Assertion à prouver

Returns:

le nom du fichier de sauvegarde produit.

Throws:

java.io.FileNotFoundException

java.io.IOException

ProuveMachine

private boolean ProuveMachine(java.lang.String NomFichier)
                       throws java.io.IOException,
                              ErreurException

Prouve une machine se trouvant dans un fichier donné à l'aide de l'atelier B. Le résultat est un booléen indiquant le résultat de la preuve

Parameters:

NomFichier - Nom du fichier à créer

Returns:

boolean Vrai si et seulement si le taux de preuve de la machine est de 100%.

Throws:

java.io.IOException

ErreurException