A decomposition rule for the Hoare logic (Q1097683): Difference between revisions

The complexity of program verification by the Hoare logic grows rapidly as the length of the program to be proved increases. This paper presents a mechanism, called a decomposition rule, which reduces the complexity of theorem proving in the program verification. The rule is simple and easy to use when the precondition for the program can be decomposed into several conditions. The meaning of the Hoare triple \(\{\) \(P\}\) \(S\{\) \(Q\}\) is that if P is true before program S, then Q is true after S is executed provided that S terminates. We can derive the following shift rule, provided that Q is not affected by executing S, \[ \frac{\{P\wedge Q\}S\{R\}}{\{P\}S\{Q\supset R\}}. \] From this rule, we can derive the decomposition rule, \[ \frac{\{P\wedge P_ 1\}S\{Q_ 1\},\quad \{P\wedge P_ 2\}S\{Q_ 2\}}{\{P\}S\{(P_ 1\supset Q_ 1)\wedge (P_ 2\supset Q_ 2)\}} \] provided that neither of \(P_ 1\) and \(P_ 2\) is affected by S. The meaning of this rule is that by decomposing the verification into two parts of \(\{P\wedge P_ 1\}S\{Q_ 1\}\) and \(\{P\wedge P_ 2\}S\{Q_ 2\}\), we can have a rather complicated postcondition \((P_ 1\supset Q_ 1)\wedge (P_ 2\supset Q_ 2)\). An illustrative example of program by this rule is given.