| Autor: |
Chen, Ran, Clochard, Martin, Marché, Claude |
| Přispěvatelé: |
Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Inria, ANR-15-CE25-0001,Colis,Correction de scripts Linux(2015), ANR-14-LAB3-0007,ProofInUse,Preuve en Œuvre (Intégration de la preuve dans le développement logiciel)(2014) |
| Jazyk: |
angličtina |
| Rok vydání: |
2016 |
| Předmět: |
|
| Zdroj: |
[Research Report] RR-8987, Inria. 2016, pp.27 |
| Popis: |
In the context of file systems like those of Unix, path resolution is the operation that given acharacter string denoting an access path, determines the target object (file, directory, etc.) designated bythis path. This operation is not trivial because of the presence of symbolic links. Indeed, the presence ofsuch 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 correctand complete.; Dans le contexte des systèmes de fichiers comme celui d’UNIX, la résolution d’un chemin estl’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ésencede 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. Nousproposons 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. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
