Logique et raisonnement¶

Pourquoi un architecte a besoin de raisonner formellement — des spécifications sans ambiguite aux invariants qui tiennent sous charge.

La précision comme outil d'ingénierie¶

Un architecte qui ne peut pas exprimer formellement ce que son système doit faire ne peut pas vérifier qu'il le fait. Le langage naturel introduit de l'ambiguite là où on a besoin de certitude. "Le service répond rapidement" — qu'est-ce que cela signifie exactement ? 200ms ? 1s ? Pour 99% des requêtes ou pour toutes ?

La logique formelle n'est pas un exercice academique. C'est le fondement de :

• la spécification sans ambiguite des contrats d'API (pre-conditions, post-conditions)
• la vérification que deux requirements ne se contredisent pas
• la demonstration qu'un algorithme est correct
• la construction d'invariants que les tests automatises peuvent vérifier

Logique propositionnelle¶

La logique propositionnelle raisonne sur des propositions — des énoncés qui sont soit vrais soit faux. Une proposition est une affirmation avec une valeur de vérité : "le service est disponible", "la requête est autorisee", "le cache est chaud".

Connecteurs logiques¶

Les propositions se combinent via des connecteurs. Soient \(P\) et \(Q\) deux propositions quelconques.

L'implication \(P \rightarrow Q\) ("si P alors Q") est souvent mal interprétée. Elle est fausse uniquement quand la premise est vraie et la conclusion est fausse. Si \(P\) est fausse, l'implication est vraie quelle que soit \(Q\) -- "si \(2+2=5\) alors la lune est en fromage" est une implication vraie en logique classique, car la premise est fausse.

Tables de vérité¶

Une table de vérité énuméré toutes les combinaisons possibles de valeurs pour déterminer la valeur d'une formule complexe. Pour \(n\) variables, il y a \(2^n\) lignes.

Exemple : vérifier que \(P \rightarrow Q\) est équivalente a \(\lnot P \lor Q\).

Les deux colonnes sont identiques — les deux formules sont équivalentes. Cette équivalence sert lors de la negation d'implications.

Tautologies et contradictions¶

Une tautologie est une formule toujours vraie quelle que soit la valeur de ses variables. Exemples fondamentaux :

• Tiers exclu : \(P \lor \lnot P\) -- soit \(P\) est vrai, soit \(\lnot P\) est vrai, pas de milieu
• Modus ponens : \((P \land (P \rightarrow Q)) \rightarrow Q\) -- si \(P\) est vrai et que \(P\) implique \(Q\), alors \(Q\) est vrai
• Loi de De Morgan : \(\lnot(P \land Q) \iff (\lnot P \lor \lnot Q)\)

Une contradiction est une formule toujours fausse. Exemple : \(P \land \lnot P\).

Les lois de De Morgan sont particulièrement utiles en programmation :

Traduction directe : nier "le user est admin ET le compte est actif" donne "le user n'est pas admin OU le compte est inactif". Comprendre cette équivalence evite des bugs classiques dans les conditions de sécurité.

Formes normales¶

Toute formule propositionnelle peut être reecrite en forme normale :

FNC (Forme Normale Conjonctive) -- conjonction de disjonctions : \((A \lor B) \land (\lnot A \lor C)\). Utilisée par les solveurs SAT, la vérification formelle, les moteurs de règles.

FND (Forme Normale Disjonctive) -- disjonction de conjonctions : \((A \land B) \lor (\lnot A \land C)\). Plus lisible pour l'analyse des cas.

Predicats et quantificateurs¶

La logique propositionnelle traite des propositions fixes. La logique des predicats etend cela aux énoncés sur des objets variables, ce qui permet de raisonner sur des structures de données, des collections, et des propriétés parametriques.

Predicats¶

Un predicat est une fonction qui retourné une valeur de vérité. Disponible(service), Superieur(x, 0), Connecte(noeud_A, noeud_B) sont des predicats. Le domaine de discours définit l'ensemble des valeurs que les variables peuvent prendre.

Quantificateurs¶

Exemples en contexte système :

-- "Toute requete autorisee est traitee."

-- "Au moins un noeud est disponible."

-- "Chaque utilisateur a exactement une session active."

Negation des quantificateurs¶

La negation intervertit les quantificateurs et nie le predicat interne :

Application : nier "tous les services sont disponibles" donne "il existe un service qui n'est pas disponible". Utile lors de la rédaction de tests — un test qui refute un invariant doit construire le predicat negatif.

Variables libres et liees¶

Une variable est liee quand elle est sous la portee d'un quantificateur (\(x\) dans \(\forall x,\ P(x)\)). Elle est libre sinon. Une formule sans variable libre est une phrase logique -- elle a une valeur de vérité définie. Une formule avec des variables libres est un schéma qu'on instancie.

Méthodes de demonstration¶

Démontrer qu'un algorithme est correct, qu'une propriété est invariante, qu'une spécification est cohérente — tout cela requiert des méthodes de demonstration rigoureuses. Il en existe quatre principales, chacune adaptée a un type de problème.

Demonstration directe¶

La plus intuitive : on part des hypothèses et on applique des règles logiques jusqu'à atteindre la conclusion.

Forme : on suppose \(P\) vrai, on en déduit \(Q\) par étapes.

Exemple : démontrer que si un entier \(n\) est pair, alors \(n^2\) est pair.

Hypothese : \(n\) est pair

Definition : \(\exists k \in \mathbb{Z},\ n = 2k\)

Calcul : \(n^2 = (2k)^2 = 4k^2 = 2(2k^2)\)

Conclusion : \(n^2 = 2m\) avec \(m = 2k^2\), donc \(n^2\) est pair.

Demonstration par contraposee¶

L'implication \(P \rightarrow Q\) est équivalente a sa contraposee \(\lnot Q \rightarrow \lnot P\). Quand il est difficile de partir de \(P\) pour atteindre \(Q\), on peut partir de \(\lnot Q\) pour atteindre \(\lnot P\).

Exemple : démontrer que si \(n^2\) est impair, alors \(n\) est impair.

Contraposee : si \(n\) est pair, alors \(n^2\) est pair. C'est exactement la demonstration directe precedente. Donc par contraposee, si \(n^2\) est impair, \(n\) est impair.

En architecture : démontrer "si le système satisfait l'invariant I alors la propriété P tient" est souvent plus facile par la contraposee "si P est violee, alors I est viole".

Demonstration par l'absurde¶

On suppose que la conclusion est fausse (\(\lnot Q\)), et on dérivé une contradiction. La contradiction prouve que \(\lnot Q\) est fausse, donc \(Q\) est vraie.

Forme : supposer \(P \land \lnot Q\), dériver une contradiction, conclure \(P \rightarrow Q\).

Exemple : démontrer qu'il n'existe pas de plus grand entier.

Hypothese : supposons qu'il existe un plus grand entier \(N\).

Construction : soit \(M = N + 1\).

Propriete : \(M > N\) par construction.

Contradiction : \(M\) est un entier superieur au "plus grand entier" \(N\).

Conclusion : l'hypothese est fausse -- il n'existe pas de plus grand entier.

En informatique : la demonstration que le problème de l'arrêt est indecidable utilisé ce principe (diagonalisation de Cantor / Turing).

Demonstration par récurrence¶

Pour les propriétés sur les entiers ou les structures inductives (listes, arbres), la récurrence est l'outil naturel.

Principe :

1. Cas de base : démontrer \(P(0)\) (ou \(P(1)\), ou \(P(\text{cas\_initial})\))
2. Hypothèse d'induction : supposer \(P(n)\) vraie pour un \(n\) quelconque
3. Étape d'induction : démontrer \(P(n+1)\) en utilisant \(P(n)\)

Exemple : démontrer que la somme \(1 + 2 + \ldots + n = \frac{n(n+1)}{2}\).

Base : \(n=1\). Somme \(= 1\). Formule : \(\frac{1 \times 2}{2} = 1\). Verifie.

Hypothese : supposer \(1 + 2 + \ldots + n = \frac{n(n+1)}{2}\).

Etape :

Récurrence forte : l'hypothèse porte sur tous les \(k \leq n\) (utile pour les algorithmes diviser pour regner).

Induction structurelle : l'hypothèse porte sur les sous-structures. Pour démontrer \(P(\text{arbre})\), on suppose \(P\) vraie pour les sous-arbres et on démontré \(P\) pour l'arbre entier. Base de la correction des algorithmes recursifs sur des structures de données.

Applications : spécification et invariants¶

Pre/post-conditions et logique de Hoare¶

La logique de Hoare formalise la correction des programmes via des triplets \(\{P\}\ C\ \{Q\}\) ou :

• \(P\) est la pre-condition (ce qui doit être vrai avant l'exécution)
• \(C\) est la commande (le code exécuté)
• \(Q\) est la post-condition (ce qui doit être vrai après)

Ce triplet spécifié le comportement attendu independamment de l'implémentation. Un test peut vérifier la post-condition, un analyseur statique peut prouver que le code respecte le triplet.

def virer(self, montant: float) -> None:
    # Pre-condition
    assert self.solde >= montant and montant > 0, (
        f"Virement impossible: solde={self.solde}, montant={montant}"
    )
    solde_avant = self.solde  # pour verifier la post-condition

    self.solde -= montant

    # Post-condition
    assert self.solde == solde_avant - montant
    assert self.solde >= 0

from functools import wraps

def requires(condition, message):
    def decorator(fn):
        @wraps(fn)
        def wrapper(*args, **kwargs):
            assert condition(*args, **kwargs), message
            return fn(*args, **kwargs)
        return wrapper
    return decorator

@requires(
    lambda self, montant: self.solde >= montant and montant > 0,
    "Pre-condition violation: solde insuffisant ou montant invalide"
)
def virer(self, montant: float) -> None:
    self.solde -= montant

Invariants de boucle¶

Un invariant de boucle est une propriété qui est vraie avant chaque iteration et préservée par chaque iteration. Il sert à démontrer la correction d'un algorithme iteratif.

Pour prouver qu'un invariant \(I\) suffit :

1. Initialisation : \(I\) est vrai avant la première iteration
2. Preservation : si \(I\) est vrai avant une iteration et la condition de boucle est vraie, \(I\) est vrai après l'iteration
3. Terminaison : quand la boucle se termine, \(I \land \lnot\text{condition}\) donne la post-condition

Exemple : recherche binaire.

def recherche_binaire(tableau, cible):
    gauche, droite = 0, len(tableau) - 1

    # Invariant : si cible est dans tableau, elle est dans tableau[gauche..droite]
    while gauche <= droite:
        milieu = (gauche + droite) // 2
        if tableau[milieu] == cible:
            return milieu
        elif tableau[milieu] < cible:
            gauche = milieu + 1  # preserve l'invariant : cible > milieu, donc gauche..droite correct
        else:
            droite = milieu - 1  # preserve l'invariant : cible < milieu, donc gauche..droite correct

    return -1
    # A la sortie : gauche > droite, donc la plage est vide.
    # Par l'invariant : cible n'est pas dans le tableau.

Spécification formelle en pratique¶

La spécification formelle n'impose pas d'utiliser un langage formel lourd (TLA+, Alloy) dans tous les projets. Une discipline minimaliste suffit dans la plupart des cas :

Cohérence et completude d'un système de règles¶

Un ensemble de règles métier peut être formule en logique et analyse mecaniquement :

• Cohérence : les règles ne se contredisent pas (pas de formule et sa negation deduisibles)
• Completude : chaque cas est couvert (aucun scenario sans règle applicable)
• Redondance : certaines règles sont des conséquences d'autres (peut être voulu ou non)

Regle 1 : \(\text{Utilisateur.age} < 18 \rightarrow \text{NePeutPasAcheterAlcool}\)

Regle 2 : \(\text{Utilisateur.age} \geq 21 \rightarrow \text{PeutAcheterAlcool}\) (droit americain)

Regle 3 : \(\text{Utilisateur.age} \in [18, 20] \rightarrow \text{???}\) (cas manquant selon la juridiction)

Identifier les lacunes avant de déployer le système, pas après avoir traite des cas incorrectement pendant des mois.

Formulaire des equivalences utiles¶

Ces equivalences sont directement applicables pour simplifier des conditions complexes dans le code, raisonner sur des filtres de requêtes, ou analyser des règles d'accès.