xfarrow/dircomp
1
0
Fork 0
mirror of https://github.com/xfarrow/dircomp.git synced 2025-06-05 21:49:19 +02:00
Code Issues Packages Projects Releases Wiki Activity

Updated Mathematical correctness of dircomp (markdown)

xfarrow
2023-04-21 20:26:49 +00:00
parent 1a29ee9883
commit 92ce471654
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Mathematical-correctness-of-dircomp.md

@@ -16,7 +16,7 @@ if <ol>
## 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.
### Point 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. \
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.
### Point 2
When the first directory is scanned through (in the `while ((element = readdir(directory1)) != NULL)`), the following actions will be performed for each file: