A Formal Proof of a Unix Path Resolution Algorithm

Ran Chen 1, 2, 3 Martin Clochard 2, 3 Claude Marché 2, 3
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : 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.
Type de document :
Rapport
[Research Report] RR-8987, Inria. 2016, pp.27
Liste complète des métadonnées

https://hal.inria.fr/hal-01406848
Contributeur : Claude Marché <>
Soumis le : jeudi 1 décembre 2016 - 15:52:40
Dernière modification le : samedi 18 février 2017 - 01:10:17
Document(s) archivé(s) le : mardi 21 mars 2017 - 11:02:56

Fichier

RR-8987.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01406848, version 1

Citation

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〉

Partager

Métriques

Consultations de
la notice

375

Téléchargements du document

223