A Formal Proof of a Unix Path Resolution Algorithm
Preuve formelle d'un algorithme de résolution de chemins dans Unix
Résumé
In the context of file systems like those of Unix, path resolution is the operation that given a
character string denoting an access path, determines the target object (file, directory, etc.) designated by
this path. This operation is not trivial because of the presence of symbolic links. Indeed, the presence of
such links may induce infinite loops.
In this report we consider a path resolution algorithm that always terminate. We propose a formal specifi-
cation of path resolution and we formally prove that our algorithm terminates on any input, and is correct
and complete.
Dans le contexte des systèmes de fichiers comme celui d’UNIX, la résolution d’un chemin est
l’opération qui étant donnée une chaîne de caractère dénotant un chemin d’accès, détermine l’objet cible
(fichier, répertoire, etc.) désigné par ce chemin. Cette opération n’est pas triviale à cause de la présence
de liens symboliques. En effet, la présence de tels liens peut induire la présence de boucles infinies.
Dans ce rapport nous considérons un algorithme de résolution de chemin qui termine toujours. Nous
proposons une spécification formelle de la résolution de chemins et nous prouvons formellement la ter-
minaison de notre algorithme, sa correction et sa complétude.
Origine : Fichiers produits par l'(les) auteur(s)