Preliminaries -- The Technical Background -- On Programming -- Fundamentals -- Algorithm Extraction -- Recursion Removal -- Quantifications -- Refinement and Re-use -- Developments -- Sorting -- Data Refinement -- Sorting Revisited -- Failures and Fixes -- Further Examples -- On Interactive Software.Central to Formal Methods is the so-called Correctness Theorem which relates a specification to …