Weakest Preconditions and Cumulative Subgoal Fulfillment: A Comparison

TL;DR

This paper compares the weakest preconditions method with the cumulative subgoal fulfillment approach for constructing correct procedures, illustrating their differences through an example and demonstrating the CSF process.

Contribution

It provides a comparative analysis of weakest preconditions and CSF, highlighting their respective methodologies with a practical example.

Findings

CSF offers an alternative to weakest preconditions in program construction.

The paper demonstrates the CSF process step-by-step.

An example illustrates the differences between the two approaches.

Abstract

We contrast the use of weakest preconditions for the correct construction of procedures with the cumulative subgoal fulfillment (CSF) approach. An example of Cohen and Monin is used for this purpose. The CSF construction process is demonstrated.