Variables ind grpe res act : Type. Variable Lire : act. Variable Ecrire : act. Variable dans : ind -> grpe -> Prop. Variable proprio : ind -> res -> Prop. Variable droit : grpe -> act -> res -> Prop. Variable peut : ind -> act -> res -> Prop. (* tout individu qui peut écrire sur une ressource peut aussi la lire *) Check (forall x r, peut x Ecrire r -> peut x Lire r). (* il existe une personne qui peut faire toutes les actions sur toutes les ressources (administrateur système) *) Check (exists x, forall a r, peut x a r). (* Le propriétaire d’une ressource peut effectuer toutes les actions sur cette ressource *) Check (forall x r, proprio x r -> forall a, peut x a r). (* Toute ressource a un et un seul propriétaire *) Check (forall r, exists x, proprio x r /\ forall y, proprio y r -> x=y). (* Aucun groupe n’est vide et toute personne appartient à (au moins) un groupe *) Check ((forall g, exists x, dans x g) /\ forall x, exists g, dans x g). (* Lorsqu’un groupe est autorisé à effectuer une action sur une ressource alors tous les membres de ce groupe peuvent effectuer l’action. *) Check (forall g a r, droit g a r -> forall x, dans x g -> peut x a r).