xfarrow
/
dircomp
mirror of https://github.com/xfarrow/dircomp.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Proved point 1-2 out of 4

xfarrow 2023-04-21 19:55:49 +00:00
parent e106b7d73b
commit 40d365eed6
2 changed files with 29 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Home.md

@ -1 +0,0 @@
Welcome to the dircomp wiki!

29
Mathematical-correctness-of-dircomp.md Normal file

@ -0,0 +1,29 @@
Mathematical correctness of dircomp.
References dircomp `1.0.3`
## Definitions
Two directories are considered to be equivalent if and only if these conditions apply:
1. They have the same number of files and folders;
2. For each file in a directory, there is the same file in the other. Two files are considered to be the same
if <ol>
<li> they have the same name, including extension;</li>
<li> they have the same content;</li>
</ol>
3. For each folder in a directory, there is a folder with the same name in the other;
4. [Will apply only if the `-r` option is specified]. For each folder in a directory, there is an equivalent folder in the other, with the same name.
## Proof
The main function responsable for telling if two directories are the same is `analyze_directories()`. We will prove its correctness in order to prove the correctness of the whole program.
**1.** It is straightforward to note that in every loop over both the directories (`while ((element = readdir(directory1)) != NULL)` and `while ((element = readdir(directory2)) != NULL)`) it is checked if an element (which can be a file or a folder) with the same name exists in the other directory. In particular, through the function `access()` for files and `stat()` for folders. Hence, knowing that cannot coexist two elements with the same name in the same directory, if one directory has one or more files than the other, it will be catched and the variable `is_directory_equal` will be set to `false`. Since nowhere else is `is_directory_equal` set to true except in its definition, we can safely state that if a difference of this kind exists, the program will correctly identify it. \
**2.** When the first directory is scanned through (in the `while ((element = readdir(directory1)) != NULL)`), the following actions will be performed:
<ol>
<li> It is checked if a file with the same name exists in the second directory;</li>
<li>If it exists there, their content is compared through the functions `byte_by_byte_file_comparison()` or `hash_by_hash_file_comparison()`.</li>
</ol>
If one of these conditions fails, then `is_directory_equal` will be set to `false`.