Weakest preconditions and cumulative subgoal fulfillment

• We discuss the use of weakest preconditions with the cumulative subgoal fulfillment (CSF) approach.
• We use an example of Cohen and Monin for this contrast.
• We show how the CSF process makes correctness integral with program construction.
• We show how CSF produces the Cohen/Monin program as well as an additional O(n)O(n) solution.
• We show how CSF yields O(logn) solutions.

“Cumulative subgoal fulfillment” (CSF) is a method for the construction of correct algorithms. We show how it formalizes and extends work of Dijkstra, Gries, and others to create loops by accumulating loop invariants. CSF's relationship with weakest preconditions is explored. An example of Cohen and Monin is used as illustration.