Inference Rules for the Partial Floyd-Hoare Logic Based on Composition of Predicate Complement

Abstract

Classical Floyd-Hoare logic is sound when total pre- and post-conditions are considered. In the case of partial conditions (predicates) the logic becomes unsound. This situation may be corrected by introducing additional constraints to the rules of the logic. But such constraints, in particular, for the sequence and while rules, are rather complicated. In this paper we propose new simpler rules formulated in a program algebra extended with the composition of predicate complement. The obtained logic is called the Complemented Partial Floyd-Hoare Logic (CPFHL). The predicate component of this logic is related to three-valued logic. We prove the soundness theorem for CPFHL and discuss further investigations of the problem. The obtained results can be useful for software verification.

1 Introduction

The research presented in this paper¹ is devoted to generalization of the classical Floyd-Hoare logic [2,3,4] to the case of partial pre- and post-conditions. This logic is a useful tool for proving partial correctness of sequential programs. It is based on properties of a Floyd-Hoare triple (assertion) of the form $\{p\}f\{q\}$ which consists of pre- and post-conditions p, q (predicates) and a program f. This assertion is treated in the following way: when the program’s input data d satisfies the pre-condition (p(d) is true), and the program terminates on d, the program’s output (the value f(d)) satisfies the post-condition (q(f(d)) is true).

Although in the classical Floyd-Hoare logic it is assumed that a 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 written in Octave syntax [5]

{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 partial, because extraction from a is not always defined in the sense that it causes an error or another type of abnormal behavior. In particular, a situation of this kind occurs in Matlab [6] 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 [7] 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,8,9].

To deal with this issue, in the previous works [10,11,12,13] extensions of the classical Floyd-Hoare logic which allowed one to reason about partial correctness of sequential programs using Floyd-Hoare triples with 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 (p(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)) is defined), 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). The logic itself will be called Partial Floyd-Hoare Logic (PFHL).

An important fact is that the classical inference system for the Floyd-Hoare logic for the language WHILE [14] is not sound in the presence of partial pre- and post-conditions [10]. One reason of this is unsoundness of the sequence rule when p, q, r are partial predicates:

where $f \bullet g$ denotes the sequential composition of programs f and g (i.e. g runs after f on the result of f).

This can be explained on the following simple example in Octave syntax. Let n be an integer-valued variable. The expression zeros(n,1) evaluates to a n $\times$ 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 assertions are valid (in the sense of weak Floyd-Hoare triples):

{n>=0} a=zeros(n,1) {a(i)==0},

{a(i)==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, new inference systems for Partial Floyd-Hoare Logic should be constructed. In our previous works we have considered two ideas of such construction. The first idea consists in restricting the class of assertions to T-increasing assertions [11]; in this case the rules preserve their validity and no other changes are required. The second idea consists in introducing constraints which restrict applicability of the rules of logic. Such a system with constrained rules was proposed in [10]. In this system the regular sequence rule was replaced with the following constrained sequence rule:

where

• $f \bullet g$ denotes the function $d \mapsto g(f(d))$ which is the result of sequential composition of f and g;

• $p \models q$ means that each interpretation of the formula $\lnot p \vee q$ (i.e. $p\rightarrow q$) never takes the false value (i.e. it is always either true or undefined);

• PC is the Predicate transformer composition [11] such that PC(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).

In a similar way some other rules were modified.

However, the presence of complicated constraints makes application of such rules difficult in all but the most trivial cases. Therefore in [11] such constraints were even called trifling constraints.

Thus, the above mentioned ideas lead to PFHL limitation (T-increasing assertions) or do not lead to practical inference systems (constrained rules). This implies that further investigation of PFHL is necessary and the inference rules have to be based on some other ideas.

In this paper we propose an extension of the predicate language with a new composition called predicate complement. Introduction of this composition permits us to modify the rules in such a way that they become sound and no constraints are required. The obtained inference system for PFHL based on extended program algebra can be useful for software verification.

2 Notation

The symbol $\tilde{\rightarrow }$ will denote partial functions and $\rightarrow$ will denote total functions (e.g. $f : A \tilde{\rightarrow }B$ means that f is a partial function on a set A with values in a set B; $f: A \rightarrow B$ means that f is a total function from A to B). We will use the symbol ${\mathop {\longrightarrow }\limits ^{n}}$ for partial functions with finite graph. For $f : D \tilde{\rightarrow }D'$:

• $f(d)\downarrow$ denotes that f is defined on $d\in D$;

• $f(d)\downarrow =d'$ denotes that f is defined on $d\in D$ and has the value $d'\in D'$;

• $f(d)\uparrow$ denotes that f is undefined on $d\in D$;

• ${{\,\mathrm{dom}\,}}(f)=\{ d\in D~|~f(d)\downarrow \}$ 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 $f_{1} (d_{1} )\cong f_{2} (d_{2} )$ means the strong equality, i.e. that $f_{1} (d_{1} )\downarrow$ if and only if $f_{2} (d_{2} )\downarrow$, and if $f_{1} (d_{1} )\downarrow$, then $f_{1} (d_{1} )=f_{2} (d_{2} )$.

We use the following notations for predicate $p: D \tilde{\rightarrow }Bool$:

• $p^{T} =\{ d~|~p(d)\downarrow =T\}$ is the truth domain of a predicate p;

• $p^{F} =\{ d~|~p(d)\downarrow =F\}$ is the falsity domain of p.

3 Program Algebras with Predicate Complement

In accordance with the composition-nominative approach [15,16,17,18] we consider program logics which are based on program algebras. Such algebras are constructed in the following way:

– first, a set D of data processed by programs is defined; in our case we treat D as hierarchical nominative data [19];

– then, classes of predicates $Pr= D \tilde{\rightarrow }Bool$ and functions $Fn= D \tilde{\rightarrow }D$ are defined;

– at last, operations (compositions) over Pr and Fn are specified.

This scheme leads to two-sorted program algebras. In our previous works [10, 11] we considered program algebras with traditional compositions. But the problem of defining unconstrained rules requires new compositions. In this paper we introduce a program algebra extended with a composition of predicate complement.

3.1 Hierarchical Nominative Data

Informally speaking, simple hierarchical nominative data are constructed inductively over sets of basic names V and values A and can be presented as trees, the arcs of which are labeled by elements of V and leafs are labeled by elements of A. Here we consider a more complex case in which names can be presented as sequences of elements of V of the form $v_1v_2{\ldots }v_n\in V^+$. Introduction of complex names from $V^+$ requires additional restrictions induced by the principle of unambiguous associative naming. This principle demands that for any hierarchical nominative data d with complex names for any two paths $(u_{1} ,u_{2} ,\ldots ,u_{k} )$ and $(v_{1} ,v_{2} ,\ldots ,v_{l} )$ in d, neither of which is a prefix of another, the words $u_{1} u_{2}\ldots u_{k}$ and $v_{1} v_{2}\ldots v_{l}$ are incomparable in the sense of the prefix relation. Such data are also called complex-named data [20]. An example of such data is $[uv \mapsto 1,w \mapsto [uw \mapsto 3 ]]$, $u,v,w \in V$. We denote this class of data as $ND_{CC}(V,A)$. Formal definitions can be found in [19, 21].

3.2 Basic Operations on Nominative Data

The basic operations on nominative data are the operations of

• denaming (taking the value of a name),

• naming (assigning a new value to a name),

• overlapping.

We define these operations for the class $ND_{CC}(V,A)$ of nominative data with complex names and values ($d\in ND_{CC}(V,A)$).

Definition 1

([19], Denaming). The (associative) denaming is an operation $v \Rightarrow _{a}$ with a parameter $v \in V^{ +}$ defined by induction on the length of v:

• if $v \in V$, then $v \Rightarrow _{a} (d) \cong {\left\{ \begin{array}{ll}d(v), &{} \text {if }d(v) \downarrow ; \\ d/v, &{} \text {if }d(v)\uparrow \text { and } d/v \ne \emptyset ;\\ \text {undefined}, &{} \text {if }d(v) \uparrow \text { and }d/v = \emptyset , \end{array}\right. }$ where $d / u = [v_{1} \mapsto d(v)~\vert ~ d(v) \downarrow ,v = uv_{1} ,v_{1} \in V^{ +} ];$

• if $v \in V^+ \backslash V$, then $v \Rightarrow _{a} (d) \cong v_{2} \Rightarrow _{a} (v_1 \Rightarrow _{a} (d)),$ where $v_1$ is the first symbol of v and $v_2$ is the suffix, i.e. $v_1$, $v_2$ are (unique) words such that $v = v_1 v_2$ and $v_1 \in V$.

Definition 2

([19], Naming). Naming is an unary operation $\Rightarrow v$ with a parameter $v \in V^{ +}$ such that $\Rightarrow v(d) = [v \mapsto d]$.

Overlapping is a kind of updating operation which updates the values of names in its first argument with the values of names in its second argument. For different types of nominative data different overlapping operations can be considered. Here we will define two kinds of overlapping: global and local overlapping. Global (associative or structural) overlapping $\nabla _a$ updates several values in the first argument while the local one $\nabla _a^v$ (with a parameter $v \in V^{ +}$) updates only one value which is associated with the name v.

Global overlapping can be used, e.g. for formalizing procedures calls, while the local overlapping can be used as a formalization of the assignment operator in programming languages.

Definition 3

([19], Global overlapping). This is a binary operation $\nabla _a$ defined by induction on the rank of the first argument as follows.

Let $ND_{{CC}_{k}} (V,A)$ be the class of data with the rank less of equal to k.

Induction base of the definition. If $d_{1} \in ND_{{CC}_{0}} (V,A)$, then

$$ d_{1} \nabla _{a} d_{2}\cong {\left\{ \begin{array}{ll} d_{2} , &{} \text { if } d_{1} = \emptyset \text { and } d_{2} \in ND_{CC}(V,A)\backslash A; \\ \text {undefined} , &{} \text { if } d_{1} \in A \text { or } d_{2} \in A. \\ \end{array}\right. } $$

Induction step of the definition. Assume that the value $d_{1} \nabla _{a} d_{2}$ is already defined for all $d_{1} ,d_{2}$ such that $d_{1} \in ND_{{CC}_{k}} (V,A)$. Let

$$d_{1} \in ND_{{CC}_{k + 1}} (V,A)\backslash ND_{{CC}_{k}} (V,A).$$

Then $d_{1} \nabla _{a} d_{2} = d$, where d is defined for each name $u \in V^+$ as follows:

• (1) $d(u) = d_{2} (u)$, if $u \in dom(d_2)$ and u does not have a proper prefix which belongs to $dom(d_{1})$;

• (2) $d(u) = d_{1} (u)\nabla _{a} (d_{2} / u)$, if $d_1(u)$ is defined and does not belong to A and u is a proper prefix of some element of $dom(d_{2})$, where

  

• (3) $d(u) = d_{2} / u$, if $d_1(u)$ is defined and belongs to A and u is a proper prefix of some element of $dom(d_{2})$;

• (4) $d(u) = d_{1} (u)$, if $d_1(u)$ is defined and u is not comparable (in the sense of the prefix relation) with any element of $dom(d_{2})$;

• (5) $d(u) \uparrow$, otherwise.

Definition 4

([19], Local overlapping). This is a binary operation $\nabla _a^v$ with a parameter $v \in V^+$ defined as follows: $d_1 \nabla _a^v d_2 \cong d_1 \nabla _a (\Rightarrow v(d_2)).$

3.3 Compositions

Now we define compositions of program algebras over nominative data with complex names and values.

Let V and A be fixed sets of basic names and values. Denote

$Pr_{CC}(V,A) = ND_{CC}(V,A) \tilde{\rightarrow }\{T, F\},$

$Fn_{CC}(V,A) = ND_{CC}(V,A) \tilde{\rightarrow }ND_{CC}(V,A)$.

We will assume that T and F do not belong to $ND_{CC}(V,A)$.

We will call the elements of $Pr_{CC}(V,A)$ (partial nominative) predicates and the elements of $Fn_{CC}(V,A)$ (partial nominative) functions.

Let us denote by $\bar{U}$ the set of all tuples $(u_1,u_2,\ldots ,u_n)$, $n \ge 1$ of complex names from $V^+$ such that whenever $i \ne j$, $u_i$ and $u_j$ are incomparable in the sense of the prefix relation.

In the following definitions $d \in ND_{CC}(V,A)$, $f, g, f_1,\ldots ,f_n \in Fn_{CC}(V,A)$, $p, p_1,p_2 \in Pr_{CC}(V,A)$.

Definition 5

(Compositions).

• Composition of superposition into a predicate

  $$ S_{P_{CC}}^{u_1,\ldots ,u_n}:Pr_{CC}(V,A) \times (Fn_{CC}(V,A))^n \rightarrow Pr_{CC}(V,A) $$

  with a parameter $(u_1,\ldots ,u_n) \in \bar{U}$ is defined as follows:

  $$ S_P^{u_1,\ldots ,u_n}(p,f_1,\ldots ,f_n)(d) \cong p(... (d \nabla _a^{u_1}f_1(d) ) \ldots \nabla _a^{u_n}f_n(d)). $$

  We will also use the following notation for this composition: $S_P^{\bar{u}}.$

• Composition of superposition into a function

  $$ S_F^{u_1,\ldots ,u_n}:Fn_{CC}(V,A) \times (Fn_{CC}(V,A))^n \rightarrow Fn_{CC}(V,A) $$

  with a parameter $(u_1,\ldots ,u_n) \in \bar{U}$ is defined as follows:

  $$ S_F^{u_1,\ldots ,u_n}(f,f_1,\ldots ,f_n)(d) \cong f(\ldots (d \nabla _a^{u_1}f_1(d)) ... \nabla _a^{u_n}f_n(d)). $$

  We will also use the following notation for this composition: $S_F^{\bar{u}}$.

• Assignment composition $AS^u: Fn_{CC}(V,A) \rightarrow Fn_{CC}(V,A)$ with a parameter $u \in V^+$ is defined as follows:

  

• Sequential composition of functions (denoted using the infix notation) $\bullet : Fn_{CC}(V,A) \times Fn_{CC}(V,A) \rightarrow Fn_{CC}(V,A)$ is defined as follows:

  

• Branching composition $IF: Pr_{CC}(V,A) \times Fn_{CC}(V,A) \times Fn_{CC}(V,A) \rightarrow Fn_{CC}(V,A)$ is defined as follows:

  $$ IF(p,f,g)(d) = {\left\{ \begin{array}{ll} f(d), &{} \text {if }p(d)\downarrow = T \text { and }f(d)\downarrow ;\\ g(d), &{} \text {if }p(d)\downarrow = F \text { and } g(d)\downarrow ; \\ \text {undefined} &{} \text {in other cases}. \end{array}\right. } $$

• Cycle composition $WH: Pr_{CC}(V,A) \times Fn_{CC}(V,A) \rightarrow Fn_{CC}(V,A)$ is defined as follows:

  $WH(p,f)(d)\downarrow =f^{(n)}(d)$, if there exists $n \ge 0$ such that $p(f^{(i)} )(d)\downarrow = T$ for all $i \in \{0,1,\ldots ,n-1\}$ and $p(f^{(n)} p)(d)\downarrow = F$, where $f^{(n)}$ is a n-times sequential composition of f with itself ($f^{(0)}$ is the identity function), and WH(p, f)(d) is undefined otherwise.

• Identity null-ary composition (function) $id: Fn_{CC}(V,A)$ ($id : ND_{CC}(V,A) \rightarrow ND_{CC}(V,A)$) is defined as follows:

  

• Composition of disjunction $\vee : Pr_{CC}(V,A) \times Pr_{CC}(V,A) \rightarrow Pr_{CC}(V,A)$ is a composition defined as follows:

  $$ (p_1 \vee p_2)(d) = {\left\{ \begin{array}{ll} T, &{} \text {if }p_{1}(d)\downarrow = T \text { or } p_2(d)\downarrow =T;\\ F, &{} \text {if }p_{1}(d)\downarrow = F \text { and } p_2(d)\downarrow =F; \\ \text {undefined} &{} \text {in other cases}. \end{array}\right. } $$

• Composition of negation $\lnot : Pr_{CC}(V,A) \rightarrow Pr_{CC}(V,A)$ is a composition such that

  $$ (\lnot p)(d) = {\left\{ \begin{array}{ll} T, &{} \text {if }p(d)\downarrow = F ;\\ F, &{} \text {if }p(d)\downarrow = T ; \\ \text {undefined} &{} \text {in other cases}. \end{array}\right. } $$

• Composition of existential quantification over hierarchical data is a unary composition $Pr_{CC}(V,A) \rightarrow Pr_{CC}(V,A)$ with a parameter $x\in V^{+}$ such that

  $$ (\exists x\, p)(d)=\left\{ \begin{array}{l} {T, \text { if }p(d\nabla _{a}^{x} d')\downarrow =T\mathrm{\; \text {for some }}d'\in ND_{CC}(V,A)}, \\ {F,\text { if }p(d\nabla _{a}^{x} d')\downarrow =F \text { for all }d'\in ND_{CC}(V,A)}, \\ \text {undefined in other cases.} \end{array} \right. $$

• Composition of predicate complement is a composition $\sim : Pr_{CC}(V,A) \rightarrow Pr_{CC}(V,A)$ such that

  $$ (\sim p)(d) = {\left\{ \begin{array}{ll} T, &{} \text {if }\,\, p(d)\,\, \text { is undefined};\\ \text {undefined} &{} \text { in other cases}. \end{array}\right. }. $$

Having compositions, we can define a special program algebra investigated in this paper.

Definition 6

A complemented program algebra over hierarchical nominative data with complex names and values $CPAND_{CC}(V,A)$ is a two-sorted algebra $CPAND_{CC}(V,A)= (Pr_{CC}(V,A), Fn_{CC}(V,A);$

where $v,u,x \in V^+,\bar{u} \in \bar{U}$.

Derived compositions like conjunction $\wedge$ and universal quantification $\forall x$ are defined in a traditional way.

Let us discuss briefly predicate compositions of this algebra. Operations (compositions) $\vee$, $\lnot$, and $\exists x$ are defined according to the truth tables of Kleene’s strong logic of indeterminacy [22]. Please note that $\vee$, $\wedge$ and $\lnot$ on the set of all partial predicates form a Kleene algebra (a De Morgan algebra which satisfies the normality axiom) [23].

In contrast to these compositions, the composition of predicate complement is more complicated. First, it does not have the monotonicity property, second, it does not have nice distributivity properties. Even more, it is not computable in the sense that the set of partial recursive predicates is not closed under this composition.

Introduction of the composition of predicate complement makes investigation of the corresponding logics more difficult. In this case methods developed for three-valued logics can be used.

Nevertheless, the algebra $(Pr_{CC}(V,A); \vee , \wedge , \lnot , \sim )$ has certain properties which make it useful in program partial correctness proofs:

• it can be proven that the algebra $(Pr_{CC}(V,A); \vee , \wedge , \lnot , \sim )$ has the same (up to the names of operations) set of identities as the algebra

  $$ (\{-1, 0, 1\}; \max (\cdot , \cdot ), \min (\cdot , \cdot ), x\mapsto -x, x \mapsto 1-|x|); $$

• all scalar functions of n variables expressible in the latter algebra are nonexpanding maps from $\{-1, 0, 1\}^n \rightarrow \{-1, 0, 1\}$ with respect to Chebyshev distance $dist((x_1, \ldots , x_n), (y_1, \ldots , y_n)) = \max _{i =1}^n |x_i - y_i|$.

Definition 7

A semantic weak Floyd-Hoare triple is a tuple (p, f, q), where $f:D \tilde{\rightarrow }D'$, $p: D \tilde{\rightarrow }Bool$, $q : D' \tilde{\rightarrow }Bool$ for some $D,D'$ such that for each $d \in D$, if $p(d)\downarrow = T$ and $f(d)\downarrow$ and $q(f(d)) \downarrow$, 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.

Please note that a semantic weak Floyd-Hoare triple induces ternary Floyd-Hoare composition $FH: Pr_{CC}(V,A) \times Fn_{CC}(V,A) \times Pr_{CC}(V,A) \rightarrow Pr_{CC}(V,A)$ [10, 11], but in this paper we do not include it into program algebras in order to not make them overcomplicated.

We start with new inference rules for the sequential composition. These rules are valid for any set of data D.

4 New Inference Rules for Sequential Composition

Theorem 1

Assume that $\{p\}f\{q\}$, $\{q\}g\{r_1\}$, and $\{\sim q\}g\{r_2\}$.

Then $\{p\}f \bullet g \{r_1 \vee r_2\}$.

Proof

Let $d \in D$. Assume that $p(d)\downarrow = T$, $(f \bullet g)(d)\downarrow$, and $(r_1 \vee r_2)((f \bullet g)(d))\downarrow$.

Then $f(d)\downarrow$ and $g(f(d))\downarrow$. Denote $d' = f(d)$ and $d'' = (f \bullet g)(d) = g(f(d))$.

Let us show that $(r_1 \vee r_2)(d'') = T$.

Suppose that $(r_1 \vee r_2)(d'') \downarrow = F$. Then $r_1(d'')\downarrow =F$ and $r_2(d'')\downarrow =F$. We have that either $q(d')\downarrow$, or $q(d')\uparrow$.

Consider the case when $q(d')\downarrow$. Then $q(f(d))\downarrow$, and since $p(d)\downarrow =T$ and $\{p\}f\{q\}$, we have $q(f(d))=q(d')=T$. Then since $r_1(g(d'))\cong r_1(d'')\downarrow$ and $\{q\}g\{r_1\}$, we have $r_1(g(d'))=r_1(d'')=T$, but this contradicts the above mentioned statement $r_1(d'')=F$.

Consider the case when $q(d')\uparrow$. Then $(\sim q)(d')\downarrow =T$. Then since $r_2(g(d'))\cong r_2(d'')\downarrow$ and $\{\sim q\}g\{r_2\}$, we have $r_2(g(d'))=r_2(d'')=T$, but this contradicts the above mentioned statement $r_2(d'')=F$.

In both cases we have a contradiction, so $(r_1 \vee r_2)(d'') \downarrow = F$ is impossible. But $(r_1 \vee r_2)(d'') \cong (r_1 \vee r_2)((f \bullet g)(d))\downarrow$ by the assumption, so $(r_1 \vee r_2)(d'') = T$.

   $\square$

This result can be used as a semantic foundation of the following unconstrained inference rule for sequential composition for the inference system for Floyd-Hoare logic with partial pre- and post-conditions (which involves the $\sim$ operation on predicates):

In the special case of coinciding $r_1$ and $r_2$, it can be rewritten as:

Theorem 1 implies that addition of the rules $R\_USEQ$ and/or $R\_SSEQ$ to the inference system AC proposed in [10, 11] (with the proper extension of syntax of pre- and post-condition predicate formulas to accommodate the symbol of $\sim$ operation) does not change its soundness.

As an informal example, consider how these rules can be applied in the case mentioned in the Introduction:

These two assumptions alone are not sufficient 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 the Introduction, this undefinedness means that an 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

where $\sim$ is not a part of Octave syntax, but just a notation to represent the statement that the expression (a(1)==0) is undefined (causes an abnormal/error state). Thus by the $R\_USEQ$ rule:

Again, here $\vee$ is not a part of Octave syntax, but a notation to represent the disjunction of two predicates.

5 New Inference Rule for Cycle Composition

Let r be a partial predicate on D and $f:D \tilde{\rightarrow }D$.

Recall that the cycle composition WH(r, f) is defined as follows: it returns a function in $D\tilde{\rightarrow }D$ such that for each $d \in D$,

$$ WH(r,f)(d)\downarrow =f^{(n)} (d), $$

if there exists an integer $n\ge 0$ such that $r(f^{(i)} (d))\downarrow =T$ for all $i=0,1,\ldots ,n-1$ and $r(f^{(n)} (d))\downarrow =F$, where $f^{(i)}$ denotes $\underbrace{f\bullet f\bullet \ldots \bullet f}_{i}$ and $f^{(0)}$ is the identity function on D (i.e. $f^{(0)}(d')=d'$ for all $d' \in D$);

and $WH(r,f)(d)\uparrow$, otherwise.

WH is intended to capture the semantics of the loop of the form while$\_$do$\_$ in imperative programming languages which support structured programming. Here r represents the semantics of the loop condition and f represents the semantics of the loop body.

In terms of WH the loop rule for the classical inference system for the Floyd-Hoare logic with total pre- and post-conditions [14] can be reformulated as follows [24, p. 15]:

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 [24, p. 16] ($R\_WH'$) 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 is more convenient to apply.

Theorem 2

Assume $\{r \wedge p\}f\{p\}$, $\{r \wedge (\sim p)\} f \{p\}$. Then $\{p\} WH(r,f) \{\lnot r \wedge p\}$.

Proof

Let $d \in D$. Assume that

Let us show that $(\lnot r \wedge p)(WH(r,f)(d)) = (\lnot r \wedge p)(d')=T$.

From the definition on WH it follows that there exists an integer $n\ge 0$ such that $r(f^{(i)} (d))\downarrow =T$ for all $i=0,1,\ldots ,n-1$, and $r(f^{(n)} (d))\downarrow =F$, and

$$d' = WH(r,f)(d) = f^{(n)} (d).$$

If $n=0$, then $d'=d$, so $r(d')\downarrow =F$ and $p(d')\downarrow =T$, whence $(\lnot r \wedge p)(d')=T$.

Now we will assume that $n \ge 1$.

Let us show by induction on $i \in \{0,1,\ldots \}$ that if $i \in \{0,1,\ldots ,n-1\}$, then $p(f^{(i)}(d))\downarrow = T$ or $p(f^{(i)}(d))\uparrow$.

Base of induction: $p(f^{(0)}(d)) \cong p(d) \downarrow = T$, so the statement holds.

Inductive step. Assume that $i \in \{0,1,\ldots ,n-1\}$. Assume that $p(f^{(i)}(d))\downarrow = T$ or $p(f^{(i)}(d))\uparrow$. Assume that $i+1 \in \{0,1,\ldots ,n-1\}$. Note that $r(f^{(i)}(d)) \downarrow =T$ because $i<n$. Denote $d_1 = f^{(i)}(d)$.

Consider the case $p(f^{(i)}(d))\downarrow = T$. Then since $r(d_1)\downarrow =T$ and $p(d_1)\downarrow =T$, we have $(r \wedge p)(d_1)\downarrow =T$. If $p(f(d_1))\downarrow$, then since $\{r \wedge p\} f \{p\}$, we have $p(f^{(i+1)}(d)) \cong p(f(d_1))\downarrow =T$. Otherwise, $p(f(d_1))\uparrow$. In either case, either $p(f^{(i+1)}(d))\downarrow = T$, or $p(f^{(i+1)}(d))\uparrow$ holds.

Consider the case $p(f^{(i)}(d))\uparrow$. Then $p(d_1)\uparrow$ and $r(d_1)\downarrow =T$. Further, $(\sim p)(d_1)\downarrow =T$, so $(r \wedge (\sim p))(d_1)\downarrow =T$. Since $\{r \wedge (\sim p)\} f \{p\}$, we have either $p(f^{(i+1)}(d)) \cong p(f(d_1)) \downarrow = T$, or $p(f^{(i+1)}(d)) \cong p(f(d_1)) \uparrow$.

In both cases $p(f^{(i+1)}(d))\downarrow = T$ or $p(f^{(i+1)}(d))\uparrow$, so the inductive step is completed.

Since $n \ge 1$ by our assumption, the proven statement implies that either $p(f^{(n-1)}(d))\downarrow = T$, or $p(f^{(n-1)}(d))\uparrow$. We have

Moreover, $r(f^{(n)} (d))\downarrow =F$, so $(\lnot r)(f^{(n)} (d))\downarrow =T$, whence $p(f^{(n)}(d))\downarrow$.

Consider the case $p(f^{(n-1)}(d))\downarrow = T$. We have $r(f^{(n-1)} (d))\downarrow =T$, therefore $(r \wedge p)(f^{(n-1)} (d)) \downarrow = T$. Then since $\{r \wedge p\}f\{p\}$ and $p(f(f^{(n-1)}(d))) \cong p(f^{(n)}(d))\downarrow$, we have $p(f^{(n)}(d)) = T$.

Consider the case $p(f^{(n-1)}(d))\uparrow$. Then because $f^{(n-1)}(d) \downarrow$, we have $(\sim p)(f^{(n-1)}(d)) \downarrow = T$. Moreover, we have $r(f^{(n-1)} (d))\downarrow =T$, whence $(r \wedge (\sim p))(f^{(n-1)} (d)) \downarrow = T$. Then because $\{r \wedge (\sim p)\}f\{p\}$ and, moreover, $p(f(f^{(n-1)}(d))) \cong p(f^{(n)}(d))\downarrow$, we have $p(f^{(n)}(d)) = T$.

In both cases we have $p(f^{(n)}(d)) = T$. Since $r(f^{(n)} (d))\downarrow =F$, we have $(\lnot r \wedge p)(WH(r,f)(d)) \cong (\lnot r \wedge p)(f^{(n)} (d)) \downarrow = T$.    $\square$

This result can be used as a semantic foundation of the following unconstrained inference rule (for the case of partial pre- and post-conditions):

6 Syntax and Interpretation of Complemented Partial Floyd-Hoare Logic

Algebra $CPAND_{CC}(V,A)$ has strong expressive power that is not required for our goal: to construct a special program logic. Therefore we restrict syntactically the class of terms of this algebra. The idea is to consider programs as special nominative functions (program functions) constructed with the help of compositions $AS^{x}$, id, $\bullet$, IF, WH, $S_{F}^{\bar{x}}$. Functions of other types can be represented by functional expressions. Formulas represent partial predicates over nominative data. The signature of the constructed logic is $\varSigma =(V, Ps, FEs, Prgs)$ where Ps, FEs, Prgs are sets of predicate, function, and program symbols respectively.

Let us give definitions of the sets of formulas $Fr^\varSigma$, functional expressions $FEx^\varSigma$, program texts $Pt^\varSigma$, and Floyd-Hoare assertions $FHFr^\varSigma$.

The sets $Fr^\varSigma$, $FE^\varSigma$, and $Pt^\varSigma$ are defined inductively (here we use the symbols of compositions, predicates and functions in the purely syntactic sense, i.e. they are currently not associated with semantics):

• 1. if $ps\in Ps$, then $ps\in Fr^\varSigma$;

• 2. if $fes\in FEs$, then $fes\in FE^\varSigma$;

• 3. if $prgs\in Prgs$, then $prgs\in Pt^\varSigma$;

• 4. if $\varPhi ,\varPsi \in$ $Fr^\varSigma$, then $\varPhi \vee \varPsi$, $\lnot \varPhi$, $\sim \varPhi$, $\exists x \varPhi \in Fr^\varSigma$;

• 5. $\Rightarrow v$, $v\Rightarrow _{a}\in FE^\varSigma$;

• 6. if $n\ge 1$, $\varPhi \in Fr^\varSigma$, $fe_{1},\dots ,fe_{n} \in FE^\varSigma$, and $\bar{x}\in \bar{U}$, then $S_{P}^{\bar{x}} (\varPhi ,fe_{1},\dots ,fe_{n} )\in$ $Fr^\varSigma$;

• 7. if $n\ge 1$, fe, $fe_{1},\dots ,fe_{n} \in FE^\varSigma$, and $\bar{x}\in \bar{U}$, then $S_{F}^{\bar{x}} (fe,fe_{1},\dots ,fe_{n} )\in$ $FE^\varSigma$;

• 8. if $n\ge 1$, $prg\in Pt^\varSigma$, $fe_{1},\dots ,fe_{n} \in FE^\varSigma$, and $\bar{x}\in \bar{U}$, then $S_{F}^{\bar{x}} (prg,fe_{1},\dots ,fe_{n} )\in$ $Pt^\varSigma$;

• 9. if $x\in V^{+}$ and $fe\in FE^\varSigma$, then $AS^{x} (fe)\in$ $Pt^\varSigma$;

• 10. $id\in Pt^\varSigma$;

• 11. if $prg_{1},prg_{2} \in$ $Pt^\varSigma$, then $pr_{1} \bullet pr_{2} \in$ $Pt^\varSigma$;

• 12. if $\varPhi \in Fr^\varSigma$ and $prg_{1},prg_{2} \in$ $Pt^\varSigma$, then $IF(\varPhi ,prg_{1},prg_{2} )\in$ $Pt^\varSigma$;

• 13. if $\varPhi \in Fr^\varSigma$ and $prg\in$ $Pt^\varSigma$, then $WH(\varPhi ,prg)\in$ $Pt^\varSigma$.

To avoid syntactical nondeterminism, parentheses can be used.

The set $FHFr^\varSigma$ is the set of all formulas of the form $\{ p\} f\{ q\}$, where p, $q\in Fr^\varSigma$ and $f\in Pt^\varSigma$.

Please note that we often use the same notation both for predicates and for formulas, e.g. depending on the context, p can be treated as a predicate or as a function; the same concerns functions and functional expressions.

Definition 8

Let $\varSigma =(V, Ps, FEs, Prgs)$ be a logic signature and A be a set. Then an interpretation J is a tuple $(CPAND_{CC}(V,A),I_{Ps}, I_{FEs} ,I_{Prgs} )$, where $I_{Ps} :Ps {\rightarrow }Pr_{CC}(V,A)$ is an interpretation mapping for predicate symbols, $I_{FEs}:FEs{\rightarrow }Fn_{CC}(V,A)$ and $I_{Prs} :Prs\rightarrow Fn_{CC}(V,A)$ are interpretation mappings for function and program symbols, respectively.

For any interpretation $J=(CPAND_{CC}(V,A),I_{Ps}, I_{FEs} ,I_{Prgs} )$ we denote by $J_{Fr}$, $J_{FE}$, and $J_{Pt}$ the formula, function, and program text interpretation mappings

$$ J_{Fr} :Fr^\varSigma {\rightarrow } Pr_{CC}(V,A), $$

$$ J_{FE} :FE^\varSigma {\rightarrow } Fn_{CC}(V,A), $$

$$ J_{Pt} :Pt^\varSigma {\rightarrow } Fn_{CC}(V,A), $$

which are the standard extensions of $I_{Ps}, I_{FEs}$, and $I_{Prgs}$ to $Fr^\varSigma$, $FE^\varSigma$, and $Pt^\varSigma$ respectively (defined by structural induction). Also, we denote by $J_{FHFr}$ the interpretation mapping of Floyd-Hoare assertions $J_{FHFr} :FHFr^\varSigma {\longrightarrow } Pr_{CC}(V,A)$ defined as follows:

$$ J_{FHFr} \; (\{ p\} f\{ q\} )=FH(J_{Fr} \; (p),J_{P{} t} (f),J_{Fr} \; (q)). $$

Here we will not define interpretations explicitly expecting that they are clear from the context. For any $P\in Fr^\varSigma$ or $P\in FHFr^\varSigma$ we will denote by $P_{J}$ or $(P)_{J}$ the predicate that corresponds to P under interpretation J. We will omit the index J when it is clear from the context.

Definition 9

A formula $P\in$ $Fr^\varSigma$ or a Floyd-Hoare assertion $P\in FHFr^\varSigma$ is valid (irrefutable) in an interpretation J (denoted as $J \models P$), if $P_{J}^{F} =\emptyset$.

Definition 10

A formula $P\in Fr^\varSigma$ or a Floyd-Hoare assertion $P\in FHFr^\varSigma$ is logically valid (denoted as $\models P$), if it is valid in every interpretation.

We will also need special logical truth-consequence and falsity-consequence relations [10] $\models _{T}, \models _{F}~\subseteq ~Fr^\varSigma \times Fr^\varSigma$.

Definition 11

A formula $Q\in Fr^\varSigma$ is a truth-consequence of a formula $P\in Fr^\varSigma$ in an interpretation J (denoted as $P_J \models _T Q$), if $P_{J}^{T} \subseteq Q_{J}^{T}$. A formula $Q\in Fr^\varSigma$ is a logical truth-consequence of a formula $P\in Fr^\varSigma$ (denoted as $P \models _T Q$), if $P_J \models _T Q$ for every interpretation J.

Definition 12

A formula $Q\in Fr^\varSigma$ is a falsity-consequence of a formula $P\in Fr^\varSigma$ in an interpretation J (denoted as $P_J \models _F Q$), if $P_{J}^{F} \supseteq Q_{J}^{F}$. A formula $Q\in Fr^\varSigma$ is a logical falsity-consequence of a formula $P\in Fr^\varSigma$ (denoted as $P \models _F Q$), if $P_J \models _F Q$ for every interpretation J.

7 Inference System for a Complemented Partial Floyd-Hoare Logic

To make the program logic CPFHL which we have defined applicable to software verification problems it is necessary to present an inference system. Such an inference system could be based on the inference system for the classical Floyd-Hoare logic with total predicates for the language WHILE [14], but it is known to be unsound in the case of partial predicates [11] which is considered in the paper. For this reason we present new inference rules based on program algebras with the composition of predicate complement. Obtained system will be sound.

We will write $\left. \vdash \right. _{X} p$ to denote that a formula p is derived in some inference system X. An inference system X is sound, if $\left. \vdash \right. _{X} p \Rightarrow ~\models p$ for each formula p, and is complete, if $\models p\Rightarrow \left. \vdash \right. _{X} p$ for each p.

Taking into consideration the obtained results we write the following inference rules ($v, x\in V^+, \bar{x} \in \bar{U}$, $p,p', q, q', r\in Fr^\varSigma$, $h,g_1,\ldots ,g_n\in FE^\varSigma$, $f,g\in Pt^\varSigma$):

Let us make the following comments to these rules:

• rules $R\_AS$, $R\_SFID$ and $R\_SF$ are the only rules oriented on the class of nominative data with complex names and values; other rules can be considered for any class of data D;

• rules $R\_SKIP$ and $R\_IF$ are traditional rules for Floyd-Hoare logics; they do not require any changes;

• rules $R\_SSEQ$ and $R\_UWH$ were proposed and investigated in the previous sections;

• rules $R\_SFID$ and $R\_SF$ specify procedure calls;

• consequence rules can be formulated in different forms; here we use the rule $R\_CONS_{TF}$ based on special consequence relations $\models _T$ and $\models _F$. In the case of total predicates this rule will be equivalent to traditional consequence rule.

We denote the inference system presented by the above rules as RCN.

Theorem 3

The inference system RCN is sound, i.e. for any Floyd-Hoare assertion $P\in$ $FHFr^\varSigma$ we have that

$$ \left. \vdash \right. _{RCN} P \Rightarrow \, \,\models P. $$

Proof

We prove the theorem by induction on the length of inference of P. Let $J=(CPAND_{CC}(V,A),I_{Ps}, I_{FEs} ,I_{Prgs} )$.

• Consider the case when P has the form $\{ S_{P}^{x} (p,h)\} \mathrm{\; }AS^{x} (h)\mathrm{\; }\{ p\}$ and P is inferred in RCN, i.e. $\vdash _{RCN} P$ ($q,p\in Fr^\varSigma , h\in FE ^\varSigma$) by rule $R\_AS$.

  Given an interpretation J we should prove that $J\models \{ S_{P}^{x} (p,h)\} \mathrm{\; }AS^{x} (h)\mathrm{\; }\{ p\}$. This means (by the definition of weak Floyd-Hoare triple) that we should prove the following statement: for any $d, d' \in ND_{CC}(V,A)$ if $S_{P}^{x}(p,h)_J(d)\downarrow =T$, $AS^{x} (h)_J(d)\downarrow =d'$, and $p _J(d')\downarrow$ then $p _J(d')=T$.

  By definition of the composition of superposition into a predicate we have that $S_{P}^{x}(p,h)_J(d)=p_J(d\nabla ^x_a h_J(d))$. By definition of assignment composition we have that $AS^{x} (h)_J(d)=d\nabla ^x_a h_J(d)$. Since $p_J(d\nabla ^x_a h_J(d))=T$ and $d\nabla ^x_a h_J(d)=d'$ we obtain that $p_J(d')=T$.

• The case when P has the form $\{ p\} \; id\; \{ p\}$ i.e. the rule $R\_SKIP$ is used to infer P is trivial.

• The case when P is obtained by rule $R\_SSEQ$ has been proved in Sect. 4 of this paper.

• The case when P is obtained by rule $R\_IF$ is a traditional one.

• The case when P is obtained by rule $R\_UWH$ has been proved in Sect. 5 of this paper.

• Consider the case when P is obtained by rule $R\_SFID$. It means that P has the form $\{ S_{P}^{\bar{x}} (p,g_{1},\dots ,g_{n} )\} S_{F}^{\bar{x}} (id,g_{1},\dots ,g_{n} )\{ p\}$ ($\bar{x}= (x_1,\ldots ,x_n)$.

  Given an interpretation J we should prove that

  

  This means (by the definition of weak Floyd-Hoare triple) that we should prove the following statement:

  for any $d, d' \in ND_{CC}(V,A)$ if $S_{P}^{\bar{x}} (p,g_{1},\dots ,g_{n} )_J(d)\downarrow =T$,

  $S_{F}^{\bar{x}} (id,g_{1},\dots ,g_{n} )_J(d)\downarrow =d'$, and $p _J(d')\downarrow$ then $p _J(d')=T$.

  By the definition of the composition of superposition into a predicate we have that $S_P^{x_1,\ldots ,x_n}(p,g_1,\ldots ,g_n)_J(d) = p_J(\ldots (d \nabla _a^{x_1}{g_1}_J(d) ) \ldots \nabla _a^{x_n}{g_n}_J(d))$. Obtained value is equal to T.

  By the definition of the composition of superposition into a function we have that $S_{F}^{x_1,\ldots ,x_n} (id,g_{1},\dots ,g_{n} )_J(d)=id_J(\ldots (d \nabla _a^{x_1}{g_1}_J(d) ) \ldots \nabla _a^{x_n}{g_n}_J(d))=d'$.

  Therefore, $p _J(d')\downarrow =T$.

• Consider the case when P is obtained by rule $R\_SF$. In this case P has the form $\{ p\} S_{F}^{\bar{x}} (f,g_{1},\dots ,g_{n} )\{ q\}$. Given an interpretation J we should prove that $J\models \{ p\} S_{F}^{\bar{x}} (f,g_{1},\dots ,g_{n} )\{ q\}$ under assumption $J\models \{ p\} S_{F}^{\bar{x}} (id,g_{1},\dots ,g_{n} )\bullet f\{ q\}$. It means that we should prove the following statement:

  for any $d, d' \in ND_{CC}(V,A)$ if $p_J(d)\downarrow =T$, $S_{F}^{\bar{x}} (f,g_{1},\dots ,g_{n} )_J(d)\downarrow =d'$, and $q _J(d')\downarrow$ then $q _J(d')=T$ using inductive hypothesis.

  First, let us prove that $(S_{F}^{\bar{x}} (id,g_{1},\dots ,g_{n} )\bullet f)_J(d) \cong S_{F}^{\bar{x}} (f,g_{1},\dots ,g_{n} )_J(d)$ for any $d \in ND_{CC}(V,A)$.

  Indeed, $(S_{F}^{\bar{x}} (id,g_{1},\dots ,g_{n} )\bullet f)_J(d)\cong f_J(S_{F}^{\bar{x}} (id,g_{1},\dots ,g_{n} )_J(d)) \cong$

  $\cong f_J(id_J(... (d \nabla _a^{u_1}g_1{_J}(d)) \ldots \nabla _a^{u_n}g_n{_J}(d)))\cong$

  $\cong f_J(\ldots (d \nabla _a^{u_1}g_1{_J}(d)) \ldots \nabla _a^{u_n}g_n{_J}(d)) \cong S_{F}^{\bar{x}} (f,g_{1},\dots ,g_{n} )_J(d)$.

  Let $p_J(d)\downarrow =T$, $S_{F}^{\bar{x}} (f,g_{1},\dots ,g_{n} )_J(d)\downarrow =d'$, and $q _J(d')\downarrow$.

  Since $(S_{F}^{\bar{x}} (id,g_{1},\dots ,g_{n} )\bullet f)_J(d) \cong S_{F}^{\bar{x}} (f,g_{1},\dots ,g_{n} )_J(d)$ we have that

  $(S_{F}^{\bar{x}} (id,g_{1},\dots ,g_{n} )\bullet f)_J(d)\downarrow =d'$.

  Then, by induction hypothesis for $\{ p\} S_{F}^{\bar{x}} (id,g_{1},\dots ,g_{n} )\bullet f\{ q\}$ we obtain the required property $q _J(d')\downarrow =T$.

• Consider the case when P is obtained by rule $R\_CONS_{TF}$. It means that P has the form $\{p\}f\{q\}$. Given an interpretation J we should prove $J\models \{ p\}f\{q\}$ under assumptions $J\models \{ p'\}f\{q'\}$, $p{}_J\models _T p'$ and $q'{}_J\models _F q$.

  Indeed, let $d \in ND_{CC}(V,A)$. Assume that $p{}_J(d)\downarrow =T$, $f_J(d)\downarrow =d'$ and $q_J(d')\downarrow$ for some $d' \in ND_{CC}(V,A)$. Since $p{}_J\models _T p'$ we have $p'{}_J(d)\downarrow =T$. Since $f_J(d)\downarrow =d'$ and $J\models \{ p'\}f\{q'\}$ we have $q'_J(d')=T$ when $q'_J(d')\downarrow$. Assume that $q_J(d')=F$. Since $q'{}_J\models _F q$ we should have $q'_J(d')=F$. We have a contradiction with $q'_J(d')=T$. Therefore, $q_J(d')=T$.

   $\square$

In the system RCN new unconventional consequence relations $\models _T$ and $\models _F$ were used. Their main semantic properties were studied in [25]. Further investigation will permit one to substitute these consequence relations by the corresponding inference relations $\vdash _{T}$ and $\vdash _{F}$. A detailed investigation of inference methods for CPFHL is planned for the forthcoming publications.

8 Conclusion

We have proposed a modified inference system for an extended Floyd-Hoare logic for partial pre- and post-conditions and partial programs studied in [10, 11, 26]. The modifications primarily concern the sequence and while rules and have been formulated in program algebras extended with the composition of predicate complement. The addition of these rules does not change the soundness of the system. Moreover, the new rules have no semantic constraints. The obtained results can be useful for verification of programs 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.