Logique & Démonstration

Introduction

Démonstrations…

  • Pourquoi ?
  • Quoi ?
  • Comment ?

Pourquoi on veut démontrer ?

📐 En mathématiques

  • Tous les résultats reposent sur des démonstrations
  • La preuve est parfois plus importante que le résultat lui-même

💻 En informatique

  • Application des maths :
    On utilise les mathématiques pour raisonner sur les programmes et les systèmes.
  • Objectif : Prouver l’absence de bugs dans les programmes pour garantir leur fiabilité.

Deux grandes approches

🧪 Tester

test

✅ Prouver

preuve

Tester

Avantages

  • Rapide
  • Facile

⚠ Inconvénients

  • pas toujours scientifique
  • Ne couvre pas tous les bugs

Program testing can be used to show the presence of bugs, but never to show their absence

Dijkstra

Preuve formelle

Avantages

  • Garanties scientifiques
  • Repose sur les maths

Inconvénients

  • Repose sur les maths

Exemple : admin d’un serveur

On veut vérifier que les accès sont cohérents avec les règles du serveur :

  • Connexion impossible si
    • ban
    • compte non créé
    • psswd incorrect
    • plus de 50 joueurs déjà connectés
  • Ban si
    • plus de 10 messages en 30 secondes
    • partage de comptes
    • utilisation de mods interdits
On teste
# Test unitaire pour vérifier le ban de spam
def test_ban_spam():
    joueur = Joueur("Sarah")
    for _ in range(11):
        joueur.envoyer_message("Spam!") 

    if(joueur.est_banni()):
        print("test ban 1 OK")
    else:
        print("test ban 1 échec")
On prouve
Theorem ban_rules :
    (msg_30_sec > 10 \/ account_nb_user > 1 \/ forbidden_mod) -> ban.
Proof.
    …
Qed.

Theorem connexion_rules :
    (ban \/ wrong_psswd \/ nb_players>=50 \/ unregistered) -> ~connect.
Proof.
    …
Qed.

Un logicien est il encore utile en 2026 ?

L’IA peut-elle éviter d’avoir à faire ce travail pénible ?

Une question de spécification

flowchart LR
    A["Déterminer ce qui doit </br> être vérifié"]
    B["Écrire les théorèmes </br> à prouver"]
    C["**Écrire les preuves**"]
    D("Certifier les preuves </br> avec un outil fiable")

    A --> B
    B --> C
    C --> D

Où est-ce que ça pourrait mal se passer ?

Theorem all_numbers_are_even : 
    forall (n:nat), exists (m:nat), m>0 /\ m*2=n
        \/ 2+2=4.
    
Proof.
    intro n. exists 42. right. simpl. reflexivity.
Qed.

Un outil logiciel pour la preuve : Rocq

`

Definition
def

test

Warning

Voir

Tip 1: Ti