Un exemple de spécification précise grâce à KAOS et le modèle relationnel

Introduction

L'histoire veut qu'un bug dans Klaro Cards faisait planter le frontend si l'on avait supprimé l'accès à un board qu'un membre avait marqué comme home page.

A l'analyse, on est tombés dans un panneau classique : implémenter la user story Je veux marquer un board comme home page sans correctement tenir compte de l'invariant associé Seuls les boards auquel un utilisateur a accès peuvent être sa home.

Une belle opportunité post-mortem de préciser la manière dont nous aurions dû analyser la chose.

Je commence par revenir sur le manquement d'analyse initial, avant de regarder en détails comment maintenir l'invariant en pratique.

C'est aussi l'occasion pour moi de montrer un peu de KAOS – méthode d'analyse aussi précise que méconnue – et de faire le lien avec le modèle relationnel. Les deux sont basés sur la logique du premier ordre, mais il est rare de les voir utilisés de manière complémentaire. Un peu d'évangélisation, tant je trouve l'approche élégante.

L'erreur initiale

Face à une user story, qui le plus souvent soutient un objectif dit Achieve (tout ou tard, quelque chose de bien) ...

Si j'indique qu'un board est ma home page, alors la prochaine fois que je charge Klaro Cards, j'atterris sur ce board.

... il convient de préciser les conditions où l'utilisateur est autorisé à le faire :

Je ne peux indiquer comme home page qu'un board auquel j'ai accès.

Jusque là, on n'avait tout bien fait : le frontend ne propose que les boards autorisés et le backend vérifie la précondition dans SetHomeBoard.

Caramba, c'est pas assez. Nombre de préconditions cachent des invariants plus forts qu'elles, des objectifs dit Maintain (jamais quelque chose de mal). En l'occurrence, la condition d'accès au board doit rester vraie durant toute la vie de la home, pas seulement lors de sa création.

Logique. Sauf qu'on passe vite à côté.

D'où un premier take away :

Quand la POST condition d'un cas d'utilisation est gardée par une précondition PRE ...

... se demander systématiquement s'il n'y a pas un invariant plus fort POST implique toujours PRE qui se cache.

Si cette phrase n'est pas claire, lisez. Je vais reconstruire cela calmement dans la suite.

Problème à résoudre

L'énoncé sur LinkedIn

Je commence par reprendre le vrai cas, un peu plus compliqué que la description donnée en introduction, et que j'avais partagé sur LinkedIn de la manière suivante :

Exercice d'architecture. Dans Klaro Cards:

1. un User est membre d'un ou plusieurs Workspaces
2. un workspace est une collection de Boards
3. un user peut choisir sa Home, càd un workspace et un board sur lesquels il atterrit par défaut

Une contrainte impose que la home soit un board partagé dans un workspace dont le user est membre.

Comment garantissez vous que cette contrainte est toujours respectée ?
(Vous pouvez supprimer la home si nécessaire en cas de conflit).

Quelle est votre stratégie de test ?

Comment vous assurez-vous que vous avez pensé à tous les cas ?

Clarifications

Suite à quelques questions sur LinkedIn, j'ai précisé ensuite :

* Un board peut être partagé dans plusieurs workspaces
* Un utilisateur n'a qu'une seule home
* On souhaite pouvoir utiliser le logiciel "normalement": supprimer un utilisateur,
  un board, un workspace, supprimer l'accès à un workspace à un utilisateur ou
  "départager" un board dans un workspace sont autant de cas d'utilisation qui ne
  doivent pas être bloqués par la home d'un utilisateur (d'où la note de bas de
  page dans l'énoncé initial)

Dans la suite, je commence par spécifier précisément le problème à résoudre, c'est-à-dire concevoir le produit. Je donnerai des pistes d'implémentation dans la suivante.

Spécification

J'utilise ici la méthode KAOS (Keep All Objective Satisfied) pour préciser formellement la contrainte à laquelle l'énoncé nous invite à réfléchir, et pour explorer et spécifier de manière systématique son impact sur les cas d'utilisation.

Objectif formel

En KAOS la contrainte est modélisée comme l'objectif ci-dessous, sous la responsabilité du logiciel (on parle alors d'un requis sur le logiciel):

Maintain[Home légitime par utilisateur]
  Def: la home d'un utilisateur est un board partagé dans un workspace dont le user est membre
  FormalDef: FORALL(u:User, b:Board, w:Workspace) isHome(u, b, w) IMPLIES (isMember(u, w) and sharedIn(b, w))

Un objectif de type Maintain est un invariant d'état que le système doit maintenir, typiquement en contraignant les exécutions permises du logiciel. Sa définition formelle introduit :

• Trois entités du domaine: User, Board et Workspace
• Trois prédicats:
  • isHome(u: User, b: Board, w: Workspace) qu'on définit comme vrai si et seulement si le couple (b, w) est défini comme home pour l'utilisateur u
  • isMember(u: User, w: Workspace) vrai si et seulement si l'utilisateur u est membre du workspace w
  • sharedIn(b: Board, w: Workspace) vrai si et seulement si le board b est accessible/partagé dans le workspace w

Les prédicats restent ici abstraits, et seront typiquement implémentés par des variables mutables du logiciel (un modèle objet et/ou une base de données relationnelle - voir plus loin).

L'expression en logique du premier ordre dit, en substance : Il est toujours vrai que SI isHome ALORS isMember && sharedIn. C'est une traduction directe de notre contrainte en langue naturelle.

Opérationnalisation

Dans KAOS les patterns d'opérationnalisation permettent d'identifier de manière systématique quels cas d'utilisation (appelés Operations) sont impactés par un requis. C'est à dire qu'on contraint explicitement ces cas d'utilisation pour garantir le requis.

Dans le cas d'un requis Il est toujours vrai que SI X ALORS Y, KAOS indique qu'il faut:

• Empêcher X de devenir vrai si Y n'est pas vrai également (ou le faire devenir vrai simultanément)
• Empêcher Y de devenir faux si X est vrai (ou le faire devenir faux simultanément)

Dans notre exemple, on veut donc contraindre les prédicats de la manière suivante :

• isHome(u,b,w) ne peut devenir vrai que si les board et workspace respectent les critères
• isMember(u,w) ne peut devenir faux qu'en supprimant la home en conflit
• sharedIn(b,w) ne peut devenir faux qu'en supprimant toutes les home en conflit

Formellement, les patterns de KAOS nous offrent l'opérationalisation suivante:

Operation SetUserHome(u: User, b: Board, w: Workspace)
  Def: définit un couple (board, workspace) comme home d'un utilisateur
  DOM PRE: NOT isHome(u, b, w)
  DOM POST: isHome(u, b, w)
  REQ PRE for Maintain[Home légitime par utilisateur]: isMember(u, w) and sharedIn(b, w)

Operation DropMembership(u: User, w: Workspace)
  Def: supprime un utilisateur d'un workspace
  DOM PRE: isMember(u, w)
  DOM POST: NOT isMember(u, w)
  REQ POST for Maintain[...]: FORALL(b: Board) !isHome(u, b, w)

Operation UnshareBoard(b: Board, w: Workspace)
  Def: supprime le partage d'un board au sein d'un workspace
  DOM PRE: sharedIn(b, w)
  DOM POST: NOT sharedIn(b, w)
  REQ POST for Maintain[...]: FORALL(u: User) !isHome(u, b, w)

Operation DropUser ...
Operation DropBoard ...
Operation DropWorkspace ...

Observez que pour garantir le requis, la première opération voit son exécution contrainte par une précondition ; les deux suivantes se voient imposer, via leur postcondition, de supprimer les home qui violeraient le requis.

(J'omets les détails des opérations DropUser, DropBoard et DropWorkspace qui doivent donner lieu au même genre de mécanique de suppression des home conflictuelles ^[1])

Liens entre prédicats et opérations

En KAOS, une opération implémente une transition naturelle d'état du système -- dites "du domaine", soit DOM -- sous contrainte des requis (REQ). Une heuristique simple permet d'identifier aisément les opérations en question, il suffit en quelque sorte de se demander quelle opération est naturellement associée à un prédicat donné :

• SetUserHome implémente une transition d'état : !isHome --> isHome
• DropMembership implémente la transition d'état isMember -> !isMember
• UnshareBoard implémente la transition d'état sharedIn -> !sharedIn

Les REQ PRE for Maintain[...] et REQ POST for Maintain[...] traduisent la relation WHY/HOW entre l'opérationalisation et les objectifs de plus haut niveau qui en expliquent l'existence. C'est une forme naturelle de documentation objectif/solution, en quelque sorte.

Conceptions alternatives

Notez que l'opérationalisation ci-dessus n'est pas la seule possible. C'est la plus naturelle pour les besoins exprimés, mais l'on pourrait aussi bien proposer la conception suivante:

Operation SetUserHome(u: User, b: Board, w: Workspace)
  DOM PRE: NOT isHome(u, b, w)
  DOM POST: isHome(u, b, w)
  REQ PRE for Maintain[...]: isMember(u, w) and sharedIn(b, w)

Operation DropMembership(u: User, w: Workspace)
  DOM PRE: isMember(u, w)
  DOM POST: NOT isMember(u, w)
  REQ PRE for Maintain[...]: NOT EXISTS(b: Board) isHome(u, b, w)

Operation UnshareBoard(b: Board, w: Workspace)
  DOM PRE: sharedIn(u, w)
  DOM POST: NOT sharedIn(u, w)
  REQ PRE for Maintain[...]: NOT EXISTS(u: User) isHome(u, b, w)

Operation DropUser ...
Operation DropBoard ...
Operation DropWorkspace ...

Dans cette opérationalisation, on empêche la suppression d'un membre ou d'un board d'un workspace dès lors qu'un utilisateur au moins les utilise comme home (via des REQ PRE cette fois). Le logiciel est moins pratique, certes, mais ne viole jamais la contrainte souhaitée.

Une autre opérationalisation encore pourrait être celle ci-dessous, menant à un tout autre produit : le logiciel autorise l'utilisateur à définir sa home à sa guise, et ajoute automatiquement le board et l'utilisateur au workspace pour ne pas violer la contrainte.

Operation SetUserHome(u: User, b: Board, w: Workspace)
  DOM PRE: NOT isHome(u, b, w)
  DOM POST: isHome(u, b, w)
  REQ POST for Maintain[...]: isMember(u, w) and sharedIn(b, w)

On le voit, la méthode KAOS permet d'être précis, de documenter le lien entre cas d'utilisation et requis, et d'explorer des conceptions alternatives du produit pour les mêmes objectifs.

Retour à l'erreur d'analyse

Revenons à notre conception où les homes conflictuelles sont supprimées. Pour reboucler avec l'introduction, l'équipe Klaro Cards était passée à côté de l'invariant mais avait bien identifié la précondition de SetHomeBoard, à savoir que les workspace et board doivent être accessibles pour créer sa home :

REQ PRE(SetHomeBoard) = isMember(...) and sharedIn(...)

Dès lors que la DOM POST est isHome(...) l'heuristique proposée plus haut aurait pu nous mettre sur la voie :

N'est il pas plus vrai encore que DOM POST => REQ PRE ?

Soit que isHome => isMember and sharedIn ?

Bien sûr que oui.

Implémentation impérative

Le seul "détail" qui mérite vraiment notre attention lors de l'implémentation impérative, c'est la manière de gérer les REQ POST des six cas d'utilisation 😅, imposées par la spécification.

Gérer les post-conditions

Les post-conditions des cas d'utilisation qui peuvent violer l'invariant, et doivent dès lors garantir la suppression des home, suggèrent l'existence d'opérations utilitaires suivantes:

// Called by/On DropMembership
Operation DropConflictualUserHome(u:User, w:Workspace)

// Called by/On UnshareBoard
Operation DropConflictualHomes(b:Board, w:Workspace)

// Called by/On DropUser
Operation DropAllUserHomes(u:User)

// Called by/On DropBoard
Operation DropAllHomesUsing(b:Board)

// Called by/On DropWorkspace
Operation DropAllHomesIn(w:Workspace)

On voit des besoins diversifiés, dûs aux différents contextes qui peuvent amener à violer le requis à mal. Différents mécanismes permettent d'éviter un couplage fort entre les opérations principales et ces opérations utilitaires. On pense par exemple à un mécanisme événementiel qui voit ces dernières ne pas être appelées directement, mais réagir de manière événementielle à l'exécution des premières.

Une autre approche consiste à n'avoir qu'une méthode utilitaire qui résoud tous les cas d'un coup :

// Called everytime we suspect a possible violation
Operation DropAllConflictualHomes()

Exemple en Java/DDD

Sur base de mon analyse ci-dessus, Claude Code m'a suggéré l'implémentation suivante en Java/DDD.

N'étant pas vraiment expert DDD moi-même, je vous laisse me faire vos commentaires. Ce type de solution me fait personnellement peur, tant elle implique un problème évident de N+1 queries pour garantir les post-conditions.

// === Domain ===

class User {
	private UserId id;
	private Home home; // nullable

	void setHome(Board b, Workspace w) {
		if (!w.hasMember(this))
			throw new InvariantViolation("User must be member of workspace");
		if (!w.hasBoard(b))
			throw new InvariantViolation("Board must be shared in workspace");
		this.home = new Home(b.id(), w.id());
	}

	// --- Opérations utilitaires (REQ POST) ---

	// Called by DropMembership
	void dropConflictualHome(WorkspaceId wid) {
		if (home != null && home.workspaceId().equals(wid))
			home = null;
	}

	// Called by UnshareBoard
	void dropConflictualHome(BoardId bid, WorkspaceId wid) {
		if (home != null && home.boardId().equals(bid) && home.workspaceId().equals(wid))
			home = null;
	}

	// Called by DropUser, DropBoard, DropWorkspace
	void dropHome() {
		home = null;
	}
}

record Home(BoardId boardId, WorkspaceId workspaceId) {}

// === Ports ===

interface UserRepository {
	User findById(UserId id);
	List<User> findByHomeWorkspace(WorkspaceId wid);
	List<User> findByHomeBoardInWorkspace(BoardId bid, WorkspaceId wid);
	void save(User u);
	void delete(User u);
}

// === Application Services ===

class SetUserHome {
	void execute(UserId uid, BoardId bid, WorkspaceId wid) {
		var u = users.findById(uid);
		var w = workspaces.findById(wid);
		var b = boards.findById(bid);
		u.setHome(b, w);  // REQ PRE vérifié ici
		users.save(u);
	}
}

class DropMembership {
	void execute(UserId uid, WorkspaceId wid) {
		// REQ POST: forall b, !isHome(u,b,w)
		var u = users.findById(uid);
		u.dropConflictualHome(wid);
		users.save(u);

		var w = workspaces.findById(wid);
		w.removeMember(uid);
		workspaces.save(w);
	}
}

class UnshareBoard {
	void execute(BoardId bid, WorkspaceId wid) {
		// REQ POST: forall u, !isHome(u,b,w)
		for (var u : users.findByHomeBoardInWorkspace(bid, wid)) {
			u.dropConflictualHome(bid, wid);
			users.save(u);
		}

		var w = workspaces.findById(wid);
		w.removeBoard(bid);
		workspaces.save(w);
	}
}

class DropUser {
	void execute(UserId uid) {
		// REQ POST: forall b,w, !isHome(u,b,w)
		var u = users.findById(uid);
		u.dropHome();
		users.delete(u);
	}
}

class DropBoard {
	void execute(BoardId bid) {
		// REQ POST: forall u,w, !isHome(u,b,w)
		for (var u : users.findByHomeBoard(bid)) {
			u.dropHome();
			users.save(u);
		}
		boards.delete(boards.findById(bid));
	}
}

class DropWorkspace {
	void execute(WorkspaceId wid) {
		// REQ POST: forall u,b, !isHome(u,b,w)
		for (var u : users.findByHomeWorkspace(wid)) {
			u.dropHome();
			users.save(u);
		}
		workspaces.delete(workspaces.findById(wid));
	}
}

Je ne m'étends pas ici, je trouve personnellement l'approche impérative trop compliquée, même si nécessaire pour tenir les requis. L'approche relationnelle est élégante et simple, en comparaison, même si plus implicite.

Implémentation relationnelle

L'approche relationnelle découle plus ou moins directement de la spécification donnée précédemment. Et pour cause : le modèle relationnel est directement compatible avec la logique du premier ordre. C'est choux-vert et vert-choux, comme je me propose de vous montrer.

Dépendances fonctionnelles

Si vous avez eu un cours de base de données, vous devez vaguement vous souvenir de la notion de dépendance fonctionnelle.

Notée A -> B, où A et B sont des ensembles d'attributs, une dépendance fonctionnelle indique que les attributs de B (dits les "dépendants") sont directement identifiés par une clef unique définie par les attributs de A (dit le "déterminant"). Ces dépendances fonctionnelles identifient les "tables" nécessaires de la base de données :

Pour nos trois entités, cela donne sans surprise :

# la table des users
{ UserID } -> { UserName, ... }

# la table des boards
{ BoardID } -> { BoardName, ... }

# la table des workspaces
{ WorkspaceID } -> { WorkspaceName, ... }

et, sensiblement plus intéressant, nos prédicats se transforment quasi magiquement également :

# isMember(u, w) : la table des membres de workspaces
{ UserID, WorkspaceID } -> { MemberSince, ... }

# sharedIn(b, w) : la table des boards des workspaces
{ BoardID, WorkspaceID } -> { SharedSince, ... }

# isHome(u, b, w) : la table des homes
{ UserID } -> { BoardID, WorkspaceID }

Le dernier cas mérite un commentaire : le fait qu'un utilisateur n'a qu'une seule home est une contrainte dont nous avons peu parlé, mais qui explique pourquoi la dépendance fonctionnelle qui découle de isHome(u,b,w) n'a que UserId dans le déterminant.

Expression de la contrainte

Reprenons maintenant la contrainte en logique du premier ordre suivante :

FORALL(u:User, b:Board, w:Workspace) isHome(u, b, w) IMPLIES isMember(u, w) and sharedIn(b, w)

Le modèle relationnel prend une approche ensembliste de la logique du premier ordre. Dans le cas qui nous occupe elle se transforme comme suit :

isHome{ UserID, WorkspaceID }  IS SUBSET OF isMember{ UserID, WorkspaceID }
AND
isHome{ BoardID, WorkspaceID } IS SUBSET OF sharedIn{ BoardID, WorkspaceID }

Je vous passe la sémantique de ces expressions. Sachez juste qu'il s'agit ici tout simplement de clefs étrangères.

Qui dit clefs étrangères dit "mécanisme de mitigation de violation des contraintes". Dont celui qui nous occupe ici, et qui revient à déclarer qu'on supprime automatiquement les home qui violent la contrainte qui nous occupe.

isHome{ ... } IS SUBSET OF isMember{ ... } ON DELETE CASCADE
AND
isHome{ ... } IS SUBSET OF sharedIn{ ... } ON DELETE CASCADE

Résultat en SQL

Comme le suggère l'implémentation proposée par Claude Code, l'approche impérative nécessite pas mal de logique métier, et risque un grand nombre de N+1 donc des soucis de performance. Ce n'est pas vrai en SQL, et c'est bien pour cela qu'à défaut d'autre chose de meilleur que lui, on apprécie son existence :

CREATE TABLE users (
  user_id INT PRIMARY KEY
);

CREATE TABLE workspaces (
  workspace_id INT PRIMARY KEY
);

CREATE TABLE boards (
  board_id INT PRIMARY KEY
);

CREATE TABLE shared_in (
  board_id INT NOT NULL REFERENCES boards(board_id) ON DELETE CASCADE,
  workspace_id INT NOT NULL REFERENCES workspaces(workspace_id) ON DELETE CASCADE,
  PRIMARY KEY (workspace_id, board_id)
);

CREATE TABLE is_member (
  user_id INT REFERENCES users(user_id) ON DELETE CASCADE,
  workspace_id INT REFERENCES workspaces(workspace_id) ON DELETE CASCADE,
  PRIMARY KEY (user_id, workspace_id)
);

CREATE TABLE homes (
  user_id INT PRIMARY KEY REFERENCES users(id) ON DELETE CASCADE,
  board_id INT NOT NULL,
  workspace_id INT NOT NULL,

  -- le board doit appartenir au workspace
  FOREIGN KEY (board_id, workspace_id)
    REFERENCES shared_in(board_id, workspace_id) ON DELETE CASCADE,

  -- le user doit être membre du workspace
  FOREIGN KEY (user_id, workspace_id)
    REFERENCES is_member(user_id, workspace_id) ON DELETE CASCADE
);

Comme on le voit ci-dessus, l'invariant est implémenté par les deux clefs étrangères, qui implémentent de simples contraintes d'inclusion, avec mécanisme de mitigation en cas de conflit.

Simple. Elégant. Et contrairement à ce qu'on peut dire parfois, c'est une approche plutôt directe de l'implémentation des requis, pour qui comprend en tout cas le lien logique entre la spécification et l'implémentation.

Conclusion

Il y a me semble-t-il trois choses à retenir de cet exercice:

1. Cherchez les invariants derrière les préconditions. Quand une opération est gardée par une précondition, demandez-vous si cette condition ne doit pas rester vraie après l'opération aussi. Si oui, vous avez un objectif Maintain — et toutes les opérations qui peuvent l'invalider doivent être identifiées et contraintes. C'est le cas qu'on a manqué, et qu'on manque souvent.

2. J'espère vous avoir convaincu que KAOS rend l'analyse systématique. L'opérationnalisation d'un Maintain[SI X ALORS Y] force à se poser deux questions : qu'est-ce qui peut rendre X vrai ? Qu'est-ce qui peut rendre Y faux ? Les réponses désignent les opérations impactées, et la méthode nous dit comment les contraindre — par précondition ou par postcondition. On n'oublie rien, et on peut explorer des conceptions alternatives du produit pour un même objectif.

3. Le modèle relationnel est le compagnon naturel de cette approche. Ce n'est pas un hasard : KAOS et le modèle relationnel partagent la même fondation — la logique du premier ordre. Un invariant KAOS se traduit souvent simplement par des contraintes de clefs étrangères sur des tables qui encodent naturellement les prédicats du domaine. Là où l'approche impérative peut demander des dizaines de lignes de code et autant d'occasions de se tromper, le modèle relationnel l'exprime déclarativement. Dommage que SQL soit si limité en pratique.

Exercice

Certaines personnes ont suggéré sur LinkedIn qu'une solution avec eventual consistency pouvait faire l'affaire également : on autorise temporairement la définition d'une home qui viole l'invariant, mais on le répare immédiatement.

Cela revient à afaiblir l'invariant en introduisant un objectif Achieve qui ressemble à ceci:

Achieve[Home conflictuelles supprimées]
  Def: toute home qui n'est pas accessible à son utilisateur est immédiatement supprimée
  Formaldef: FORALL(u:User, b:Board, w:Workspace) isHome(u,b,w) and NOT(isMember(u,w) and sharedIn(b,w)) IMPLIES NEXT(!isHome(u,b,w))

(où NEXT veut dire "dans l'état immédiatement après")

Cet objectif mène naturellement à l'opération suivante :

Operation DropHome(u:User, b:Board, w:Workspace)
  DOM PRE: isHome(u, b, w)
  DOM POST: !isHome(u, b, w)
  REQ TRIG for Achieve[Home conflictuelles supprimées]: ???

On vous demande de spécifier la REQ TRIG, qui est une condition qui, quand elle est vraie, impose que l'opération s'exécute immédiatement.

Comment modifiez-vous l'architecture pour garantir cette TRIGGER condition ?