# Quality Assurance Assignment 3
Group 22

This is just a empty example file to illustrate how a report could look like.
You do not need to use Markdown, use whatever you like, but in the end you must hand in a PDF file, and make sure that the oracle can be copy/pasted from your report to PathCrawler without problems.

## Theory Questions
**1. What is an oracle? Why don't we just use algorithm under test as an oracle?**

With an oracle you can test the behaviour and the output of a program in a test for different test cases, so the oracle decides, whether the software, which is being tested, behaves as expected.

Using algorithm under test would specify exact areas to test where an oracle is able to test specified critical regions with conditions that might be missed by an algorithm.

**2. What is the difference between concolic and symbolic execution? Explain it using the example.**

Concolic execution:
* concrete + symbolic execution
* in additon to symbolic values, variables also have real (concrete) values (so it is possible to test inaccessible paths and black-box components)
* executed in several iterations

Symbolic execution:
* parameters become symbolic instead of concrete values
* at the end, you can insert real values instead of the symbolic values and a proof of correctness (Korrektheitsbeweis) can be executed
* with path condition you can decide which if-branch will be executed
* unreachable paths cannot be tested
* white-box testing

**3. What are the advantages of concolic execution over random testing?**

In concolic execution, you can determine the region which should be tested and the start of the execution will also have a random input. That is not possible in random testing.
Covering all branches does not mean that the program doesn’t have any bugs. Things like condition coverage and modified condition / decision coverage exist because of this. You need to ensure that all possible inputs are handled correctly by the code, which is a much harder problem than traversing all branches (e.g. which can be done by random testing).

**4. Explain why loops are problematic and how they are dealt with in concolic execution?**

A symbolic execution with loops does not provide any evidence.
The concolic execution itself is a loop with several iterations. The path-conditions (which specifies exactly one path through the program) will be noticed and if no input for other conditions has been found (all conditions has been covered), the execution will be stopped. A program with loop(s) could have an infinite amount of paths.

**5. Is concolic execution white-box or black-box testing and why?**
Concolic execution is white-box and black-box testing. In addition to symbolic values which requires the source code (white-box testing), variables also have real values. It makes possible to test inaccessible paths (where you don't have access to the code, but test the behaviour of the function) and black-box components.

**6. Which bugs cannot be caught with concolic execution? _(Bonus)_**

For example, bugs in multithreaded applications may not be found.

## PathCrawler Online

### fibonacci()

**Variable domains:**
* 1 ≤ dim(output) ≤ 100
* 1 ≤ n ≤ 100

**Unquantified preconditions:**
* n == dim(output)

**Oracle:**

void oracle_fibonacci(
  int Pre_n, int n, 
  int *Pre_output, int *output)
{
  if (Pre_n != n) 
  {
    pathcrawler_verdict_failure();
    return; 
  }
    
  for (int i = 1; i < n; i++) 
  {
    if (output[i] < output[i-1]) 
    {
      pathcrawler_verdict_failure();
      return;
    }
    if (i < n-1) 
    {
      if (output[i-1] + output[i] != output[i+1]) 
      {
        pathcrawler_verdict_failure();
        return;
      }
    }
  }
  
  pathcrawler_verdict_success();
}

**Correct**: No, mutant.

**Bug**:
We found the bug using PathCrawler as soon as `n ≥ 3`, because then we can check if `output[n+1] = output[n] + output[n-1]`, but this condition does not hold because `output[0]` is always zero, `output[1]` is always 1 and `output[2]` is always 2.
However, this behaviour is not correct according the Fibonacci number series, since `0+1≠2`.

### lcm()

**Variable domains:**
* 1 ≤ a ≤ 1000
* 1 ≤ b ≤ 1000

**Oracle:**

void oracle_lcm(
  int Pre_a, int a, 
  int Pre_b, int b, 
  int pathcrawler__retres__lcm)
{

  if (Pre_a != a)
  {
    pathcrawler_verdict_failure();
    return;
  }
  if (Pre_b != b)
  {
    pathcrawler_verdict_failure();
    return;
  }

  if (a == b)
  {
    if (pathcrawler__retres__lcm != a || pathcrawler__retres__lcm != b)
    {
      pathcrawler_verdict_failure();
      return;
    }
  }

  if(pathcrawler__retres__lcm < a || pathcrawler__retres__lcm < b)
  {
    pathcrawler_verdict_failure();
    return;
  }
 
 pathcrawler_verdict_success();
}

**Correct**: Yes, correct.

**Bug**:
–

### intersection()
**Array domains:**
* -20 <= array2[INDEX_0] <= 20
* -20 <= array1[INDEX_0] <= 20

**Variable domains:**
* 1 <= dim(output_length) <= 1
* 50 <= dim(output) <= 50
* 0 <= l2 <= 50
* 0 <= l1 <= 50
* 0 <= dim(array2) <= 50
* 0 <= dim(array1) <= 50

**Unquantified preconditions:**
* l1 == dim(array1)
* l2 == dim(array2)

**Oracle:**

void oracle_intersection(
  int *Pre_array1, int *array1, 
  int *Pre_array2, int *array2, 
  int Pre_l1, int l1, 
  int Pre_l2, int l2, 
  int *Pre_output, int *output, 
  int *Pre_output_length, int *output_length)
{
  if (Pre_l1 != l1)
  {
    pathcrawler_verdict_failure();
    return;
  }
  if (Pre_l2 != l2)
  {
    pathcrawler_verdict_failure();
    return;
  }

  for (int i = 0; i < l1; i++)
  {
    if (Pre_array1[i] != array1[i])
    {
      pathcrawler_verdict_failure();
      return;
    }
  }

  for (int i = 0; i < l2; i++)
  {
    if (Pre_array2[i] != array2[i])
    {
      pathcrawler_verdict_failure();
      return;
    }
  }

  if (*output_length < 0)
  {
    pathcrawler_verdict_failure();
    return;
  }

  
  for (int i = 0; i < *output_length; i++)
  {
    int found = 0;
	for (int j = 0; j < l1; j++)
    {
      if (output[i] == array1[j])
      {
        found = 1;
      }
    }
    if (found == 0)
    {
      pathcrawler_verdict_failure();
      return;
    }
    
    found = 0;
    for (int j = 0; j < l2; j++)
    {
      if (output[i] == array2[j])
      {
        found = 1;
      }
    }
    if (found == 0)
    {
      pathcrawler_verdict_failure();
      return;
    }
  }

  pathcrawler_verdict_success();
}

**Correct**: Yes, correct.

**Bug**:
–

### sort()
**Array domains:**
* -500 ≤ array[INDEX_0] ≤ 500

**Variable domains:**
* 0 ≤ n ≤ 500
* 0 ≤ dim(array) ≤ 500

**Unquantified preconditions:**
* n == dim(array)

**Oracle:**

void oracle_sort(
  int *Pre_array, int *array, 
  int Pre_n, int n)
{
  if (Pre_n != n)
  {
    pathcrawler_verdict_failure();
    return;
  }

  for(int i = 1; i < n; i++)
  {
    if(array[i] > array[i-1])
    {
      pathcrawler_verdict_failure();
      return;
    }
  }

  pathcrawler_verdict_success();
}

**Correct**: Yes, correct.

**Bug**:
–

### contains() (BONUS)
**Array domains:**
* 0 ≤ array[INDEX_0] ≤ 1

**Variable domains:**
* 0 ≤ x ≤ 1

**Unquantified preconditions:**
* x == y

**Quantified preconditions:**
* TODO: Remove this -> ∀ A : A ≥ 0 ⇒ array[A] ≥ array[2 * A]

**Oracle:**

void oracle_contains() {
}

**Correct**: Yes, correct.|No, mutant.

**Bug**:
Description of the bug, and how you found it using PathCrawler.