From 92ce471654e9735abb24b4fa51a129de8a1ed023 Mon Sep 17 00:00:00 2001 From: xfarrow Date: Fri, 21 Apr 2023 20:26:49 +0000 Subject: [PATCH] Updated Mathematical correctness of dircomp (markdown) --- Mathematical-correctness-of-dircomp.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathematical-correctness-of-dircomp.md b/Mathematical-correctness-of-dircomp.md index 5a2e8b5..55a2000 100644 --- a/Mathematical-correctness-of-dircomp.md +++ b/Mathematical-correctness-of-dircomp.md @@ -16,7 +16,7 @@ if
    ## 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: