Combinatorial objects have configurations which can be enumerated by algorithms, but especially for imperative programs, it is difficult to find out if they produce the correct output and don’t generate duplicates. Therefore, for some of the most common combinatorial objects, namely n_Sequences, n_Permutations, n_Subsets, Powerset, Integer_Compositions, Integer_Partitions, Weak_Integer_Compositions and Trees, this thesis formalizes efficient functional programs and verifies their correctness with help of the interactive theorem prover Isabelle. In addition, for some combinatorial structures the enumeration function is then used to show the structure’s cardinality.     «

Combinatorial objects have configurations which can be enumerated by algorithms, but especially for imperative programs, it is difficult to find out if they produce the correct output and don’t generate duplicates. Therefore, for some of the most common combinatorial objects, namely n_Sequences, n_Permutations, n_Subsets, Powerset, Integer_Compositions, Integer_Partitions, Weak_Integer_Compositions and Trees, this thesis formalizes efficient functional programs and verifies their correctness...     »

Kombinatorische Objekte haben Konfigurationen, welche von Algorithmen enumeriert werden können, aber insbesondere für imperative Programme ist es schwierig herauszufinden, ob sie das richtige Ergebnis liefern und keine Duplikate erzeugen. Daher werden in dieser Arbeit für einige der geläufigsten kombinatorischen Objekte, nämlich n_Sequences, n_Permutations, n_Subsets, Powerset, Integer_Compositions, Integer_Partitions, Weak_Integer_Compositions and Trees, effiziente funktionale Programme formalisiert und dessen Korrektheit mit Hilfe des des interaktiven Theorembeweisers Isabelle verifiziert. Darüber hinaus wird für einige der kombinatorischen Strukturen die Kardinalität mithilfe der jeweiligen Aufzählungsfunktion bewiesen.      «

Kombinatorische Objekte haben Konfigurationen, welche von Algorithmen enumeriert werden können, aber insbesondere für imperative Programme ist es schwierig herauszufinden, ob sie das richtige Ergebnis liefern und keine Duplikate erzeugen. Daher werden in dieser Arbeit für einige der geläufigsten kombinatorischen Objekte, nämlich n_Sequences, n_Permutations, n_Subsets, Powerset, Integer_Compositions, Integer_Partitions, Weak_Integer_Compositions and Trees, effiziente funktionale Programme...     »