# Homework 4
by Rachel Eron eronx001, Samuel Fountain fount032, Thomas Fredrickson fredr349, Griffin Higley higle018

## Problem 1
### a)

Assume that there is a value that corresponds to the key given in the input for the binarySearch function. Also assume that both the dictKeys and dictValues are sorted so that index i in each array will map the key[i] -> val[i]. Also assume that dictValues is sorted.

Observe that dictValues and key do not change in the program. Now as the program starts execution inorder for the program to execute line 27, the while loop needs to be executed. This means that high must be >= low. ie dictSize >= 1.

based on the comparison the program has three states it could be in.
* a) The value at dictValue[mid] is > key. In which case the search space in truncated to the lower half of the array
* b) The value at dictValue[mid] is < key. In which case the search scace is truncated to the upper half of the array
* c) The value at dictValue[mid] is == key. In which case we have found the key had line 27 is executed returning the key -> value

If the program is in either state a) or in state b) the program will loop again. The same checks will be ran and either state a), b), or c) will be the outcome. This loop will run until low = high which case the outcome will be state c) based on our assumption. This is because this value is the only value left to check in the array and there for must be the value we are looking for.

So logically the postcondition of line 18 with the comparison is

mid = M ^ comparison = C

For line 27 to execute the condition on line 19 must be false, which would cause the post condition

mid = M ^ comparison = C ^ ¬(C < 0)

Additionally line 22 must execute to false, causing the post condition

mid = M ^ comparison = C ^ ¬(C < 0) ^ ¬(C > 0) 

Therefore the pre condition of line 25 is

mid = M ^ comparison = C ^ ¬(C < 0) ^ ¬(C > 0) 

and

¬(C < 0) ^ ¬(C > 0) implies (C=0)

and

(C = 0) implies that mid = key

Therefore the statment return dictValues[mid] at line 27 always returns the value of the input key.

### b)
#### Pre Condition
low = L ^ high = H ^ mid = M ^ comparison = C
#### Post-condition (if statment line 1)
low = L ^ high = H ^ mid = M ^ comparison = C ^ ¬(C <0)
#### Post-condition (if statment line 5)
low = L ^ high = H ^ mid = M ^ comparison = C ^ ¬(C <0) ^ ¬(C > 0)
#### Post-condition (if statment line 9)
low = L ^ high = H ^ mid = M ^ comparison = C ^ ¬(C <0) ^ ¬(C > 0) ^ ¬(C = 0)

#### Conclusion
The final post-condition is low = L ^ high = H ^ mid = M ^ comparison = C ^ ¬(C <0) ^ ¬(C > 0) ^ ¬(C = 0). This final state is not possible. This is because C is an integer. So assuming ¬(C <0) ^ ¬(C > 0), we know C is equal to 0 because ¬(C > 0) ^ ¬(C < 0) implies c = 0. The property of the comparison relation (<) needed to complete the proof was the antisymmetric relation.
### c)
#### Pre-Condition
``
n = N ^ a = A ^ len(N) = A
``
#### Post-Condition
`` c
len(N) = A ^ n = 1 ^ v = Sum from N to n (1) when (d*(a[n]-a[n-1]) < 0 ^ D = d ^(D > 0 ∨ D < 0 ∨ D = 0)
``
## Problem 2
### a)
| Number of Element | Weights | Output | Log File |
|-------------------|-----------|-------------------------------|-------------------------|
| 3 | 2 2 2 | 3 2 1 1 1 | log-E_3-W_2_2_2.txt |
| 3 | 3 1 1 | 3 2 1 3 2 1 | log-E_3-W_3_1_1.txt |
| 4 | 1 2 4 4 | 4 3 2 4 3 1 4 3 2 4 3 | log-E_5-W_1_2_4_4.txt |
| 5 | 3 4 1 2 5 | 5 4 3 2 5 1 2 5 1 2 5 4 1 2 5 | log-E_5-W_3_4_1_2_5.txt |
### b)
<img src="https://latex.codecogs.com/gif.latex?psums[n]&space;\equiv&space;\sum_{i=0}^{n}counts[n]" title="psums[n] \equiv \sum_{i=0}^{n}counts[n]" />

### c)
<img src="https://latex.codecogs.com/gif.latex?counts[top]&space;\leq&space;psum[x]*cur\_counts&space;\;&space;\forall&space;x&space;\in&space;range(top,num\_elems-1)\wedge&space;psums[n]&space;=&space;\sum_{i=0}^{n}counts[n]&space;\;&space;\forall&space;n&space;\in&space;range(0,num\_elems)" title="counts[top] \leq psum[x]*cur\_counts \; \forall x \in range(top,num\_elems-1)\wedge psums[n] = \sum_{i=0}^{n}counts[n] \; \forall n \in range(0,num\_elems)" />

#include <stdio.h>
#include <stdlib.h>

#define SWAP(a, b)                                                             \
  {                                                                            \
    int _tmp = a;                                                              \
    a = b;                                                                     \
    b = _tmp;                                                                  \
  }

int cur_count = 0, alloc_count = 0, total_count = 0, num_elems = 0;

int *counts, *psums, *elems;

char *fname = "./log.txt";

void recordData();
void write_array(char *array_name, int *lst, FILE *file);

void initialize(int n, FILE *fptr) {
  int i = 0;

  num_elems = n;
  counts = (int *)calloc(n, sizeof(int));
  psums = (int *)calloc(n, sizeof(int));
  elems = (int *)calloc(n, sizeof(int));
  for (i = 0; i < n; ++i) {
    elems[i] = i + 1;
    fscanf(fptr, "%d", &counts[i]);
    psums[i] = total_count += counts[i];
  }
  recordData();
}

int next_elem() {
  int top = num_elems - 1;
  int ret = elems[top];

  if (alloc_count >= total_count)
    return 0;

  ++alloc_count;
  ++cur_count;
  --psums[top];
  --counts[top];
  while (top > 0 && counts[top] <= (cur_count * psums[top - 1])) {
    psums[top - 1] += (counts[top] - counts[top - 1]);
    SWAP(counts[top], counts[top - 1]);
    SWAP(elems[top], elems[top - 1]);
    --top;
  }

  if (top != num_elems - 1)
    cur_count = 0;
  recordData();
  return ret;
}

void setupRecordData() {
  FILE *file = fopen(fname, "w");
  if (file == NULL)
    exit(1);
  fclose(file);
}

void recordData() {
  FILE *file = fopen(fname, "a");
  int i;

  fputs("------------------------------\n", file);
  write_array("counts", counts, file);
  write_array("psums", psums, file);
  //  write_array("elems", elems, file);
  fclose(file);
}

void write_array(char *array_name, int *lst, FILE *file) {
  int i = 0;
  fprintf(file, "%-6s = ", array_name);
  while (i < num_elems) {
    fprintf(file, "%4i ", lst[i]);
    ++i;
  }
  fputs("\n", file);
  return;
}

int main() {
  int next;
  setupRecordData();
  printf("number of elements: ");
  scanf("%d", &num_elems);
  printf("\nweights:\n");
  initialize(num_elems, stdin);
  printf("\n");

  while ((next = next_elem()) > 0)
    printf("%d ", next);
  printf("\n");
}