Partial correctness: The term-wise approach (Q793507): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/0167-6423(84)90017-0 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1963991971 / rank | |||
Normal rank |
Latest revision as of 23:28, 19 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Partial correctness: The term-wise approach |
scientific article |
Statements
Partial correctness: The term-wise approach (English)
0 references
1984
0 references
The first reason to consider the correctness of programs with respect to terms rather than predicates is a simple observation that the classical Hoare's logic, although complete, is too weak to specify programs. Even if we know that a command c is correct w.r.t. predicates \(n\geq 0\) and \(x=n!\) we still cannot claim that c computes factorials since c might update n instead (e.g. c might be: \(n:=0\); \(x:=1)\). A way out put forward in the paper is to allow \(\{t_ 1\}c\{t_ 2\}\) where \(t_ 1\) and \(t_ 2\) are terms, to mean the value of \(t_ 2\) after execution of c is, if defined, equal to the value of \(t_ 1\) before. Now \(\{\) n!\(\}\) \(c\{\) \(x\}\) means that c assigns to x the factorial of the initial value of n. The actual calculus of the term-wise correctness turns out very close to the classical Hoare's logic with the backward substitution (in terms) and the loop invariants (terms as well). The generalization onto procedures and functions is easier than is the case with the Hoare's logic. The paper gives the inference system which is sound and relatively complete.
0 references
term-wise correctness
0 references
applicative features
0 references
Hoare's logic
0 references
soundness
0 references
completeness
0 references