Classical Floyd-Hoare logic is valid when total pre- and postconditions are considered. In the case of partial conditions (predicates) the logic becomes invalid. This situation may be corrected by introducing additional constraints for the rules of the logic. But such constraints, especially for the sequence and while rules, are rather complicated. In this paper we propose a new simpler sequence rule formulated in an extended program algebra. The same considerations also allow to reformulate the while rule. The obtained results can be useful for software verification.
The classical Floyd-Hoare logic [
Although in the classical Floyd-Hoare logic it is assumed that program may not terminate and its output may be undefined on a particular input d (f (d) is undefined), it is also assumed that the pre- and post-conditions p, q are predicates which are defined on all possible data , i.e. that they are total predicates.
Partiality of these predicates can arise naturally, if they are expressed using operations which can cause errors, nontermination, or non-well-defined behavior. For example, one may want to consider the Floyd-Hoare triple
{true} a[
In the literature [
To deal with this issue in the previous works [
Here a Floyd-Hoare triple {p}f {q} means that when the program’s input data d satisfies the pre-condition ( q(d) is defined and true), and the program terminates on d, and the post-condition is defined on the program’s output (the value q(f (d))), then the program’s output satisfies the post-condition ( q(f (d)) is true). We call this interpretation of a triple with partial pre- and post-conditions a weak Floyd-Hoare triple (the reason is that it does not require the post-condition to be defined, if the pre-condition is defined; one alternative is to require that the post-condition is defined whenever the pre-condition is defined which we call the strong Floyd-Hoare triple, but which we do not consider in this paper).
An important fact is that the classical inference system for the Floyd-Hoare
logic for the language WHILE [
R SEQ {p} f {q}, {q} g {r} where f • g denotes the sequential composition of programs f and g (i.e. g is runs after f on the result of f ).
This can be explained on the following simple example in Octave syntax. Suppose that n denotes an integer-valued variable. The expression zeros(n,1) evaluates to a n × 1 vector of zeros. If the variable a contains a vector, the expression length(a) evaluates to the length of a. The i-th (i=1,2,...) component can be accessed using the expression a(i) which raises an error, if the value of i is not a valid index, e.g. if the length of a is less than the value of i. Assignment is denoted as =, equality test is denoted as ==, and comparisons are denoted as >=, >. Then we can assume that the following are valid assertions (in the sense of weak Floyd-Hoare triples): {a(1)==0} m=length(a) {m>0}
We assume that in the first triple the post-condition is undefined, if the length of a is zero (a is empty), which happens if n is zero. However,
{n>=0} a=zeros(n,1); m=length(a) {m>0} is not a valid assertion (in sense of weak Floyd-Hoare triples), since if n is zero, then a is a zero-length vector (is empty) and m is zero.
Because of unsoundness of some rules of the classical inference system in
the presence of partial predicates, in [
R SEQ’ {p} f {q}, {q} g {r} , p |= P C(f • g, r)
{p} f • g {r}
where
– f • g denotes the function d 7→ g(f (d)) which is the result of sequential
composition of f and g;
– p |= q means that each interpretation of the formula ¬p ∨ q (p → q) never
takes a false value (i.e. it is always either true or undefined);
– P C is the Predicate transformer composition [
The presence of a complicated constraint, however, makes application of this rule dificult in all but the most trivial cases.
In this paper we propose an alternative unconstrained sequence rule for Floyd-Hoare logic with partial predicates based on extended program algebra which can be useful for software verification. 2
The symbol →˜ will denote partial functions and → will denote total functions (e.g. f : A →˜B means that f is a partial function on a set A with values in a set B; f : A → B means that f is a total function from A to B). We will use the symbol −n→ for partial functions with finite graph. For f : D→˜ D0: – f (d) ↓ denotes that f is defined on d ∈ D; – f (d) ↓= d0 denotes that f is defined on d ∈ D with a value d0 ∈ D0; – f (d) ↑ denotes that f is undefined on d ∈ D; – dom(f ) = {d ∈ D | f (d) ↓} is the domain of a function (note that there are diferent definitions of the domain of a partial function in diferent branches of mathematics); we use the convention from recursion theory).
The notation f1(d1) ∼= f2(d2) means the strong equality, i.e. that f1(d1) ↓ if and only if f2(d2) ↓, and if f1(d1) ↓, then f1(d1) = f2(d2).
Let D be a non-empty set. We will consider its elements mathematical models
of computer data (which is used as input or output for programs of interest).
An example of such models can be nominative sets [
We will consider partial functions from D to D (denoted as D→˜ D) as semantic models of sequential programs operating on such data.
Let f, g : D →˜D. Denote by f • g a function D→˜ D such that – (f • g)(d) = g(f (d)), if g(f (d)) is defined; – (f • g)(d) is undefined, otherwise.
We will call f • g the sequential composition of f and g.
Denote by T, F the logical values true and false.
We call partial functions from an arbitrary set X to Bool = {T, F } partial predicates on X.
Let p, q : D →˜Bool.
Denote by p ∨ q the partial predicate D→˜ Bool such that – (p ∨ q)(d) = T , if p(d) ↓= T (i.e. p(d) is defined and has the value T ), or if q(d) ↓= T ; – (p ∨ q)(d) = F , if p(d) ↓= F and q(d) ↓= F ; – (p ∨ q)(d) is undefined, otherwise.
Denote by p ∧ q the partial predicate D→˜ Bool such that – (p ∧ q)(d) = T , if p(d) ↓= T and q(d) ↓= T ; – (p ∧ q)(d) = F , if p(d) ↓= F or q(d) ↓= F ; – (p ∧ q)(d) is undefined, otherwise.
– (¬p)(d) = T , if p(d) ↓= F ; – (¬p)(d) = F , if p(d) ↓= T ; – (¬p)(d) is undefined, if p(d) is undefined.
Operations (compositions) ∨, ∧, and¬ are respectively disjunction,
conjunction, and negation operations on partial predicates. These operations are defined
according to the truth tables of Kleene’s strong logic of indeterminacy [
Denote by ∼ p the partial predicate D→˜ Bool such that – (∼ p)(d) = T , if p(d) is undefined; – (∼ p)(d) is undefined, if p(d) is defined.
It means that that we extend a program algebras, and in particular predicate algebra, with new operation ∼
.
Definition 1.
A semantic weak Floyd-Hoare triple is a tuple (p, f, q), where f : D →˜D0, p : D →˜Bool, q : D0→˜ Bool for some D, D0such that for each d ∈ D, if p(d) ↓= T and f (d) ↓ and q(f (d)) ↓, then q(f (d)) = T .
Then {p}f • g{r1 ∨ r2}.
– {p}f {q} means that (p, f, q) is a semantic weak Floyd-Hoare triple. Theorem 1. Assume that {p}f {q}, {q}g{r1}, and {∼ q}g{r2}. Proof. Let d ∈ D. Assume that p(d) ↓= T , (f •g)(d) ↓, and (r1 ∨r2)((f •g)(d)) ↓.
Then f (d) ↓ and g(f (d)) ↓. Denote d0 = f (d) and d00 = (f • g)(d) = g(f (d)). Let us show that (r1 ∨ r2)(d00) = T .
Suppose that (r1 ∨ r2)(d00) ↓= F . Then r1(d00) ↓= F and r2(d00) ↓= F . We have that either q(d0) ↓, or q(d0) ↑. tioned statement r1(d00) = F . { } { }
Consider the case when q(d0) ↓. Then q(f (d)) ↓, and since p(d) ↓= T and p f {q}, we have q(f (d)) = q(d0) = T . Then since r1(g(d0)) ∼= r1(d00) ↓ and q g{r1}, we have r1(g(d0)) = r1(d00) = T , but this contradicts the above menthe above mentioned statement r2(d00) = F .
Consider the case when q(d0) ↑. Then (∼ q)(d0) ↓= T . Then since r2(g(d0)) ∼= r2(d00) ↓ and {∼ q}g{r2}, we have r2(g(d0)) = r2(d00) = T , but this contradicts
In both cases we have a contradiction, so (r1 ∨ r2)(d00) ↓= F is impossible. But (r1 ∨r2)(d00) ∼= (r1 ∨r2)((f •g)(d)) ↓ by the assumption, so (r1 ∨r2)(d00) = T . tu
This result can be used as a semantic foundation of the following unconoperation on predicates): strained inference rule for sequential composition for the inference system for Floyd-Hoare logic with partial pre- and post-conditions (which involves the ∼ R USEQ R SSEQ {p} f {q}, {q} g {r1}, {∼ q}g{r2}
{p} f • g {r1 ∨ r2}
{p} f {q}, {q} g {r}, {∼ q}g{r}
In the special case of coinciding r1 and r2, it can be rewritten as:
Theorem 1 implies that addition of the rules R U SEQ and/or R SSEQ to
operation) does not change its soundness.
the inference system AC proposed in [
As an informal example, consider how these rules can be potentially applied in the case mentioned in the introduction: {a(1)==0} m=length(a) {m>0}.
These two assumptions alone are not suficient to establish the triple concerning the sequential composition. A missing piece of information is the triple describing the behavior of the instruction m=length(a) when the predicate (a(1)==0) is undefined. Under the interpretation assumed in Introduction, this undefinedness means that the attempt of evaluation of (a(1)==0) leads to an abnormal/error state. If a is a defined vector, this happens exactly when a has zero length (is empty). If a is undefined, then an attempt of evaluation of length(a) causes an error. Thus we can state that
{∼(a(1)==0)} m=length(a) {m=0}. where ∼ is not a part of Octave syntax, but just a notation to represent the statement that the expression (a(1)==0) is undefined (causing an abnormal/error state). Thus by the R U SEQ rule:
{n>=0} a=zeros(n,1); m=length(a) {m>0 ∨ m=0}.
Again, here ∨ is not a part of Octave syntax, but a notation to represent the disjunction of two predicates. 4
W H(r, f )(d) ↓= f (n)(d), if there exists an integer n ≥ 0 such that r(f (i)(d)) ↓= T for all i = 0, 1, ..., n − 1 and r(f (n)(d)) ↓= F , where f (i) denotes f • f • ... • f and f (0) is the identity | {iz } function on D (i.e. f (0)(d0) = d0 for all d0 ∈ D); and W H(r, f )(d) ↑, otherwise.
In [
In terms of W H the loop rule for the classical inference system for the
FloydHoare logic with total pre- and post-conditions [
{r ∧ p} f {p} R WH {p} W H(r, f ) {¬r ∧ p}
This rule, generally, is not valid in the case of partial pre- and post-conditions, but can be replaced with a constrained rule [18, p. 16] (R W H0) in this case.
Applying the approach which we used in the statement and proof of Theorem 1, we can propose an alternative unconstrained rule for the while loop which may be more convenient to apply.
Theorem 2. Assume {r ∧p}f {p}, {r ∧(∼ p)}f {p}. Then {p}W H(r, f ){¬r ∧p}. p)(W H(r, f )(d)) ↓.
Proof. Let d ∈ D. Assume that p(d) ↓= T , W H(r, f )(d) ↓= d0, and (¬r ∧
Let us show that (¬r ∧ p)(W H(r, f )(d)) = (¬r ∧ p)(d0) = T . that r(f (i)(d)) ↓= T for all i = 0, 1, ..., n − 1, and r(f (n)(d)) ↓= F , and From the definition on
d0 = W H(r, f )(d) = f (n)(d).
If n = 0, then d0 = d, so r(d0) ↓= F and p(d0) ↓= T , whence (¬r ∧ p)(d0) = T .
Let us show by induction on i ∈ {0, 1, ...} that if i ∈ {0, 1, ..., n − 1}, then p(f (i)(d)) ↓= T or p(f (i)(d)) ↑. because i < n. Denote d1 = f (i)(d).
Base of induction: p(f (0)(d)) ∼= p(d) ↓= T , so the statement holds.
Inductive step. Assume that i ∈ {0, 1, ..., n − 1}. Assume that p(f (i)(d)) ↓= T or p(f (i)(d)) ↑. Assume that i + 1 ∈ {0, 1, ..., n − 1}. Note that r(f (i)(d)) ↓= T
Consider the case p(f (i)(d)) ↓= T . Then since r(d1) ↓= T and p(d1) ↓= T , we have (r ∧ p)(d1) ↓= T . If p(f (d1)) ↓ , then since { r ∧ p}f {p}, we have p(f (i+1)(d)) ∼= p(f (d1)) ↓= p(f (i+1)(d)) ↓= T , or p(f (i+1)(d)) ↑ holds.
Consider the case p(f (i)(d)) ↑. Then p(d1) ↑ and r(d1) ↓= T . Then (∼ p)(d1) ↓= T , so (r ∧ (∼ p))(d1) ↓= T . Then since { either p(f (i+1)(d)) ∼= p(f (d1)) ↓= T , or p(f (i+1)(d)) ∼= p(f (d1)) ↑. r ∧ (∼ p)}f {p}, we have In both cases p(f (i+1)(d)) ↓= T or p(f (i+1)(d)) ↑, so the inductive step is
completed. p(f (n)(d)) ↓.
Since n ≥ 1 by our assumption, the proven statement implies that either p(f (n−1)(d)) ↓= T , or p(f (n−1)(d)) ↑
. We have (¬r ∧ p)(f (n)(d)) ∼= (¬r ∧ p)(W H(r, f )(d)) ↓. Moreover, r(f (n)(d)) ↓= F , so (¬r)(f (n)(d)) ↓= T , whence we have p(f (n)(d)) = T .
Consider the case p(f (n−1)(d)) ↓= T . We have r(f (n−1)(d)) ↓= T , so (r ∧ p)(f (n−1)(d)) ↓= T . Then since {r ∧ p}f {p} and p(f (f (n−1)(d))) ∼= p(f (n)(d)) ↓, (r ∧ (∼ p))(f (n−1)(d)) ↓= T . Then because { p(f (f (n−1)(d))) ∼= p(f (n)(d)) ↓, we have p(f (n)(d)) = T . (∼ p)(f (n−1)(d)) ↓= T . Moreover, we have r(f (n−1)(d)) ↓= T , whence Consider the case p(f (n−1)(d)) ↑. Then because f (n−1)(d) ↓, we have r ∧ (∼ p)}f {p} and, moreover, (¬r ∧ p)(W H(r, f )(d)) ∼= (¬r ∧ p)(f (n)(d)) ↓= T .
In both cases we have p(f (n)(d)) = T . Since r(f (n)(d)) ↓= F , we have tu
This result can be used as a semantic foundation of the following unconstrained inference rule (for the case of partial pre- and post-conditions): R UWH {r ∧ p} f {p}, {r ∧ (∼ p)}f {p}
{p} W H(r, f ) {¬r ∧ p} 5
We have proposed modifications of the inference system for an extension of the
classical Floyd-Hoare logic to the case of partial pre- and post-conditions and
partial programs proposed in [
In the future we plan to make detailed comparison of inference systems and propose new modifications to improve their eficiency.