-

Program Logics of Renominative Level with the Composition of Predicate Complement

0 Taras Shevchenko National University of Kyiv , 60 Volodymyrska Street, City of Kyiv, Ukraine, 01033

Program logics are wildly used for software verification. Such logics are based on formal program models and reflect main program properties. Among various program logics, Floyd-Hoare logic and its variants take a special place because of its naturalness and simplicity. But such logics are oriented on total pre- and post-conditions, and in the case of partial conditions they become unsound. Different methods to overcome this problem were proposed in our previous works. One of the methods involves extension of program algebras with the composition of predicate complement. This permits to modify rules of the logic making them sound. Such modification requires introduction of undefinedness conditions into logic rules. In this paper we continue our research of such logics. We investigate a special predicate logic called logic of renominative (quantifier-free) level with the composition of predicate complement. This logic is a constituent part of the program logic. We introduce a special consequence relation for this logic, construct a sequent calculus, and prove its soundness and completeness.

software verification program logic Floyd-Hoare logic partial predicate soundness completeness

The formalism of program logics is the main instrument for software verification [ 1 ]. To be effective, such logics should reflect main program properties. Therefore, adequate formal program models should be constructed which will form a base for a program logic. Among such logics we should point to Floyd-Hoare logic and its variants as quite natural and simple [2, 3]. But such logics are oriented on total pre- and post-conditions, and in the case of partial conditions (predicates) they become unsound.

In our previous works [4, 5] we considered several methods to extend Floyd-Hoare logic for partial predicates, in particular, we proposed two methods: 1) introduction of special rule constraints; and 2) restriction of the class of program assertions (of Hoare triples). Both methods make a logic sound but they are difficult for practical usage or are rather restrictive. Here we study one more method which proposes to extend program algebras with the composition of predicate complement [ 6, 7 ]. Introduction of this composition permits to modify rules in such a way that they become sound, but a negative side of this proposal is that logic becomes more complicated. In this case, undefinedness conditions for predicates should be taken into account.

In this paper we continue our research of logics with the composition of predicate complement. We concentrate on a base logic which is a constituent part of program logic. This logic is a special logic of partial quasiary predicates of renominative (quantifier-free) level. We introduce a consequence relation with undefinedness conditions, study its properties, and define a sequent calculus. We prove the soundness and completeness theorems for this logic with the composition of predicate complement. 2

Program Algebras with the Composition of Predicate

Complement

According to the principles of composition-nominative approach [8, 9] we construct program logics based on program algebras. Such algebras are defined in the following way [ 9, 10 ]: 1) a set D of data processed by programs is defined; 2) the classes of partial predicates Pr = D pBool and partial functions

Fn = D p D are defined; 3) operations (compositions) over Pr and Fn are specified.

This scheme leads to two-sorted program algebras. In our previous works we considered program algebras with traditional compositions. But the problem of defining sound rules for program logics requires new compositions. Therefore, here we consider a program algebra extended with the composition of predicate complement. This unary predicate composition is defined in the following way ( p  Pr, d  D ): ( p)(d)   unTde,fiinfedp,(dif) ips(udn)diesfidneefdin,ed.

Specifying D as the class DCC (V , A) of hierarchical nominative data [ 7, 11 ] with complex names and values built over the set of basic names V and the set of basic values A, we can define a complemented program algebra as a two-sorted algebra [7] CPANDCC (V , A)  (PrCC (V , A), FnCC (V, A);

ASu ,id, IF,WH, SFu , SPu , v, v a , , , x, ) where PrCC (V, A) and FnCC (V , A) are classes of partial predicates and partial function over DCC (V , A) respectively; ASu , id, IF, WH, SPu , SFu are compositions of assignment, identity, conditional, cycle, superposition into predicate, superposition into function respectively;  v and v a are naming and denaming functions; , , x, are composition of disjunction, negation, existential quantification, and predicate complement; v, u, x V  are complex names, u U is a sequence of complex names. This algebra is quite expressive to present formal semantics of rather complex programs.

A special program logic of Floyd-Hoare type based on such algebras is presented in [7]. Its distinctive feature is introduction of new rules which are sound for partial predicates and which use preconditions constructed with the help of the composition of predicate complement.

For example, a classical rule of Floyd-Hoare logic for sequential execution of operators f and g has the form

R _ SEQ {p} f {q},{q}g{r}

{p} f  g{r} where f  g denotes sequential execution of f and g.

This rule is not sound in the case of partial predicates [4]. Therefore, a new sound rule based on extended program algebra was introduced [7]:

{p} f {q},{q}g{r},{ q}g{r} R _ SSEQ {p} f  g{r} .

Obtained program logic can be an important instrument of program verification. So, its thorough investigation is required. This is a rather complicated challenge; therefore, we start with more simple logics. First, we identify a special predicate logic as a constituent part of the program logic. Such predicate logic can be considered as a logic defining constraints (program annotations). Second, we will consider here only logic LQCR of renominative level which can be characterized as quantifier-free predicate logic of partial quasiary predicates with the composition of predicate complement. The case of first-order logic with quantifiers and functions is planned to study in the forthcoming papers. 3

Logic of Partial Quasiary Predicates of Renominative Level with the Composition of Predicate Complement To define a logic LQCR we should define [ 9, 10 ] – its class of algebras; – its language (based on logic signature); – its class of interpretations; – its consequence relation; – its inference relation based on some calculus.

Formal definitions will be given in the next section. We will use the following notations: – S pS ' ( S tS ' ) is the class of partial (total) mappings from S to S '; – p(d)  ( p(d)  ) means that p is defined (undefined) on d; – p(d)  T ( p(d)  F ) means that p is defined on d with value T (F). For this case we also use simpler notation p(d)  T ( p(d )  F ).

The terms and notations, not defined here, are treated in the sense of [ 12 ]. 3.1

Complemented Algebras of Partial Quasiary Predicates of Renominative Level Let V be a set of names (variables) and A be a set of values. The class V A of nominative sets (partial assignments, partial data) is defined as the class of all partial mappings from V to A, thus, V A  V p A .

Nominative sets represent states of program variables.

The main operation for nominative sets is a total unary parametric renomination rvx11,,......,,vxnn : V A t V A , where v1,..., vn , x1,..., xn are names, and v1,..., vn are distinct [ 12 ]. Intuitively, given nominative set d this operation yields a new nominative set changing the values of v1,..., vn to the values of x1,..., xn respectively. We also use simpler notation for this renomination: rv . We write x v to denote that x is a varix able from v ; we write v  x to denote the set of variables that occur in the sequences v and x .

The set of assigned variables (names) in d is denoted asn(d).

Let PrAV  V A pBool be the set of all partial predicates over V A . Such predicates are called partial quasiary predicates. For a predicate p  PrAV its truth, falsity, and undefinedness domains are denoted T(p), F(p), and  ( p) respectively. Please note that these domains do not intersect pairwise and their union is equal to V A ; thus, predicate p is defined by T(p) and F(p) only, because  ( p)  V A \ (T( p)  F( p)) .

Operations over PrAV are called compositions. Basic compositions of renominative level over quasiary predicates are disjunction , negation , and renomination Rv . x We extend this set with the composition of predicate complement . These compositions are defined by the following formulas ( p, q  PrAV ): – T(pq) = T(p)T(q); F(pq) = F(p)F(q); – T(p) = F(p); F(p) = T(p); – T (Rxv ( p)) = {dVA | rvx (d) T( p) }; F (Rxv ( p)) = {dVA | rvx (d)  F( p) }; – T( p) =  ( p) ; F( p)=  .

Please note that definitions of disjunction and negation are similar to strong Kleene’s connectives [ 13 ]. We consider as a composition of propositional level.

A tuple

 QCR (V, A) = < PrAV ; , , Rxv , > is called a complemented algebra of partial quasiary predicates of renominative level.

A class of such algebras (with different A) forms a semantic base for a logic LQCR.

Now we describe the main properties of  QCR (V, A). We do not formulate traditional properties of propositional compositions of disjunction and negation [ 9, 14 ], but concentrate on properties of compositions of renomination and complement.

Compositions of disjunction and negation have traditional properties; in contrast to these compositions, the composition of predicate complement is more complicated: it does not have the monotonicity property and it does not have distributivity properties with respect to disjunction. For this composition we identify the following properties.

Lemma 1. For any p  PrAV we have p  p ; p  p ; p  p .

Lemma 2. For any p  PrAV we have 1) T( p)   ; F( p)  T ( p) ;  ( p)   ( p) ; 2) T(Rxv ( p)) = T ( (Rxv ( p))) ; F(Rxv ( p))   ;  (Rxv ( p)) =  ( (Rxv ( p))) .

The notion of unessential variable is important for the composition of renomination. A name (variable) z is unessential for predicate p  PrAV , if for any dVA the value of p does not depends on the value of z [ 9, 12 ].

Lemma 3. The following properties of the compositions of renomination and predicate complement hold for any p  PrAV :

R) Rxv ( p  q)  Rxv ( p)  Rxv (q) ; R) Rxv (p)  Rxv ( p) ; RR) Rxv (Ryw ( p))  Rxv wy ( p) ; R ) Rv ( p) 

x R) R(p) = p; RI) Rzz,,xv ( p)  Rxv ( p) ;

Rxv ( p) ;

RU) Ryz,,vx ( p)  Rxv ( p) if zV is unessential for p. is called the language signature.

For simplicity, we use the same notation for symbols of compositions and compositions themselves.

Given QCR , we define inductively the language of LQCR – the set of formulas denoted Fr( LQCR ) or simply Fr: – if P  Ps then PFr. Formulas of such forms are called atomic; – if , Fr then , , Rxv  ,  Fr . Let  QCR (V, A) = < PrAV ; , , Rv ,

x QCR  (V,U;, , Rvx , ; Ps) , IQPs  Ps tPrAV > be a complemented algebra of a signature be an interpretation mapping of predicate symbols. Then a tuple J( QCR ) = ( QCR (V, A), IQPs ) is called an LQCR interpretation.

We simplify notation for LQCR -interpretation J( QCR ) omitting LQCR and QCR .

In interpretation J, an algebra  QCR (V, A) defines interpretations of composition symbols while IQPs defines interpretations of predicate symbols.

For given interpretation J and formula , we can define by induction on the structure of  its value in J. Obtained predicate is denoted  J.

Lemma 4. Let J be an interpretation and , Fr. Then

R) R()J = J ; RI) Rzz,,xv ()J  Rxv ()J ; RU) Ryz,,vx ()J  Rxv ()J if zV is unessential for ; R) Rxv ()J  Rxv ()J ; R) Rxv (  )J  Rxv ()J  Rxv ()J ; RR) Rxv (Ryw ())J  Rxv wy ()J ; R ) Rv ( )J  x

Rxv ()J . 3.4

Logical Consequence Relation under Conditions of Undefinedness Introduction of composition requires more complicated consequence relation because undefinedness domains should be taken into consideration. Here we introduce new consequence relation between sets of formulas denoted |=IR which generalizes irrefutability relation |=IR [7].

Let   Fr and J be an interpretation.

We denote:

T(J ) as T( J),

F(J ) as F( J),  (J ) as ( J).    Here J denotes set {  |    }.

J Set  can be empty. In this case

T() = T() = F() = F() = () = () = V A .

Let , U,   Fr. Informally, the statement “ is irrefutable consequence of  under undefinedness conditions U in interpretation J ” means “for any dVA if J (d)  for any U then it is not possible that ( J (d) = T for any  and J (d) = F for any  )”.

This statement is equivalent to the following statement:

“for any dVA if d(UJ) then it is not possible that dT(J)F( J) ”. The former statement can be reformulated as follows:

“for any dVA it is not possible that (d(UJ) and dT(J)F( J)) ”. Finally, we obtain the following statement:

“(UJ)  T(J)  F( J) =  ”.

So, we come to the following formal definition:  is irrefutable consequence of  under undefinedness conditions U in interpretation J (denoted U /  J |=IR  ) if

T(J)  (UJ)  F( J) = .

In particular, for U =  we obtain irrefutability consequence relation  J |=IR .  is logical irrefutability consequence of  under undefinedness conditions U (denoted U /  |=IR ), if U /  J |=IR  for any interpretation J.

In particular, for U = , we get traditional logical irrefutability relation  |=IR .

Let us now describe the main properties of the consequence relation |=IR for propositional level.

By definition of |=IR, we obtain monotonicity: M) Let   , U  W, and   ; then U /  |=IR   W /  |=IR .

Proof. Property С holds because T(J)  F(J) = .

For property СUL we take into consideration that (J)  T(J) = .

For property СUR we take into consideration that (J)  F(J) = .

Property C holds because F( J) = .

For |=IR the following properties of formula decomposition hold.

U, /  |=IR , ; U) U,  /  |=IR   U / ,  |=IR  and U /  |=IR , ;

L) U / ,  |=IR   U,  /  |=IR .

Proof. Property U holds because (J) = (J).

Property U holds because

 (J  J )  ( (J )  (J )) ( (J )  F(J )) (F(J )  (J )) . Property

U holds because  ( J ) = T(J)  F(J). U,

Properties L, R, L, R are similar to properties of |=IR [ 9, 12, 13 ]. Properties U,

L, U are special for LQCR.

Let us consider properties of relation |=IRU of a renominative level. Their proofs are based on Theorem 2. Each of properties R, RI, RU, RR, R, R, R of Lemma 4 induces three corresponding properties for |=IRU, depending on the position of a formula (in the left side of |=IRU, in the right side of |=IRU, in the undefinedness conditions of |=IRU). Such properties are formulated in a similar way, for example, the following properties R L, R R, R U are induced by R :

R L) U / Rxv ( ),  |=IR   U / Rxv (),  |=IR ; R R) U /  |=IR , Rxv ( )  U /  |=IR , Rxv () ;

R U) U, Rxv ( ) /  |=IR   U, Rxv ()/  |=IR . 4

Sequent Calculus for LQCR Usually, inference relations are defined by some axiomatic systems (calculi). We present here a system that formalizes logical consequence relation between two sets of formulas. Such systems are called sequent calculi.

We construct a sequent calculus CQCR for relation |=IR.

The main objects of this calculus are sequents. Here we consider only the case with finite sequents. We construct calculus in the style of semantic tableau, so, we will treat sequents as finite sets of formulas signed (marked, indexed) by symbols |– , –| , and  .

Formulas from  (they are signed by |–) are called T-formulas, formulas from  (they are signed by –|) are called F-formulas, and formulas from U (they are signed by ) are called  -formulas.

Sequents are denoted |–U–|, in abbreviated form .

The derivation in a sequent calculus has the form of a tree whose vertices are sequents. Such trees are called sequent trees.

The rules of sequent calculus are called sequent forms. They are syntactical analogs of the semantic properties of the corresponding relations of logical consequence. Details of the definition of sequent tree can be found in [ 12 ].

Closed sequents are axioms of the sequent calculus.

A closed sequent is specified in such a way that the following condition should hold:

if sequent |–U–| is closed then U /  |=IR .

Sequent calculus is defined by basic sequent forms and closure conditions of sequents.

For CQCR we take the following closure conditions:

sequent |–U–| is closed if condition CCUL CUR C holds.

Here C, CUL, CUR, C are the following basic closure conditions: C) exists :  and ; CUL) exists :  and U; CUR) exists :  and U;

C ) exists :  .

Theorem 3. If sequent |–U–| is closed then U/ |=IR .

Proof. The theorem statement follows directly from Theorem 1.

The sequent forms of decomposition of compositions , , are induced by the corresponding properties of formulas decomposition, in particular, basic sequent forms of CQCR calculus are induced by the formula decomposition properties L, R, L, R, U, U, U, L: | |,  ; |,  | |,  ; |,   ,  ; ,  |,  |,  ;  ,  ,  , | ,  |,  ,  | |,  |,  ; | |, |,  ,  ;

For the composition of renomination we use the following forms of equivalent transformations:

Rxv wy () represents application of two successive renominations Here Rxv (Ryw()) [ 12 ].

Forms of simplification: |–R |, ; |R(), –|R |, ; |R(), R  R(,), ;  |,  |,   , 

; |–R |Rxv (), |Rxv (),

; |Rxv (), |– R | Rxv (), |Rxv ( ),

; |–RR |Rxv wy (), |Rxv (Ryw()),

; |–R |Rxv () Rxv (), ; –|R |Rxv () Rxv (), | ,  | , 

. –|R |Rxv (), |Rxv (),

; |Rxv (), –| R  | Rxv (),

|Rxv ( ), –|RR |Rxv wy (), |Rxv (Ryw()), ; R Rxv (), ;

Rxv (), ; R Rxv () Rxv (), ;

Rxv (), ;  R  Rxv (), ;

Rxv ( ), RR Rxv wy (), Rxv (Ryw()), . |–RI | Rxv (),  ;

| Rzz,,xv (),  |–RU | Ruv (),  ; | Rzy,,uv (),  –|RI | Rxv (),  ;

| Rzz,,xv (),  –|RU | Ruv (),  | Rzy,,uv (),  ; RI  Rxv (),  ;

 Rzz,,xv (),  RU  Rxv (),   Ryz,,vx (),  .

The names of the sequent forms are consistent with the names of the properties of the decomposition of the formulas. Introduction of undefinedness formulas additionally leads to new sequent forms with three premises (rule ).

For basic rules of CQCR we have the following main properties.

Theorem 4.

be basic sequent form. Then 1. Let | W|

| U| a) U /  |=IR   b) U /  |IR  

W /  |=IR ;

W /  |IR . 2. Let | W|

|V| | U| a) U /  |=IR   b) U /  |IR  

W /  |=IR  and V /  |=IR ;

W /  |IR  or V /  |IR . 3. Let | W| |V| |Y| | U| be basic sequent form. Then

be basic sequent form. Then a) U /  |=IR   b) U /  |IR  

W /  |=IR  and V /  |=IR  and Y /  |=IR ;

W /  |IR  or V /  |IR  or Y /  |IR .

Proof. The proof of the theorem is obtained by set-theoretic methods using a formula specifying relation |=IR. 5

Soundness and Completeness of CQCR Now we prove soundness and completeness theorems for CQCR.

Theorem 5 (soundness). Let sequent |–U–| be derivable in CQCR. Then U /  |=IR .

The completeness is traditionally proved on the basis of theorems of the existence of a counter-model for the set of formulas of a non-closed path in the sequent tree. In this case a method of model sets is used.

We apply this method to the CQCR calculus.

Set Н of signed formulas is a model set (Hintikka’s set) for LQCR if the following conditions hold:

or   Н and –|Н or –|Н and   Н; Н Н

L) If |  Н, then   Н;

v Н R R) | Rx ( )  H  | Rxv ()  H ;

v Н R U)  Rx ( )  H   Rxv ()  H .

Conditions for the composition of renomination are formulated in a similar way, for example, sequent forms RI and R induce the following conditions:

A set H  Fr is called satisfiable if there exist a set A, an interpretation J, and a nominative set   V A such that – |–Н  A()  = T; – –|Н  A()  = F; –   Н  A()  .

A set Н of signed formulas for which the above-written conditions hold is called HQCR-model.

Theorem 6. Let H be HQCR-model for LQCR. Then H is satisfiable.

Proof. Given HQCR-model Н, we should construct a set A, an interpretation J, and a nominative set   V A that demonstrate satisfiability of H. These constructions are rather complicated due to undefinedness conditions therefore here we do not present the proof in all details but demonstrate only its main parts.

Let W = nm(Н) be a set of subject names (variables) that occur in H. Let a set А duplicates W and VA be a nominative set such that asn() = W.

Let us prescribe values of basic predicates on nominative set  and nominative sets of the form rvx () . To do this, we use notations PA() = T, PA() = F, and PA()  ) to prescribe the value of P on d in algebra  QCR (V, A) equal to T, equal to F, and to be undefined respectively: – |– PН  PA() = T; – –| PН  PA() = F; –  P Н  PA()  ; – | Rxv (P)  H  PA (rvx ())  T ; – – | Rxv (P)  H  PA (rvx ())  F ;  Rxv (P)  H  PA (rvx ())  . – Formulas of the form | Rxv (P) are called primitive.

For a predicate symbol PPs that does not occur in H, its value can be chosen in arbitrary way. Also, we should treat variables from U as unessential.

For atomic and primitive formulas the satisfiability statements follow from their definitions.

Now the proof goes on by induction on the formula structure.

Let us prove the theorem for conditions НRIL, Н R R, Н R U, НL, НR, НU, НL, НR, НU, Н U, Н L .

Let | Rzz,,xv ()  H . By НRIL we have | Rxv ()  H . By induction hypothesis Rxv ()A ()  T , therefore Rzz,,xv ()A ()  T .

Let | Rx ( )  H . By Н R R we have | Rxv ()  H . By induction hypothesis v Rxv ()A ()  F , therefore Rv ( )A ()  F .

Rv ( )  H . By Н R U we have  Rxv ()  H . By induction hypothesis Let  x Rxv ()A()  , therefore Rv ( )A()  .

Let |–Н. By НL we have –|Н. By induction hypothesis A() = F, therefore A() = T.

Let –|Н. By НR we have |–Н. By induction hypothesis A() = T, therefore A() = F.

Let |–Н. By НL we have |–Н or |–Н. By induction hypothesis A() = T and A() = T, therefore ()A() = T.

Let –|Н. By НR we have –|Н and –|Н. By induction hypothesis A() = F and A() = F, therefore ()A() = F.

Let   Н. By НU we have   Н. By induction hypothesis A()  , therefore A()  .

Let     Н. By НU   Н and   Н or   Н and –|Н or –|Н and   Н. By induction hypothesis A()  and A()  or A()  and A() = F or A() = F and A()  . Therefore (A)()  .

Let 

Let | fore

 A(d)  T . A() = T or A() = F, this gives A()  , therefore  A(d)  .  Н. By Н

U we have |–Н or –|Н. By induction hypothesis  Н. By Н

L we have   Н. By induction hypothesis A()  , thereTheorem 7. Let  be unclosed path in a sequent tree for |–U–| and H be the set of all formulas in . Then H is a model set.

Proof. We should check that H satisfies all requirements that specify a model set. Details can be found in [ 12 ] but additionally undefinedness conditions should be taken into account.

The completeness theorem follows from Theorems 6 and 7.

Theorem 8 (completeness). Let U /  |=IR  hold. Then sequent |–U–| is derivable in CQCR.

Proof. Assume that U /  |=IR  and |–U–| is not derivable. In this case a sequent tree for |–U–| is not closed. Thus, an unclosed path  exists in this tree. Let H be the set of all formulas of this path. By Theorem 7, H is a model set. By theorem 6 this means that a counter-model for |–U–| was constructed. But this contradicts to U /  |=IR  . 5. Conclusion The efficiency of program verification heavily depends on program logics supporting corresponding verification methods. Traditional Floyd-Hoare logic and its variants are oriented on total pre- and post-conditions (total predicates) and do not support partial predicates. In this paper we have studied a new method for constructing sound program logics. This method is based on extending program logics with the composition of predicate complement. The method permits to construct a sound calculus for program logic but it makes the calculus more complicated because undefinedness conditions should be taking into consideration.

Also, introduction of partial predicates required extension of a base predicate logic to a logic of partial quasiary predicate. For this logic we have defined and investigated a special consequence relation called irrefutability consequence relation with undefinedness conditions. For a case of quantifier-free predicate logic of partial quasiary predicates (renominative level) we have constructed a calculus of sequent type and proved its soundness and completeness.

In the future we plan to construct a sequent calculus for predicate logic over hierarchical nominative data and prove its soundness and completeness. Also, we plan to develop a prototype of theorem prover oriented on such logics. Initial steps were made in [ 15 ].

[1] Abramsky , S. , Gabbay , D. , Maibaum , T. (editors). Handbook of Logic in Computer Science , Oxford University Press, Vol. 1 - 5 ( 1993 -2000)

Hoare , C. : An axiomatic basis for computer programming , Commun. ACM 12 ( 10 ), 576 - 580 ( 1969 )

Apt , K. : Ten years of Hoare's logic: a survey - part I, ACM Trans . Program. Lang. Syst . 3 ( 4 ), 431 - 483 ( 1981 )

Kryvolap , A. , Nikitchenko , M. , Schreiner , W. : Extending Floyd-Hoare logic for partial pre- and postconditions . In: Communications in Computer and Information Science , vol. 412 , pp. 355 - 378 . Springer, Cham ( 2013 )

Nikitchenko , M. , Kryvolap , A. : Properties of inference systems for Floyd-Hoare logic with partial predicates , Acta Electrotechnica et Informatica , 13 ( 4 ), 70 - 78 ( 2013 )

[6] Ivanov , I. , Nikitchenko , M. : On the sequence rule for the Floyd-Hoare logic with partial pre- and post-conditions . In Proceedings of the 14th International Conference on ICT , vol. 2104 of CEUR Workshop Proc., pp. 716 - 724 ( 2018 )

Nikitchenko , M. , Ivanov , I. , Korniłowicz , A. , Kryvolap , A. : Extended Floyd-Hoare logic over relational nominative data . In: Bassiliades, N. , Ermolayev , V. , Fill , H.G. , Yakovyna , V. , Mayr , H.C. , Nikitchenko , M. , Zholtkevych , G. , Spivakovsky , A . (eds.) Information and Communication Technologies in Education, Research, and Industrial Applications. pp. 41 - 64 . Springer International Publishing, Cham ( 2018 )

Nikitchenko , N.S.:

A composition-nominative approach to program semantics . Technical report , IT-TR 1998- 020 , Technical University of Denmark ( 1998 )

Nikitchenko , M. , Shkilniak , S. : Mathematical logic and theory of algorithms . Кyiv: VPC Кyivskyi Universytet , in Ukrainian ( 2008 )

[10] Nikitchenko , M. , Tymofieiev , V. : Satisfiability in Composition-Nominative Logics , Open Computer Science (former Central European Journal of Computer Science) , vol. 2 , issue 3, pp. 194 - 213 ( 2012 )

[11] Nikitchenko , M. , Ivanov , I. , Skobelev , V. : Proving properties of programs on hierarchical nominative data , Comput. Sci. J . Moldova, 24 ( 3 ( 72 )), 371 - 398 ( 2016 )

[12] Nikitchenko , M. , Shkilniak , S. : Algebras and logics of partial quasiary predicates , Algebra and Discrete Mathematics , vol. 23 . No 2, pp. 263 - 278 ( 2017 )

[13] Korniłowicz , A. , Ivanov , I. , Nikitchenko , M. : Kleene algebra of partial predicates . Formalized Mathematics , 26 , 11 - 20 ( 2018 )

[14] Nikitchenko , M. , Shkilniak , O. Shkilniak , S. : Pure first-order logics of quasiary predicates, Problems in Programming . No 2 -3 , pp. 73 - 86 , in Ukrainian ( 2016 )

[15] Kornilowicz , A. , Kryvolap , A. , Nikitchenko , M. , Ivanov , I. : Formalization of the nominative algorithmic algebra in Mizar . In: J. Świątek , L. Borzemski , Z. Wilimowska (eds.) ISAT 2017 , AISC , vol. 656 , pp. 176 - 186 . Springer, Cham ( 2018 )