175 Satisfiability Problems in Quasiary Program Logics Mykola Nikitchenko, Stepan Shkilniak, Valentyn Tymofieiev Department of Theory and Technology of Programming, Taras Shevchenko National University of Kyiv, UKRAINE, 60 Volodymyrska Street, City of Kyiv, Ukraine, 01033, email: mykola.nikitchenko@gmail.com Abstract: In the paper we present special program nominative logics (CNL). specification algebras and logics defined for classes of In this paper we continue our work on studying CNL [4–6] quasiary mappings. Informally speaking, such mappings focusing on quasiary specification algebras and logics. The are partial mappings defined over partial states (partial main questions under discussion concern satisfiability assignments) of variables. Conventional n-ary mappings problems and their reduction to satisfiability problems in can be considered as a special case of quasiary mappings. logics of n-ary mappings. Such mappings better reflect properties of software systems. We describe methods of reducibility of the II. QUASIARY MAPPINGS satisfiability problem in quasiary logics to the Quasiary mappings can be met in different branches of satisfiability problem in logics of n-ary mappings. The mathematics, logics, and computer science. Informally methods proposed can be useful for software verification. speaking, such mappings appear when we use variables Keywords: n-ary mapping, quasiary mapping, program (names) to construct mapping arguments. Here we consider algebra, specification logic. only usage of quasiary mappings in logic semantics and formal models of programs. I. INTRODUCTION The notion of quasiary predicate and function can be Algebraic approach to software system specification has easily understood when we analyze Tarski’s definition of the following two characteristics: 1) the formalism of many- first-order language semantics. This semantics is based on the sorted algebras is used to model such systems; 2) special notion of interpretation which consists of two parts: 1) logics based on such many-sorted algebras are used to reason interpretation of predicate and function symbols in some about system properties. In the literature various kinds of structure, and 2) interpretation of individual variables in the such algebras and logics are described (e.g. see [1, 2]). domain of this structure. The latter are usually called variable In this paper we present special algebras and logics assignments (or valuations) and can be represented by total defined for classes of quasiary mappings. Informally mappings from a set of individual variables (names) V into speaking, such mappings are partial mappings defined over some set of basic values A. The class of such total mappings partial states (partial assignments) of variables. Conventional will be denoted V  →t A or AV, and called total nominative n-ary mappings can be considered as a special case of sets. Thus, Tarski’s semantics interprets predicate and quasiary mappings. Quasiary mappings better reflect function symbols as total quasiary predicates and functions properties of software systems therefore construction and defined on the class AV of total nominative sets. In investigation of algebras and logics of quasiary mapping is an applications like model checking, program verification, important challenge. automated theorem proving, etc., partial assignments Proposed constructions are based on a composition- (nominative sets) are often used instead of total assignments. nominative approach [3]. Principles of the approach The class of such partial mappings will be denoted (development of program notions from abstract to concrete, p V → A or VA, and called partial nominative sets (partial priority of semantics, compositionality of programs, and nominativity of program data) specify program models as data); the term ‘partial is often omitted. Predicates and composition-nominative systems which consist of functions over nominative sets are called quasiary. This composition, description, and denotation systems. A means that formulas and terms can be interpreted as quasiary composition system defines semantic aspects of programs, a predicates and functions respectively. description system defines program descriptions (syntactic Quasiary mappings also appear in a natural way in aspects), and a denotation system specifies meanings denotational semantics of programs. In this semantics (referents) of descriptions. We consider semantics of program states are represented as nominative sets, Boolean programs as partial functions over a class of data processed expressions as quasiary predicates of the type PrAV =VA by programs; compositions are n-ary operations over  p → Bool, arithmetical expressions as quasiary functions of functions. Thus, a composition system can be specified by two algebras: data algebra and function algebra. Function p the type FnVA = VA  → A, and program statements as bi- algebra is the main semantic notion in program formalization. quasiary functions (program functions) of the type PFAV =VA Terms of this algebra define syntax of programs (description p system), and ordinary procedure of term interpretation gives a → VA. Semantics of structured statements is defined by denotation system. the following compositions with conventional meaning: The constructed program models form a base for assignment composition AS x (x is a parameter from V), developing special program logics called composition- composition of sequential execution •, conditional ACIT 2018, June 1-3, 2018, Ceske Budejovice, Czech Republic 176 composition IF, loop composition WH. For structural SS F . S Fy , x ( S Fx ,v ( f , f , h ), f ', h ') = S Fy , x ,v ( f , σ ) , expressions we additionally use unary denomination composition ′x and various superpositions. SS G . SGy , x ( SGx ,v ( g , f , h ), f ', h ') = SGy , x ,v ( g , σ )) , Thus, we obtain a program algebra with three carriers: where quasiary predicates, quasiary functions, and bi-quasiary σ = ( f ', S Fy , x ( f1 , f ', h '),..., S Fy , x ( f k , f ', h '), functions (program functions). Such algebras can be called algorithmic algebras. S Fy , x (h1 , f ', h '),..., S Fy , x (hm , f ', h ')). To extend such algebras to program specification algebras Lemma 2 (distributivity of superposition). The following we add quantifiers and prediction composition ‘⋅’. Prediction properties hold in AVA (CsV ) : composition is simply a functional composition of a program function and a predicate. This composition is strong enough S∨. S Pv ( p ∨ q, f= ) S Pv ( p, f ) ∨ S Pv (q, f ) , to represent Hoare assertions, and therefore, specification S¬. S Pv (¬p, f ) = ¬S Pv ( p, f ) , algebras with these compositions are rather expressive [7]. In the rest of the paper we consider program specification S=. S= P ( h1 h= v 2 , f ) ( S F ( h= v v 1 , f ) S F ( h2 , f )) . algebras and logics of partial quasiary mappings. ∃u S Pv ( S Px ( p, ' u ), f ) , u≠x, u ∉ v , u is S∃. S Pv (∃xp, f ) = To emphasize a mapping’s partiality/totality we write the unessential for p and f , p t sign → for partial mappings and the sign  → for total (here “u is unessential for p and f ” means that p mappings. Given a partial mapping µ, µ ′: D → D′ , d, p (d ) ≅ p (d ') and f ( d ) ≅ f ( d ') for any d and d ' such that d′ ∈ D we write: d ||−{u} = d ' ||−{u} ). – µ(d)↓ (µ(d)↑) to denote that µ is defined (undefined) on d; Superposition compositions are not distributive with – µ(d)↓= d′ to denote that µ is defined on d with a value d′ ; respect to WH, therefore we simplify superpositions into – µ (d ) ≅ µ '(d ') to denote the strong equality. program functions using the identity program function id. We omit proofs and some details of complicated Lemma 3 (superpositions with program functions). The definitions. following properties hold in AVA (CsV ) : III. QUASIARY SPECIFICATION ALGEBRAS SG. S= G ( g , f ) SG (id , f ) • g – superposition into program v v function, We use the following set of composition symbols parameterized by V: SP. S Pv ( g ⋅ p, f= ) SGv ( g , f ) ⋅ p – superposition with v v v v v v prediction composition. CsV = {∨, ¬, ∃x, ' x, S P1,..., n , S F1,..., n , = , SG1,..., n , AS x , •, IF , WH , ⋅} Lemma 4 (superposition simplification). The following Formal definitions of compositions can be found in [4, 7, properties hold in AVA (CsV ) : v v v v v v 8]. Compositions S P1,..., n , S F1,..., n , and SG1,..., n are called SE. S P ( p) = p , S F ( f ) = f , SG ( g ) = g – superpositions superpositions and represent substitutions of quasiary with empty parameter list, functions into a predicate, function, and program function x ∉ v , S Fx,v (' x, f , h ) = f – SiD. S Fv (' x, f ) = ' x if respectively. We also denote such compositions as S Pv , S Fv , superpositions into denomination functions, SGv . SwD. S Px,v ( p, ' x, f ) = S Pv ( p, f ) , S Fx,v (h, ' x, f ) = S Fv (h, f ) A tuple AVA (CsV ) = < PrAV , FnVA , PFAV ; CsV > is called – superpositions with denomination function, quasiary specification algebra (QSA) over V and A. ST. S Pv , x, y , z (ϕ , f , h, h ', f ') = S Pv , y , x, z (ϕ , f , h ', h, f ') , Variables used as composition parameters can be classified as essential in the sense that they can affect the result of S Fv , x, y , z ( f , f , h, h ', f ') = S Fv , y , x, z ( f , f , h ', h, f ') , composition application evaluation and as updatable in the v , x, y , z v , y , x, z SG ( g , f , h, h ', f ') = SG ( g , f , h ', h, f ') – sense that the values of these variables can change during transposition of parameters. evaluation. Variable x is essential for denomination These properties will be used to construct superpositional composition ' x , variable x is updatable for ∃x and AS x , normal forms for language expressions. v v v v Now we study relations between QSA AVA (CsV ) and QSA variables v1 ,..., vn are updatable for S P1,..., n , S F1,..., n , and v v A A (CsV ' ) induced by the following two relations between V' SG1,..., n . sets of their names: Now we describe the main properties of superpositions. 1) there is a renomination bijection β : V  t →V ' , Lemma 1 (superposition folding). Let y = y1 ,..., yn , 2) V ' is an extension of V ( V ⊆ V ' ). f ' = f1 ',..., f n ' ; x = x1 ,..., xk , f = f1 ,..., f k , h ' = h1 ',..., hk ' , In the first case β induces in a natural way new v = v1 ,..., vm , h = h1 ,..., hm , { y1 ,..., yn } ∩ {v1 ,..., vm } = ∅. t mappings β P : PrAV  t → PrAV', β F : FnVA  → FnVA ' , and Then the following properties hold in AVA (CsV ) : SS P . S y , x ( S x ,v ( p, f , h ), f ', h ') = S y , x ,v ( p, σ ) , βG : PFAV  t → PFAV ' with the following properties. P P P ACIT 2018, June 1-3, 2018, Ceske Budejovice, Czech Republic 177 Theorem 1. Mappings βC , βP , βF , and βG define an set of terms Tr (ΣVQ ), and the set of programs Pg (ΣVQ ) are isomorphism of QSA AVA (CsV ) and QSA AVA ' (CsV ' ) . defined by induction in a traditional way. Theorem 2. Let V ⊆ V ' . Then inclusion mapping Interpretational component is defined in the following induces (ignoring variables from U = V ' \ V ) an injective way. Given ΣVQ =(CsV , Ps, Fs, Pgs) and a set A we can define homomorphism of AVA (CsV ) into AVA ' (CsV ) . a QSA AVA (CsV ) = < PrAV , FnVA , PFAV ; CsV > . Composition Now we can study an algebra with mappings over total data that “mimic” mappings over partial data. A special symbols have fixed interpretation, but we additionally need t t element ε (ε∉A) will represent a case when a value of a interpretations I Ps : Ps  → PrAV , I Fs : Fs  → FnVA , and variable or a function is undefined. Let Aε= A ∪ {ε } and t I Pgs : Pgs  → PFAV of predicate, function, and program t V → A ∪ {ε } . We construct a QSA A ε = V  AVA,ε (CsεV ) with function symbols respectively. A tuple total data that “mimics” QSA AVA (CsV ) . Carriers of the new J = (ΣQ , A, I , I , I ) is called an V Ps Fs Pgs LQ -interpretation. algebra are classes p PrAV,ε = AεV → Bool , Usually the prefix LQ is omitted. Given an interpretation J we denote meanings in J of a formula Φ , a term t , and a t p → Aε , and PFAV,ε = AεV → AεV . FnTAV,ε = AεV  program π respectively Φ J , t J , and π J . + V Then we define mapping ε D t : A  → AεV that “add ε LQ -formula Φ is satisfiable in an interpretation J if there exists an element d such that Φ J (d ) ↓= T . This is denoted into a nominative set. This mapping induces mappings ε+P , + LQ , J |≈ Φ . Formula Φ is satisfiable in the logic LQ ( LQ |≈ Φ ε+F , and εG relating corresponding carriers. ), if there exists an interpretation J such that LQ , J |≈ Φ . Theorem 3. Mappings ε+P , ε+F , and εG+ define an Formulas Φ and Ψ are equisatisfiable, if they are both isomorphism of AVA (CsV ) and AVA,ε (CsεV ) . satisfiable or both unsatisfiable. We treat n-ary operations as a special case of quasiary LQ -formula Φ is called valid in an interpretation J if there mappings with the set of variables N={1,…, n} and total is no d such that Φ J (d)↓= F. This is denoted LQ , J |= Φ, data. In this case a total nominative set [1  a1 ,..., n  an ] is which means that Φ is not refutable in J. A formula Φ is represented by a tuple (a1 ,..., an ) . Thus, all algebra mappings called valid in LQ if LQ , J |= Φ for any interpretation J. We are defined on a Cartesian product An. Compositions from shall denote this LQ |= Φ, or just |= Φ if the logic in hand is CsN can be treated as compositions over n-ary mappings. understood from the context. Here we do not redefine compositions in this style LQ -formulas Φ and Ψ are equivalent, if for every J assuming that it is a simple task. The term ‘unified’ means predicates Φ J and Ψ J are identical. Such notion of that all mappings have the same arity. equivalence can be also defined for terms and programs. Obtained algebra is called a unified n-ary specification Validity and satisfiability problems for QSL are related in algebra (NSA) and is denoted A NA (Cs N ) . The following the following way: Φ is valid in J if and only if ¬Φ is proposition is practically an immediate consequence of unsatisfiable in J. Theorems 1–3. Let N={1,…,n}. We treat a unified n-ary specification Theorem 4. Let V = {v1 ,..., vn } , N = {1,..., n} ( n ≥ 1 ), logic LN as a quasiary specification logic with a signature {1,..., n} β : V  t → N be a bijection, AVA (CsV ) be QSA and Σ nN =( Csn , Ps, Fs, Pgs) constructed over total A NA,ε (Cs N ) be NSA ( ε ∉ A ). Then mappings βC , βP  εP+ , nominative sets. This logic is semantically based on unified n-ary specification algebras. βF  εF+ , and βG  εG+ define an isomorphism of QSA AVA (CsV ) Now we will study a problem how to relate LQ and LN and NSA A NA,ε (Cs N ) . with respect to the satisfiability problem, namely, given LQ - IV. QUASIARY SPECIFICATION LOGIC formula Φ construct LN -formula Φ n such that Φ and Φ n will be equisatisfiable. We do this in several steps: To define a quasiary specification logic, denoted LQ , we have to specify its semantic, syntactic, and interpretational ─ introducing a logic LQU with unessential variables, components [4, 8]. ─ constructing a superpositional normal form Φ s of Φ in Semantic components of LQ is based on the class of LQU , quasiary specification algebras AVA (CsV ) for different A. ─ introducing a logic LQUR with finitely restricted sets of A syntactic component specifies the language of LQ updatable variables, constructed over signature ΣVQ = (CsV , Ps, Fs, Pgs ) where Ps, ─ constructing a unified superpositional normal form Φu of QUR Fs, and Pgs are respectively the sets of predicate symbols, Φ s in L , ordinary function symbols, and program function symbols. ─ constructing from Φ s a formula Φt of logic LQURT with total For simplicity, we use the same notation for symbols of data, compositions and compositions themselves. ─ translating Φt into LN -formula Φ n , For a given signature ΣVQ the set of formulas Fr (ΣVQ ) , the ACIT 2018, June 1-3, 2018, Ceske Budejovice, Czech Republic 178 ─ proving equisatisfiability of Φ and Φ n . features of software systems as partiality of data, partiality Logic LQ being a rather powerful logic still is not and unrestricted arity of predicate and functions, sensitivity to expressible enough to represent various important unassigned variables. For the constructed logics some laws of transformations. Therefore we introduce as its extension a classical logic fail. We have studied relations of quasiary logic with unessential variables denoted LQU . Here U is an logics to logics of n-ary mapping. Obtained results demonstrate that logics of quasiary mappings are more infinite set of variables such that V ∩U = ∅ . Unessential powerful and expressive than logics based on n-ary variables do not affect the meaning of formulas (terms, mappings. We have developed methods of reduction of the programs) [4,8]. An additional requirement is that satisfiability problems in quasiary logics to the satisfiability unessential variables are not updatable by programs. The problems for logics based on n-ary mappings. Such methods signature of LQU is ΣVQ,U = (CsV ∪U , Ps, Fs, Pgs). can be useful for construction and investigation of logics for The following statement is a consequence of Theorem 2. program reasoning. Lemma 5 ( LQU is a model-theoretic conservative extension Future work on the topic will include construction of of LQ ). Let LQU -interpretation J U be an calculi for important fragments of the considered logics. Also, a prototype of software systems for theorem proving in unessential extension of LQ -interpretation J , Φ ∈ Fr (ΣVQ ) , quasiary specification logics should be developed. First steps in this direction are made in [9, 10]. t ∈ Tr (ΣVQ ) , π ∈ Pg (ΣVQ ) . Then REFERENCES ιUP (Φ J ) = Φ J U , ιUF (t J ) = t J U , and ιGU (π J ) = π J U . [1] Handbook of Logic in Computer Science, S. Abramsky, Introduction of LQU permits to formulate transformations Dov M. Gabbay, and T. S. E. Maibaum (eds.), in 5 rules based on properties presented in Lemmas 1–4. volumes, Oxford Univ. Press, Oxford, 1993–2001. LQU -formula Φ is said to be in superpositional normal [2] D. Sannella, A. Tarlecki, “Foundations of Algebraic form, if the following conditions hold: Specification and Formal Software Development”, SP. For each subformula S Pv (Ψ, t ) of formula Φ we have Springer, 2012. that Ψ∈Ps; [3] N.(M.) Nikitchenko, “A Composition Nominative SF. For each subformula of the form S Fv (t , t ') we have that Approach to Program Semantics”. Technical Report t∈Fs; IT−TR 1998-020, Technical University of Denmark, 103 SG. For each subformula of the form SGv (π, t ) we have p., 1998. [4] M. Nikitchenko, V. Tymofieiev, “Satisfiability in that π = id . Composition-Nominative Logics”, Central European Lemma 6. Let Φ ∈ Fr (ΣVQ∪U ) . Then, using Journal of Computer Science, vol. 2, issue 3, 2012, pp. transformation specified by Lemmas 1-4, a superpositional 194-213. normal form Φ s of Φ can be constructed such that Φ s ≈ Φ . [5] M. Nikitchenko, S. Shkilniak, “Applied Logic”, In a similar way we can define transformations that first Publishing house of Taras Shevchenko National lead to a formula Φt of logic LQUR with total data and then to University of Kyiv, Kyiv, 2013 (in Ukrainian), 278 p. T [6] M. Nikitchenko, V. Tymofieiev, “Composition- formula Φ n of logic LN . Nominative Logics in Rigorous Development of Software V. REDUCTION OF THE SATISFIABILITY PROBLEM Systems”, LNBIP, vol. 137, pp. 140–151. Springer, Combining all obtained results, we can prove the Heidelberg, 2013. following main theorem that states reducibility of the [7] A. Kryvolap, M. Nikitchenko, W. Schreiner, “Extending satisfiability problem in quasiary specification logics with Floyd-Hoare logic for partial pre- and postconditions”, finitely restricted sets of updatable variables to the CCIS, vol. 412, pp. 355-378, Springer, Heidelberg, 2013. satisfiability problem in n-ary specification logics. [8] M. Nikitchenko, S. Shkilniak, “Algebras and logics of Theorem 5. Let Φ be a LQUR -formula and Φ n be a LN - partial quasiary predicates”, Algebra and Discrete formula obtained by the above-described transformations. Mathematics, vol. 23, number 2, 2017, pp. 263–278. Then Φ and Φ n are equisatisfiable. [9] I. Ivanov, M. Nikitchenko, A. Kryvolap, A. Kornilowicz, Results of such kind permit to use existing satisfiability “Simple-Named Complex-Valued Nominative Data – checkers for classical predicate and program logics, based on Definition and Basic Operations”, Formalized n-ary mappings, to check satisfiability of formulas for Mathematics, 25(3), pp. 205-216, 2017. quasiary logics. [10] A. Kornilowicz, A. Kryvolap, M. Nikitchenko, I. VI. CONCLUSION Ivanov, “Formalization of the nominative algorithmic algebra in Mizar”, Advances in Intelligent Systems and In this paper, we have developed special program Computing, vol. 656, pp. 176–186, Springer, 2017. specification algebras and logics defined for classes of quasiary mappings. These algebras and logics reflect such ACIT 2018, June 1-3, 2018, Ceske Budejovice, Czech Republic