[PDF] Preuves Interactives et Applications

View - Download Preuves Interactives et Applications

Previous PDF

Next PDF

Preuves Interactives et Applications

Christine Paulin & Burkhart Wolff

Université Paris-Saclay

Master Informatique FIIL, 2016-17

C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 1 / 47

Introduction 14 Sept. 2015

1Introduction

2Contexte

3Rappels sur la logique

4Lambda-calcul simplement typé

5Démonstration Coq et Isabelle

6Exercices

C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 2 / 47

Objectifs du cours

Comprendre et savoir utiliser desassistants de preuves interactivesLangagede descr iptiond"objets mathématiques et de propr iétés

Environnement

pour constr uireinter activementdes preuv esde propr iétés

facilité denotationbibliothèquesréutilisablesdes procédures de preuvesautomatiquesdes outils (tactiques) de décomposition de preuve (analyse par cas, récurrence)un noyau de vérificationsûrDécouvrir deux systèmes importants

Isabelle/HOL:https://isabelle.in.tum.de/Coq:http://coq.inria.frC. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 3 / 47

Déroulement du cours

séances de cours/TD/TP projet à réaliser page Web du cours C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 4 / 47

Plan du cours

1(CP) Introduction, motivations, lambda-calcul simplement typé.

2(BW) Logique d"ordre supérieur, représentation des termes et des

formules en Coq et Isabelle/HOL, preuves élémentaires.3(CP) Définitions inductives de types de données et de relations,

définitions récursives et preuves par récurrence, représentation en Coq et Isabelle/HOL.4(BW) Exemple de modélisation en Isabelle/HOL.

5(CP) Exemple de modélisation en Coq.

6(BW) Techniques de démonstration automatique, cas de la rééecriture

(système de réécriture, unification, confluence et terminaison), mise en oeuvre dans les assistants de preuve.7(CP & BW) Applications avancées. C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 5 / 47

Cours 1

1Introduction

2Contexte

3Rappels sur la logique

4Lambda-calcul simplement typé

5Démonstration Coq et Isabelle

6Exercices

C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 6 / 47

Démarche

Objectif : contrôler le comportement des

systèmes informatiquesUtiliser des outilsmathématiques modélisation (abstraction) machine, programme, environnement, comportement attendu méthodes de construction de programmes validation simulation preuves de correction Outils informatiques pour faciliter les traitements mathématiquesvalider les modèles et les méthodes construire des preuves complexes C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 7 / 47

Ordinateur, calcul et preuve

Les ordinateurs effectuent des calculs sur des objets binaires. Les mathématiques définissent des notions et établissent la vér ité

d"énoncés via du calcul et des preuves.Peut-on représenter une notion mathématique comme un objet binaire?

Peut-on calculer si un énoncé est vrai?

Peut-on vérifier qu"une preuve est correcte?

C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 8 / 47

Motivations

Pourquoi s"intéresser aux assistants de preuve?Limitations liées à l"indécidabilité et à la complexité

Gérer des preuvesinfaisablesà la mainTransformer les objets mathématiques en objets informatiques

Intégrer raisonnement et calcul

Maximiser la confiance

Emergence d"une nouvelle activité

Génie/Ingénierie des preuves

C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 9 / 47

Outils pour le calcul

calculatrice opérations de basecalcul formel langage spécialisé, fonctions avancées, interfacefeuille de calcul présentation, éditionprogrammation langage universel,

bibliothèques, spécialistesproblème :modéliser, combiner les méthodesC. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 10 / 47

Calcul et Preuve

CalculAssistant de preuve

CalculatriceNoyau de vérification

Feuille de CalculEdition des preuves, tactiques

Calcul formelBibliothèques spécialisées

ProgrammationExtension via plugin

Les machines font mieux les calculs que nous

Elles peuvent aussi nous aider à construire/vérifier des preuves C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 11 / 47

Quelques exemples d"applications

Programmes prouvés

SEL4 (Isabelle/HOL, NICTA), micro-noyau sécurisé de système d"exploitationCompcert (Coq, Inria), compilateur C optimisant Sécurité : modélisation des plateformes JavaCard en Isabelle/HOL et CoqMathématiques : théorème 4 couleurs, conjecture Kepler,

Feit-Thompson...Preuves formelles en informatique

arithmétique des ordinateurs (nombres flottants) cryptographie, combinatoire sémantique des langages de programmation

Back-end pour d"autres environnements

revérification de traces, résolution d"obligations de preuve, couverture de tests C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 12 / 47

Historique assistants de preuve

Automath

A utomatingMathematics ,Nicolaas G. de Br uijn,Eindho ven,1967 Mizar (théor iedes ensemb les)Andrz ejT rybulec,Univ ersityof Białystok, 1973 LCF Lo gicf orComputab leFunctions ,Robin Milner ,Edimbourg et Stanf ord, 1972
HOL (HOL4, HOL-l ight)Higher-Order Logic ,Mik eGordon, Cambr idge,1988

Isabelle

(/HOL, /ZF) Larr yP aulson,Cambr idge,1989 (T obiasNipk ow,Münich)

1980 NuPrl : Bob Constable, Cornell U, 1984

Agda et ses prédecesseurs : Thierry Coquand, Chalmers U, Coq Gér ardHuet et Thierr yCoquand, Inr iaP aris,1984 (Epig ram,O TT,

Matita)

ACL2 A Computati onalLogic f orApplicativ eCommon Lisp ,Rober tS .Bo yer et J Strother Moore, 1990 (NqThm, 1971) PVS Prototype V erificationSystem, Sam Owre ,Shankar et John Rushb y,

SRI, Stanford, 1992

C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 13 / 47

Coq versus Isabelle/HOL

Deux systèmes matures, applications variées

multi-plateformes commandes :Isabelle2015,coqideExpertise locale (BW Isabelle, CP Coq) Un large sous-ensemble commun pour la modélisation logique d"ordre supérieur définitions inductives tactiques

Des choix différents

logique classique versus intuitionniste objets définissables, systèmes de types choix architecturaux C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 14 / 47

Enjeux actuels

Situation

une technologie qui se développe depuis plus de 30 ans des applications phares qui concernent des communautés variées un besoin général d"assistance dans les preuves des outils qui nécessitent une certaine expertise et du temps

Recherches actuelles

Evolution des langages (expressivité, style)

Environnements

langages de tactique bibliothèques parallélisation

Preuves automatiques et sûres

C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 15 / 47

Débouchés industriels

Trusted Logic/Labs!GemaltoClearSy (atelier B)

Adacore

TrustInSoft

Internet of trust

Prove & Run

SafeRiver

Edukera

Activités

Production de logiciels critiques

cartes à puce, aéronautique, ferroviaire ... automobiles, santé, énergie ...

Conception d"outils

C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 16 / 47

Cours 1

1Introduction

2Contexte

3Rappels sur la logique

4Lambda-calcul simplement typé

5Démonstration Coq et Isabelle

6Exercices

C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 17 / 47

Logique du premier ordre

Termes (t;u;:::)x c f(t1;:::;tn)variables (x;y;:::)signature : constantes et symboles de fonction d"arité fixée

Formules logiquest=u?A)B8x;AAutres connecteurs:AA)? 9x;A :8x;:A A_B :A)B A^B :(A):B)Symboles de prédicat avec arité pour des concepts " atomiques »

P(t1;:::;tn)Règles de précédence

:A^B= (:A)^B A_B^C=A_(B^C)

A_B)C= (A_B))C A)B)C=A)(B)C)

8x;A)B=8x;(A)B)9x;A)B=9x;(A)B)C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 18 / 47

Exemples

théorie des paires :

signature :pair(arité 2) etfst,snd(arité 1)axiomes :8x y;fst(pair(x;y)) =x8x y;snd(pair(x;y)) =yxest un multiple de3 signature : constante3 et f onction(arité 2)formule :9y;x=3yxest la somme de deux carrésnotions atomiques :

xa les yeux bleus :couleur-yeux(x) =bleu yeux-bleus(x)xest l"ami dey:ami(x;y)C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 19 / 47

Preuves sous hypothèses (séquents)

A

1;:::;An|{z}

hypothèses` |{z} déductionB|{z}

conclusionNotation;pour les hypothèses (ensemble de formules)Validité : dans toute situation qui rend les hypothèses vraies, la

conclusion est également vraieEquivalent àA1^:::^An)BouA1):::)An)BExemples (dire si les séquents suivants sont vrais)

A)B;A`B,A)B;B`AA)B;B` :AC. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 20 / 47

Logique du premier ordre sortée

La logiquesortéeconsidère plusieurs univers séparés pour les objetsLes sortes sont des symboles (en nombre fini) commenat,bool...Les symboles de constantes, de fonctions ou de prédicats sont déclarés

avec une arité qui donne les sortes des arguments et du résultat.Les variables dans les quantifications sont annotées par leur sorte

Exemple (yeux bleux) :

sortes : individus et couleurs;cconstantes et fonctionsbleu:c,couleur-yeux: []!cprédicat=a pour arité[c;c]il existe une personne aux yeux bleus

9x:;couleur-yeux(x) =bleuLes sortes évitent l"usage de prédicats " ensemblistes » comme

est-couleurouest-individuLes sortes ne permettent pas de représenter n"importe quel ensemble : l"appartenance à la sorte est une propriété syntaxique de l"objet C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 21 / 47

Programmation fonctionnelle

utiliser des fonctions au sens mathématique pour représenter des calculs

abbréviation :f(x) =x2+x+1définition récursive :f(0) =1f(n+1) = (n+1)f(n)calculer :f(3)les fonctions sont des objets comme les autres

fonction d"ordre supérieur :fgdéfinie par(fg)(x) =f(g(x))raisonnement mathématique sur les fonctions

C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 22 / 47

Mélange logique et programmes

Il n"est pas immédiat de raisonner sur des programmes quelconquescalculsimpurs

p=pnon valide sipfait des effets de bord(x++ ==x++)random==randomproblème de terminaisonf(x) =iff(x) =0then1else0

on prouvef(x) =0,f(x) =1, d"où0 =1C. Paulin & B. Wolff (Université Paris Sud)Preuves Interactives2016-17 23 / 47

quotesdbs_dbs28.pdfusesText_34

[PDF] cartes et coupes geologiques - Faculté des Sciences de Rabat

[PDF] Finances publiques 2014-2015 - 22 exercices - Lextenso Etudiant

[PDF] Etude de fonctions

[PDF] realiser l 'etude financiere - Formasup

[PDF] L #8482 évaluation formative

[PDF] COMMENT REALISER UNE FICHE METIER ?

[PDF] la viabilite des radios de proximite

[PDF] CONSEILS POUR REDIGER UNE FICHE DE LECTURE

[PDF] M -Guid - Méditation Chrétienne du Québec

[PDF] Construire et exporter un schéma avec X Mind - WordPresscom

[PDF] Définir une problématique de recherche - Université de Moncton

[PDF] La progression pédagogique La fiche de préparation de - Eduscol

[PDF] Pyramide des biomasses

[PDF] COMMENT FAIRE UNE RECHERCHE SUR INTERNET ?

[PDF] Comment écrire une rédaction: quelques conseils utiles