Algorithms and correctness

Algorithmic problem

An algorithmic problem is described by:

1. a set of feasible inputs.
2. for each input a set of feasible outputs;
3. optionally, an objective function, which assigns a real number to each feasible solution (the quality of the feasible solution). If an objective function is specified, it is also specified whether the objective function is to be minimized or to be maximized.

Operations and instructions

A programming languages offers a possibility to specify instructions (a.k.a. statements). An instruction specifies a sequence of operations; executing the machine amounts to executing this sequence of operations.

Algorithm

1. An algorithm is associated with an algorithmic problem.
2. An algorithm is a sequence of instructions how to compute a feasible output for a given input.
3. If an objective function is given, the objective function value of the generated solution is a criterion for the quality of an algorithm. More specifically:
   1. in case of minimization: a low objective function value is favored;
   2. in case of maximization: a high objective function value is favored.

Iterative and recursive algorithms

1. Basically, a non-trivial algorithm is a loop or recursion plus some preprocessing and/or postprocessing.
2. If an algorithm consists of several loops/recursions that are executed strictly after each other, it may be viewed as two algorithms that are executed after each other.
3. An iteration of a loop may contain another loop or recursion. Analogously, a recursive call may contain another loop or recursion. We say that a loop/recurions inside a loop/recursions is nested or the inner loop/recursion. The nesting loop/recursion is the outer one.

Remark:

1. Clearly, a loop may be transformed into a recursion and vice versa. So, every algorithm may be formulated either as a loop or as a recursion. However, in most cases, one of these two options looks simpler and "more natural" than the other one.
2. Formulating an algorithm as a loop might be favorable in many cases because a loop allows more control than a recursion. More specifically, a loop may be implemented as an iterator whose method for going one step forward implements the execution of one iteration of the loop. Such an implementation allows to terminate the loop early, to suspend execution and resume execution later on, and to execute some additional instructions between two iterations (e.g. for visualization or for testing).

Correctness

An algorithm is correct if three conditions are fulfilled for every feasible input:

1. All operations are well-defined. For example, access to an array component outside the array's index range and
2. Each loop and recursion terminates regularly, that is, the break condition is fulfilled after a finite number of operations.
3. The output delivered by the algorithm is a feasible output for the given input.

Invariant

1. The invariant of a loop consists of all assertions that are true immediately before the first iteration, immediately after the last iteration, and between two iterations. These assertions are called the invariant assertions of this loop.
2. The invariant of a recursion consists of all assertions that are fulfilled immediately after each recursive call. These assertions are called the invariant assertions of this recursion.

Remarks:

1. The invariant of an algorithm has a specific function in the correctness proof for the algorithm. Typically, in a documentation, only those invariant assertions are stated that are relevant for this purpose.
2. The invariant is also essential for testing purposes: a white-box test of a loop/recursion should definitely check maintenance of all relevant invariant assertions.

Variant

Remarks:

1. The invariant has a specific function in the correctness proof for the algorithm. It should contain all statements relevant for this purpose. It should contain no further statements unless there is a good reason for that.
2. Important for tests

Correctness proofs

1. The variant must be specified in a way that allows to conclude that the break condition will be fulfilled after a finite number of iterations.
2. The invariant

'Remark: for complexity the number of iterations bounded.