A Formal Proof of a Unix Path Resolution Algorithm - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2016

A Formal Proof of a Unix Path Resolution Algorithm

Preuve formelle d'un algorithme de résolution de chemins dans Unix

(1, 2) , (1, 2) , (1, 2)
1
2

Abstract

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.
Fichier principal
Vignette du fichier
RR-8987.pdf (606.48 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01406848 , version 1 (01-12-2016)

Identifiers

  • HAL Id : hal-01406848 , version 1

Cite

Ran Chen, Martin Clochard, Claude Marché. A Formal Proof of a Unix Path Resolution Algorithm. [Research Report] RR-8987, Inria. 2016, pp.27. ⟨hal-01406848⟩
388 View
544 Download

Share

Gmail Facebook Twitter LinkedIn More