From 40d365eed6fbfdd1d9662f69f1afb82905c89032 Mon Sep 17 00:00:00 2001 From: xfarrow Date: Fri, 21 Apr 2023 19:55:49 +0000 Subject: [PATCH] Proved point 1-2 out of 4 --- Home.md | 1 - Mathematical-correctness-of-dircomp.md | 29 ++++++++++++++++++++++++++ 2 files changed, 29 insertions(+), 1 deletion(-) delete mode 100644 Home.md create mode 100644 Mathematical-correctness-of-dircomp.md diff --git a/Home.md b/Home.md deleted file mode 100644 index 243c34f..0000000 --- a/Home.md +++ /dev/null @@ -1 +0,0 @@ -Welcome to the dircomp wiki! diff --git a/Mathematical-correctness-of-dircomp.md b/Mathematical-correctness-of-dircomp.md new file mode 100644 index 0000000..1d229c1 --- /dev/null +++ b/Mathematical-correctness-of-dircomp.md @@ -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
    +
  1. they have the same name, including extension;
    2. +
  2. they have the same content;
    3. +
+ +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: +
    +
  1. It is checked if a file with the same name exists in the second directory;
    2. +
  2. If it exists there, their content is compared through the functions `byte_by_byte_file_comparison()` or `hash_by_hash_file_comparison()`.
    3. +
+ +If one of these conditions fails, then `is_directory_equal` will be set to `false`. + +