=Paper=
{{Paper
|id=Vol-2104/paper_259
|storemode=property
|title=On the Sequence Rule for the Floyd-Hoare Logic with Partial Pre- and Post-Conditions
|pdfUrl=https://ceur-ws.org/Vol-2104/paper_259.pdf
|volume=Vol-2104
|authors=Ievgen Ivanov,Mykola Nikitchenko
|dblpUrl=https://dblp.org/rec/conf/icteri/IvanovN18
}}
==On the Sequence Rule for the Floyd-Hoare Logic with Partial Pre- and Post-Conditions==
https://ceur-ws.org/Vol-2104/paper_259.pdf
On the Sequence Rule for the Floyd-Hoare Logic
with Partial Pre- and Post-Conditions
Ievgen Ivanov, Mykola Nikitchenko
Taras Shevchenko National University of Kyiv
64/13, Volodymyrska Street, 01601 Kyiv, Ukraine
ivanov.eugen@gmail.com, nikitchenko@unicyb.kiev.ua
Abstract. Classical Floyd-Hoare logic is valid when total pre- and post-
conditions 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.
Keywords. Formal methods, software verification, Floyd-Hoare logic.
1 Introduction
The classical Floyd-Hoare logic [1–3] is a useful tool for proving partial cor-
rectness of sequential programs. It is based on properties of Floyd-Hoare triples
(assersions) of the form {p}f {q} which consists of pre- and post-conditions p,
q (predicates) and a program f . This assersion is treated in the following way:
when the program’s input data d satisfies the pre-condition (q(d) is true), and
the program terminates on d, the program’s output (the value f (d)) satisfies the
post-condition (q(d) is true).
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[1]:=0 {a[1]=0}
where a[1]:=0 denotes the operation of assignment of the value 0 to the 1-st
element of the array (or a more sophisticated key-value map) a, and a[1]=0 is a
predicate stating that the 1-st element of a is zero. Logically, it makes sense to
consider the latter predicate (the truth value of which depends on the content
of a) as partial and assume that it is defined only when a has an element with
index/key 1 (e.g. it is undefined, when a has no content). Note that depending on
the rules of the programming language, the assignment operation may be always
well-defined (e.g. if the assignment a[1]:=0 automatically allocates the space for
the new value, if it is not allocated), but the post-condition predicate may be
formally partial, because extraction from a is not always defined in the sense that
it causes an error or other types of abnormal behavior. In particular, a situation
of this kind occurs in Matlab [4] and Octave [5] languages for element insertion
and extraction operations for vectors (these languages and the corresponding
environments are widely used in scientific computing).
In the literature [6] one finds discussions of the ways of emulating partial
predicates and functions in software specifications using total predicates and/or
functions, however, almost all approaches which try to avoid partiality have some
drawbacks which are described in [7, 6, 8].
To deal with this issue in the previous works [9, 10] extensions of the classical
Floyd-Hoare logic which allowed one to reason about partial correctness of se-
quential programs using Floyd-Hoare triples consisting of both partial programs
and partial pre- and post-conditions were investigated.
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 termi-
nates 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 [11] is not sound in the presence of partial pre-
and post-conditions [9]. One reason of this is unsoundness of the sequence rule
when p, q, r are partial predicates:
{p} f {q}, {q} g {r}
R SEQ {p} f • 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 ex-
pression 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):
{n>=0} a=zeros(n,1) {a(1)==0}
{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 [9] a new inference system for an extended
Floyd-Hoare logic with partial pre-and post-conditions for a similar language was
proposed. Besides a few other modifications, in this system the regular sequence
rule was replaced with the following constrained sequence rule:
{p} f {q}, {q} g {r}
R SEQ’ , 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 [10] such that P C(f, q) is a
partial predicate r such that for any data d, r(d) = q(f (d)), if f (d) (i.e.
program value) and q(f (d)) (i.e. the value of the predicate q on the result
of f on data d) are defined, and r(d) is undefined otherwise (i.e. if f (d) or
q(f (d)) are undefined).
The presence of a complicated constraint, however, makes application of this
rule difficult 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 Notation
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
n
˜ 0:
symbol −→ for partial functions with finite graph. For f : D→D
– 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
different definitions of the domain of a partial function in different 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 ).
3 Constructing New Sequence Rule
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 [12, 13] (which are partial
assignments of values to variable names) or nominative data [12–15] (which
can be thought of as hierarchically constructed, nested nominative sets). The
latter ones can be used to represent many forms of data commonly used in
programming (e.g. multidimensional arrays, lists, trees, etc.) [12].
We will consider partial functions from D to D (denoted as D→D) ˜ as se-
mantic 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.
Denote by ¬p the partial predicate D→Bool
˜ such that
– (¬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, conjunc-
tion, and negation operations on partial predicates. These operations are defined
according to the truth tables of Kleene’s strong logic of indeterminacy [16]. The
set of all partial predicates on D together with these operations forms a Kleene
algebra (a De Morgan algebra which satisfies the normality axiom) [17].
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→D˜ 0 , p : D→Bool,
˜ q : D0 →Bool
˜ for some D, D 0 such that
for each d ∈ D, if p(d) ↓= T and f (d) ↓ and q(f (d)) ↓, then q(f (d)) = T .
We will use the following notation:
– {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 }.
Then {p}f • g{r1 ∨ 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 ) ↑.
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 men-
tioned statement r1 (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
the above mentioned statement r2 (d00 ) = F .
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 .
t
u
This result can be used as a semantic foundation of the following uncon-
strained inference rule for sequential composition for the inference system for
Floyd-Hoare logic with partial pre- and post-conditions (which involves the ∼
operation on predicates):
{p} f {q}, {q} g {r1 }, {∼ q}g{r2 }
R USEQ
{p} f • g {r1 ∨ r2 }
In the special case of coinciding r1 and r2 , it can be rewritten as:
{p} f {q}, {q} g {r}, {∼ q}g{r}
R SSEQ
{p} f • g {r}
Theorem 1 implies that addition of the rules R U SEQ and/or R SSEQ to
the inference system AC proposed in [9, 10] (with the proper extension of syntax
of pre- and post-condition predicate formulas to accommodate the symbol of ∼
operation) does not change its soundness.
As an informal example, consider how these rules can be potentially applied
in the case mentioned in the introduction:
{n>=0} a=zeros(n,1) {a(1)==0}
{a(1)==0} m=length(a) {m>0}.
These two assumptions alone are not sufficient to establish the triple con-
cerning 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 ab-
normal/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 state-
ment 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 Application to the While Loop Analysis
Let r be a partial predicate on D and f : D→D.
˜
Denote by W H(r, f ) the function D→D˜ such that for each d ∈ D,
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
| {z }
i
function on D (i.e. f (0) (d0 ) = d0 for all d0 ∈ D);
and W H(r, f )(d) ↑, otherwise.
In [12] W H, considered as an operation on r and f , is called the while com-
position. It is intended to capture the semantics of the loop of the form
while r do f end
in imperative programming languages which support structured programming.
Here f represents the semantics of the loop body.
In terms of W H the loop rule for the classical inference system for the Floyd-
Hoare logic with total pre- and post-conditions [11] can be reformulated as fol-
lows [18, p. 15]:
{r ∧ p} f {p}
R WH
{p} W H(r, f ) {¬r ∧ p}
Here p represents the loop invariant.
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 H 0 ) 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}.
Proof. Let d ∈ D. Assume that p(d) ↓= T , W H(r, f )(d) ↓= d0 , and (¬r ∧
p)(W H(r, f )(d)) ↓.
Let us show that (¬r ∧ p)(W H(r, f )(d)) = (¬r ∧ p)(d0 ) = T .
From the definition on W H it follows that 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 , and
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 .
Now we will assume that n ≥ 1.
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)) ↑.
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
because i < n. Denote d1 = f (i) (d).
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 )) ↓= T . Otherwise, p(f (d1 )) ↑. In either case, either
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 {r ∧ (∼ p)}f {p}, we have
either p(f (i+1) (d)) ∼
= p(f (d1 )) ↓= T , or p(f (i+1) (d)) ∼
= p(f (d1 )) ↑.
In both cases p(f (i+1) (d)) ↓= T or p(f (i+1) (d)) ↑, so the inductive step is
completed.
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
p(f (n) (d)) ↓.
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)) ↓,
(n)
we have p(f (d)) = T .
Consider the case p(f (n−1) (d)) ↑. Then because f (n−1) (d) ↓, we have
(∼ p)(f (n−1) (d)) ↓= T . Moreover, we have r(f (n−1) (d)) ↓= T , whence
(r ∧ (∼ p))(f (n−1) (d)) ↓= T . Then because {r ∧ (∼ p)}f {p} and, moreover,
p(f (f (n−1) (d))) ∼
= p(f (n) (d)) ↓, we have p(f (n) (d)) = T .
In both cases we have p(f (n) (d)) = T . Since r(f (n) (d)) ↓= F , we have
(¬r ∧ p)(W H(r, f )(d)) ∼ = (¬r ∧ p)(f (n) (d)) ↓= T . t
u
This result can be used as a semantic foundation of the following uncon-
strained inference rule (for the case of partial pre- and post-conditions):
{r ∧ p} f {p}, {r ∧ (∼ p)}f {p}
R UWH {p} W H(r, f ) {¬r ∧ p}
5 Conclusion
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 [9, 10]. These modifications concern sequence and
while rules and have been formulated in the extended program algebras. The
addition of these rules does not change the soundness of the system. However,
the new rules have no semantic constraints, unlike the sequence rule of the
original system. The obtained results can be useful for verification of program
with respect to specifications which can contain partial operations.
In the future we plan to make detailed comparison of inference systems and
propose new modifications to improve their efficiency.
References
1. Floyd, R.: Assigning meanings to programs. Mathematical aspects of computer
science 19(19-32) (1967)
2. Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10)
(1969) 576–580
3. Apt, K.: Ten years of Hoare’s logic: A survey – part I. ACM Trans. Program.
Lang. Syst. 3(4) (1981) 431–483
4. : MATLAB – MathWorks. https://www.mathworks.com/products/matlab.html
5. : GNU Octave. https://www.gnu.org/software/octave/
6. Jones, C.: Reasoning about partial functions in the formal development of pro-
grams. In: Proceedings of AVoCS’05. Volume 145., Elsevier, Electronic Notes in
Theoretical Computer Science (2006) 3–25
7. Hähnle, R.: Many-valued logic, partiality, and abstraction in formal specification
languages. Logic Journal of the IGPL 13(4) (2005) 415–433
8. Gries, D., Schneider, F.: Avoiding the undefined by underspecification. Technical
report, Ithaca, NY, USA (1995)
9. Nikitchenko, M., Kryvolap, A.: Properties of inference systems for Floyd-Hoare
logic with partial predicates. Acta Electrotechnica et Informatica 13(4) (2013)
70–78
10. Kryvolap, A., Nikitchenko, M., Schreiner, W.: Extending Floyd-Hoare logic for
partial pre- and postconditions. In Ermolayev, V., Mayr, H., Nikitchenko, M., Spi-
vakovsky, A., Zholtkevych, G., eds.: Information and Communication Technologies
in Education, Research, and Industrial Applications. Volume 412 of Communica-
tions in Computer and Information Science. Springer International Publishing
(2013) 355–378
11. Nielson, H., Nielson, F.: Semantics with applications – a formal introduction.
Wiley professional computing. Wiley (1992)
12. Skobelev, V., Nikitchenko, M., Ivanov, I.: On algebraic properties of nominative
data and functions. In Ermolayev, V., Mayr, H., Nikitchenko, M., Spivakovsky,
A., Zholtkevych, G., eds.: Information and Communication Technologies in Ed-
ucation, Research, and Industrial Applications. Volume 469 of Communications
in Computer and Information Science. Springer International Publishing (2014)
117–138
13. Nikitchenko, M., Shkilniak, S.: Mathematical logic and theory of algorithms.
Publishing house of Taras Shevchenko National University of Kyiv, Ukraine (in
Ukrainian) (2008)
14. Kornilowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: Formalization of the
algebra of nominative data in mizar. In Ganzha, M., Maciaszek, L.A., Paprzycki,
M., eds.: Proceedings of the 2017 Federated Conference on Computer Science and
Information Systems, FedCSIS 2017, Prague, Czech Republic, September 3-6, 2017.
(2017) 237–244
15. Kornilowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I. In: Formalization of
the Nominative Algorithmic Algebra in Mizar. Springer International Publishing,
Cham (2018) 176–186
16. Kleene, S.: Introduction to metamathematics. North-Holland Publishing Co.,
Amsterdam, and P. Noordhoff, Groningen (1952)
17. Kornilowicz, A., Ivanov, I., Nikitchenko, M.: Kleene algebra of partial predicates.
Accepted for publication in Formalized Mathematics (2018)
18. Kornilowicz, A., Kryvolap, A., Nikitchenko, M., Ivanov, I.: An approach to for-
malization of an extension of Floyd-Hoare logic. In: Proceedings of the 13th Inter-
national Conference on ICT in Education, Research and Industrial Applications.
Integration, Harmonization and Knowledge Transfer, Kyiv, Ukraine, May 15-18,
2017. (2017) 504–523