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 (a file, a 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. We consider a path resolution algorithm that always terminate, detecting if it enters an infinite loop and reports a resolution failure in such a case. We propose a formal specification of path resolution and we formally prove that our algorithm terminates on any input, and is correct and complete with respect to our formal specification.
@article{6767,
title = {A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links},
journal = {Journal of Formalized Reasoning},
volume = {10},
year = {2017},
doi = {10.6092/issn.1972-5787/6767},
language = {EN},
url = {http://dml.mathdoc.fr/item/6767}
}
Chen, Ran; Clochard, Martin; Marché, Claude. A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links. Journal of Formalized Reasoning, Tome 10 (2017) . doi : 10.6092/issn.1972-5787/6767. http://gdmltest.u-ga.fr/item/6767/