Validation Formelle

Description

• cours - matière potentielle : precedent

Problematique Logique de Hoare Specification Formelle JML un BISL pour Java Validation Formelle Validation Formelle

• bisl pour java langage
• correction partielle
• problematique logique de hoare specification
• formelle jml
• ins
• bisl pour java validation par annotations assertions dans le code
• validation formelle

Sujets

• Precedent
• Validation
• Annotation
• Logique
• Correction

Informations

• Publié par: ubbu0
• Nombre de lectures: 134
• Langue: Français

Extrait

Problematique
Logique de Hoare
Speci cation Formelle
JML un BISL pour Java
Validation Formelle
Validation FormelleProblematique
Logique de Hoare
Speci cation Formelle
JML un BISL pour Java
Plan de l’expose
1 Problematique
2 Logique de Hoare
Langage
Correction partielle et totale
Axiomes
Exemple
Resultats
3 Speci cation Formelle
Langage de speci cation
Design by Contract: Principe
4 JML un BISL pour Java
Les bases
E ets de bords
Constructions Avancees
Validation FormelleProblematique
Logique de Hoare
Speci cation Formelle
JML un BISL pour Java
I have a dream
Mon programme est correct
I have another dream
La preuve de correction est automatique
Necessite de formaliser:
speci cations
semantique du langage
calcul de correction
Validation FormelleProblematique
Logique de Hoare
Speci cation Formelle
JML un BISL pour Java
Speci cation formelle (voir cours precedent):
Decrire formellement le comportement
Veri er que l’execution est conforme
De maniere dynamique a l’execution du programme
De maniere statique par examen du code
Validation FormelleProblematique
Logique de Hoare
Speci cation Formelle
JML un BISL pour Java
Validation
Approchee
Typage: un programme bien type ne declenche pas d’erreur
Typage fort, systeme de type coherent,
Analyse statique: veri cation d’un modele abstrait, veri cation
de certaines proprietes, analyse correcte mais incomplete.
Exacte
Derivation du programme a partir de speci cations formelles
(CoQ, B,. . . )
Veri cation a posteriori du programme dans une logique
adaptee (Hoare,. . . )
Validation FormelleProblematique
Logique de Hoare
Speci cation Formelle
JML un BISL pour Java
Validation par annotations
Assertions dans le code (formalisme logique adapte au langage
C, Java,. . . )
Evaluation des annotations a l’execution (JMLRAC, . . . ) ou
statique (ESC/Java2,. . . )
Principe de developpement (Design by Contract)
Validation FormelleProblematique
Logique de Hoare
Speci cation Formelle
JML un BISL pour Java
Di cultes:
Problemes di ciles (indecidable!)
Passage a l’echelle
Formation des developpeurs
Resultats:
Theoriques: pointeurs, memoire, SD evoluees
Pratiques: langages, prouveurs generiques, dedies
Validation FormelleLangage
Problematique
Correction partielle et totale
Logique de Hoare
Axiomes
Speci cation Formelle
Exemple
JML un BISL pour Java
Resultats
Plan de l’expose
1 Problematique
2 Logique de Hoare
Langage
Correction partielle et totale
Axiomes
Exemple
Resultats
3 Speci cation Formelle
Langage de speci cation
Design by Contract: Principe
4 JML un BISL pour Java
Les bases
E ets de bords
Constructions Avancees
Validation FormelleLangage
Problematique
Correction partielle et totale
Logique de Hoare
Axiomes
Speci cation Formelle
Exemple
JML un BISL pour Java
Resultats
Objectif: une logique de preuve de programme
Validation FormelleLangage
Problematique
Correction partielle et totale
Logique de Hoare
Axiomes
Speci cation Formelle
Exemple
JML un BISL pour Java
Resultats
Un petit langage imperatif
Exp ::= nj e op e op2 OP =f+; ;;=g; n2 Z
Cond ::= Tj Fj e comp e
j C^ Cj C_ Cj:C comp2f==;>;<g
Ins ::= x=e; (a ectation)
j if C then Ins (conditionnelle simple)
j if C then Ins else Ins (conditionnelle)
j Ins Ins (sequence)
j while C do Ins (iteration)
Programme = element genere par Ins
Validation Formelle