af algoritmer. Metoderne er baseret på brug af formelle specifikationer af algoritmernes funktion samt prædikattransformeren "Den svageste Præbetingelse" (weakest precondition). Selv om man i praksis ikke ønsker at benytte formalismen, hjælper bogens metoder med til at skabe gode arbejdsformer, når man udvikler programmer. Således opnås der større sikkerhed for, at programmerne fungerer korrekt, dvs. i overensstemmelse med specifikationerne.