Beispiel Denotationale Semantik

monoton :: Ord a => [a] -> Bool
monoton (x : y : zs) = 
    x <= y && monoton (y:zs)
monoton  _ = True

merge :: Ord a => [a] -> [a] -> [a]
merge [] ys = ys ; merge xs [] = xs
merge (x:xs) (y:ys) = 
    if x <= y then x : merge ... ...
              else ...

Behauptung: ∀ xs, ys: monoton xs && monoton ys ⇒ monoton (merge xs ys)

Beweis: Indukt. über length xs + length ys