A decomposition rule for the Hoare logic
type: Item
instance of: scholarly article
title: A decomposition rule for the Hoare logic
zbMATH Open document ID: 0635.68004
DOI: 10.1016/0020-0190(87)90006-8
author: Tadao Takaoka
published in: Information Processing Letters
publication date: 1987-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 4035105
zbMATH Keywords: program verification
zbMATH Keywords: Hoare logic
zbMATH Keywords: decomposition rule
zbMATH Keywords: complexity of theorem proving
MaRDI profile type: Publication
full work available at URL: 0020-0190(87)90006-8
OpenAlex ID: W2028808675
cites work: Q4174692
cites work: An axiomatic basis for computer programming
cites work: Automatic program verification. I: A logical basis and its implementation
cites work: Logical analysis of programs
description: scientific article; zbMATH DE number 4035105