Verifikation von funktionalen Programmen

Beweisen Sie:

append ist assoziativ
reverse ( reverse xs ) == xs

Beweis-Methoden:

• Term-Umformungen (= equational reasoning)

  Ersetzung von äquivalenten Teiltermen

• Induktion
  • Induktions-Anfang (bei Listen: Nil)
  • Induktions-Schritt (bei Listen: Cons)

d. h. genauso wie in der Mathematik