Formalization and Validation of Fundamental Sequence Algorithms by Computer-assisted Checking of Finite Models

While common textbooks go into great details when it comes to the analy- sis of sequence algorithms, they lack in proper proofs and moreover formal specifications. The most essential part, the loop invariant is either described very vaguely or is completely missing. This thesis gives those missing spec- ifications as well as so called verification conditions upon which one can fully prove an algorithm. Normally such a process is very difficult and it is easy to wrongly specify an algorithm. With the help of the RISC Algorithm Language (RISCAL), developed at the Research Institute for Symbolic Com- putation (RISC), this process is simpler as this system provides additional checks that help noticing early if a specification is wrong. It uses finite model checking, which makes it possible to check the adequacy of speci- fications even if they include general quantifiers, which would be difficult infinite models. The result of the thesis is a collection of specifications for various search- ing and sorting algorithms. The algorithms are implemented for different data types (array, recursive lists, pointer-linked lists) to serve as an addition to common textbooks.