Algorithms and correctness
Algorithmic problem
An algorithmic problem is described by:
- a set of feasible inputs.
- for each input a set of feasible outputs;
- 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
- An algorithm is associated with an algorithmic problem.
- An algorithm is a sequence of instructions how to compute a feasible output for a given input.
- 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:
- in case of minimization: a low objective function value are favored;
- in case of maximization: a high objective function value are favored.
Iterative and recursive algorithms
- Basically, a non-trivial algorithm is a loop or recursion plus some preprocessing and/or postprocessing.
- If an algorithm consists of several loops/recursions that are
nested loops/recursions
Correctness
An algorithm is correct if three conditions are fulfilled for every feasible input:
- All operations are well-defined. For example, access to an array component outside the array's index range and
- Each loop and recursion terminates regularly, that is, the break condition is fulfilled after a finite number of operations.
- The output delivered by the algorithm is a feasible output for the given input.
Invariant
- The invariant of a loop is a set of statements, which are fulfilled immediately before the first iteration, immediately after the last iteration, and between two iterations.
- The invariant of a recursion is a set of statements, which are fulfilled immediately after
- after preprocessing Maintenance of the
Remarks:
- 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.
- Important for tests!
Variant
Remarks:
- 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.
- Important for tests
Correctness proofs
- 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.
- The invariant
'Remark: for complexity the number of iterations bounded.