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`. + +