In the paper we present special program specification algebras and logics defined for classes of quasiary mappings. Informally speaking, such mappings are partial mappings defined over partial states (partial assignments) of variables. Conventional n-ary mappings can be considered as a special case of quasiary mappings. Such mappings better reflect properties of software systems. We describe methods of reducibility of the satisfiability problem in quasiary logics to the satisfiability problem in logics of n-ary mappings. The methods proposed can be useful for software verification.
Algebraic approach to software system specification has
the following two characteristics: 1) the formalism of
manysorted algebras is used to model such systems; 2) special
logics based on such many-sorted algebras are used to reason
about system properties. In the literature various kinds of
such algebras and logics are described (e.g. see [
In this paper we present special algebras and logics defined for classes of quasiary mappings. Informally speaking, such mappings are partial mappings defined over partial states (partial assignments) of variables. Conventional n-ary mappings can be considered as a special case of quasiary mappings. Quasiary mappings better reflect properties of software systems therefore construction and investigation of algebras and logics of quasiary mapping is an important challenge.
Proposed constructions are based on a
compositionnominative approach [
The constructed program models form a base for developing special program logics called compositionnominative logics (CNL).
In this paper we continue our work on studying CNL [
Quasiary mappings can be met in different branches of mathematics, logics, and computer science. Informally speaking, such mappings appear when we use variables (names) to construct mapping arguments. Here we consider only usage of quasiary mappings in logic semantics and formal models of programs.
The notion of quasiary predicate and function can be easily understood when we analyze Tarski’s definition of first-order language semantics. This semantics is based on the notion of interpretation which consists of two parts: 1) interpretation of predicate and function symbols in some structure, and 2) interpretation of individual variables in the domain of this structure. The latter are usually called variable assignments (or valuations) and can be represented by total mappings from a set of individual variables (names) V into some set of basic values A. The class of such total mappings will be denoted V t → A or AV, and called total nominative sets. Thus, Tarski’s semantics interprets predicate and function symbols as total quasiary predicates and functions defined on the class AV of total nominative sets. In applications like model checking, program verification, automated theorem proving, etc., partial assignments (nominative sets) are often used instead of total assignments. The class of such partial mappings will be denoted V p→ A or VA, and called partial nominative sets (partial data); the term ‘partial is often omitted. Predicates and functions over nominative sets are called quasiary. This means that formulas and terms can be interpreted as quasiary predicates and functions respectively.
Quasiary mappings also appear in a natural way in denotational semantics of programs. In this semantics program states are represented as nominative sets, Boolean expressions as quasiary predicates of the type PrAV =VA p→ Bool, arithmetical expressions as quasiary functions of the type FnVA = VA p→ A, and program statements as biquasiary functions (program functions) of the type PFAV =VA p→ VA. Semantics of structured statements is defined by the following compositions with conventional meaning: assignment composition AS x (x is a parameter from V), composition of sequential execution •, conditional
SSF. S y,x (SFx,v ( f , f , h ), f ', h ') = S y,x,v ( f ,σ ) ,
F F SSG. S y,x (SGx,v (g, f , h ), f ', h ') = S y,x ,v (g,σ )) ,
G G where σ = ( f ', SFy,x ( f1, f ', h '),..., S y,x ( fk , f ', h '),
F S y,x (h1, f ', h '),..., S y,x (hm , f ', h ')).
F F
Lemma 2 (distributivity of superposition). The following properties hold in AVA (CsV ) :
S∨. S Pv ( p ∨ q, f ) =S Pv ( p, f ) ∨ S Pv (q, f ) , S¬. S Pv (¬p, f ) =¬S Pv ( p, f ) , S=. S Pv (h1
=h2 , f ) =(S Fv (h1, f ) =SFv (h2 , f )) .
S∃. S Pv (∃xp, f ) =∃u S Pv (SPx ( p, 'u), f ) , u≠x, u ∉ v , u is unessential for p and f , (here “u is unessential for p and f ” means that p(d ) ≅ p(d ') and f (d ) ≅ f (d ') for any d and d ' such that d ||−{u} = d ' ||−{u} ).
Superposition compositions are not distributive with respect to WH, therefore we simplify superpositions into program functions using the identity program function id.
Lemma 3 (superpositions with program functions). The following properties hold in AVA (CsV ) :
SG. S Gv (g, f ) =Gv(id S , f ) • g – superposition into program function,
SP. S Pv (g ⋅ p, f ) =S Gv (g, f ) ⋅ p – superposition with prediction composition.
Lemma 4 (superposition simplification). The following properties hold in AVA (CsV ) : composition IF, loop composition WH. For structural expressions we additionally use unary denomination composition ′x and various superpositions.
Thus, we obtain a program algebra with three carriers: quasiary predicates, quasiary functions, and bi-quasiary functions (program functions). Such algebras can be called algorithmic algebras.
To extend such algebras to program specification algebras
we add quantifiers and prediction composition ‘⋅’. Prediction
composition is simply a functional composition of a program
function and a predicate. This composition is strong enough
to represent Hoare assertions, and therefore, specification
algebras with these compositions are rather expressive [
In the rest of the paper we consider program specification algebras and logics of partial quasiary mappings.
To emphasize a mapping’s partiality/totality we write the sign p→ for partial mappings and the sign → for total t mappings. Given a partial mapping µ, µ ′: D p→ D′ , d, d′ ∈ D we write: – µ(d)↓ (µ(d)↑) to denote that µ is defined (undefined) on d; – µ(d)↓= d′ to denote that µ is defined on d with a value d′ ; – µ (d ) ≅ µ '(d ') to denote the strong equality.
We omit proofs and some details of complicated definitions.
III. QUASIARY SPECIFICATION ALGEBRAS
We use the following set of composition symbols parameterized by V: CsV = {∨, ¬, ∃x, ' x, S Pv1,...,vn , S Fv1,...,vn , = , S Gv1,...,vn , AS x , •, IF ,WH ,⋅}
Formal definitions of compositions can be found in [
P F G superpositions and represent substitutions of quasiary functions into a predicate, function, and program function respectively. We also denote such compositions as S Pv , S Fv , v SG .
A tuple AVA (CsV ) =FnVA < PrAV , , PFAV ;CsV > is called quasiary specification algebra (QSA) over V and A.
Variables used as composition parameters can be classified as essential in the sense that they can affect the result of composition application evaluation and as updatable in the sense that the values of these variables can change during evaluation. Variable x is essential for denomination composition ' x , variable x is updatable for ∃x and AS x , variables v1,..., vn are updatable for S v1,...,vn , S v1,...,vn , and P F S v1,...,vn .
G Now we describe the main properties of superpositions. Lemma 1 (superposition folding). Let v = v1,..., vm , h = h1,..., hm , {y1,..., yn} ∩{v1,..., vm} Then the following properties hold in AVA (CsV ) :
SSP. SPy,x (SPx,v ( p, f , h ), f ', h ') = S y,x,v ( p,σ ) , P =. ∅ superpositions x ∉ v , SFx,v (' x, f , h ) = f –
SE. SP ( p) = p , SF ( f ) = f , SG (g) = g – with empty parameter list,
SiD. if
S Fv (' x, f ) = ' x superpositions into denomination functions,
SwD. S x,v ( p, ' x, f ) = S Pv ( p, f ) , S x,v (h, ' x, f ) = S Fv (h, f )
P F – superpositions with denomination function,
ST.
S v ,x, y,z (ϕ , f , h, h ', f ') = S v , y,x,z (ϕ , f , h ', h, f ') ,
P P S v ,x, y,z ( f , f , h, h ', f ') = S v , y,x,z ( f , f , h ', h, f ') ,
F F S v ,x, y,z (g, f , h, h ', f ') = S v , y,x,z (g, f , h ', h, f ') –
G G transposition of parameters.
These properties will be used to construct superpositional normal forms for language expressions.
Now we study relations between QSA AVA (CsV ) and QSA AVA' (CsV ' ) induced by the following two relations between sets of their names: 1) there is a renomination bijection β :V t→V ' , 2) V ' is an extension of V ( V ⊆ V ' ).
In the first case β induces in a natural way new mappings β P : PrAV t→ PrAV ' , β F : FnVA t→ FnVA ' , and βG : PFAV t→ PFAV ' with the following properties.
Theorem 1. Mappings βC , βP , βF , and βG define an isomorphism of QSA AVA (CsV ) and QSA AVA' (CsV ' ) .
Theorem 2. Let V ⊆ V ' . Then inclusion mapping induces (ignoring variables from U = V ' \ V ) an injective homomorphism of AVA (CsV ) into AVA' (CsV ) .
Now we can study an algebra with mappings over total data that “mimic” mappings over partial data. A special element ε (ε∉A) will represent a case when a value of a variable or a function is undefined. Let Aε = A ∪{ε } and AεV= V t→ A ∪{ε } . We construct a QSA AVA,ε (CsεV ) with total data that “mimics” QSA AVA (CsV ) . Carriers of the new algebra are classes
PrAV,ε = AεV p→ Bool , FnTAV,ε = AεV t→ Aε , and PFAV,ε = AεV p→ AεV .
Then we define mapping ε D+ : V A t→ AεV that “add ε into a nominative set. This mapping induces mappings ε+P , ε+F , and εG+ relating corresponding carriers.
Theorem 3. Mappings ε+P , ε+F isomorphism of AVA (CsV ) and A A,ε (CsεV ) .
V , and εG+ define an
We treat n-ary operations as a special case of quasiary mappings with the set of variables N={1,…, n} and total data. In this case a total nominative set [1 a1,..., n an ] is represented by a tuple (a1,..., an ) . Thus, all algebra mappings are defined on a Cartesian product An. Compositions from CsN can be treated as compositions over n-ary mappings.
Here we do not redefine compositions in this style assuming that it is a simple task. The term ‘unified’ means that all mappings have the same arity.
Obtained algebra is called a unified n-ary specification algebra (NSA) and is denoted A NA (Cs N ) . The following proposition is practically an immediate consequence of Theorems 1–3.
Theorem 4. Let V = {v1,..., vn} , N = {1,..., n} ( n ≥ 1), β : V t→ N be a bijection, AVA (CsV ) be
QSA and A NA,ε (Cs N ) be NSA ( ε ∉ A ). Then mappings βC , βP εP+ , βF εF+ , and βG εG+ define an isomorphism of QSA AVA (CsV ) and NSA A NA,ε (Cs N ) .
To define a quasiary specification logic, denoted LQ , we
have to specify its semantic, syntactic, and interpretational
components [
Semantic components of LQ is based on the class of quasiary specification algebras AVA (CsV ) for different A.
A syntactic component specifies the language of LQ constructed over signature ΣVQ = (CsV , Ps, Fs, Pgs) where Ps, Fs, and Pgs are respectively the sets of predicate symbols, ordinary function symbols, and program function symbols. For simplicity, we use the same notation for symbols of compositions and compositions themselves.
For a given signature ΣVQ the set of formulas Fr(ΣVQ ) , the set of terms Tr(ΣVQ ), and the set of programs Pg(ΣVQ ) are defined by induction in a traditional way.
Interpretational component is defined in the following way. Given ΣVQ =(CsV , Ps, Fs, Pgs) and a set A we can define
I Ps : Ps t→ PrAV , a QSA AVA (CsV ) =FnVA < PrAV , , PFAV ; CsV > . Composition symbols have fixed interpretation, but we additionally need interpretations
function symbols J = (ΣVQ , A, I Ps , I Fs , I Pgs ) of predicate, function, and respectively.
is called an
program
A tuple LQ -interpretation.
Usually the prefix LQ is omitted. Given an interpretation J we denote meanings in J of a formula Φ , a term t , and a program π respectively
Φ J , tJ , and π J .
LQ -formula Φ is satisfiable in an interpretation J if there exists an element d such that Φ J (d ) ↓= T . This is denoted LQ , J |≈ Φ . Formula Φ is satisfiable in the logic LQ ( LQ |≈ Φ ), if there exists an interpretation J such that LQ , J |≈ Φ . Formulas Φ and Ψ are equisatisfiable, if they are both satisfiable or both unsatisfiable.
LQ -formula Φ is called valid in an interpretation J if there is no d such that ΦJ (d)↓= F. This is denoted LQ , J |= Φ, which means that Φ is not refutable in J. A formula Φ is called valid in LQ if LQ , J |= Φ for any interpretation J. We shall denote this LQ |= Φ, or just |= Φ if the logic in hand is understood from the context.
LQ -formulas Φ and Ψ are equivalent, if for every J predicates ΦJ and ΨJ are identical. Such notion of equivalence can be also defined for terms and programs.
Validity and satisfiability problems for QSL are related in the following way: Φ is valid in J if and only if ¬Φ is unsatisfiable in J.
Let N={1,…,n}. We treat a unified n-ary specification logic LN as a quasiary specification logic with a signature ΣnN =( Cs{n1,...,n} , Ps, Fs, Pgs) constructed over total nominative sets. This logic is semantically based on unified n-ary specification algebras.
Now we will study a problem how to relate LQ and LN with respect to the satisfiability problem, namely, given LQ formula Φ construct LN -formula Φn such that Φ and Φn will be equisatisfiable. We do this in several steps: ─ introducing a logic LQU with unessential variables, ─ constructing a superpositional normal form Φs of Φ in ─ introducing a logic LQUR with finitely restricted sets of updatable variables, ─ constructing a unified superpositional normal form Φu of LQU , Φs in LQUR , ─ constructing from Φs a formula Φt of logic LQUR with total T data, ─ translating Φt into LN -formula Φn , ─ proving equisatisfiability of Φ and Φn .
Logic LQ being a rather powerful logic still is not
expressible enough to represent various important
transformations. Therefore we introduce as its extension a
logic with unessential variables denoted LQU . Here U is an
infinite set of variables such that V ∩ U = ∅ . Unessential
variables do not affect the meaning of formulas (terms,
programs) [
Q
The following statement is a consequence of Theorem 2. Lemma 5 ( LQU is a model-theoretic conservative extension of LQ ). Let LQU -interpretation JU be an unessential extension of LQ -interpretation J , Φ ∈ Fr(ΣVQ ) , t ∈Tr(ΣVQ ) , π ∈ Pg(ΣVQ ) . Then
ιUP (ΦJ ) = ΦJU , ιUF (tJ ) = tJU , and ιGU (πJ ) = πJU .
Introduction of LQU permits to formulate transformations rules based on properties presented in Lemmas 1–4.
LQU -formula Φ is said to be in superpositional normal form, if the following conditions hold:
SP. For each subformula SPv (Ψ, t ) of formula Φ we have that Ψ∈Ps;
SF. For each subformula of the form SFv (t, t ') we have that t∈Fs;
SG. For each subformula of the form SGv (π, t) we have that π = id .
Lemma using transformation specified by Lemmas 1-4, a superpositional normal form Φs of Φ can be constructed such that Φs ≈ Φ .
In a similar way we can define transformations that first lead to a formula Φt of logic LQUR with total data and then to T formula Φn of logic LN .
V. REDUCTION OF THE SATISFIABILITY PROBLEM Combining all obtained results, we can prove the following main theorem that states reducibility of the satisfiability problem in quasiary specification logics with finitely restricted sets of updatable variables to the satisfiability problem in n-ary specification logics.
Theorem 5. Let Φ be a LQUR -formula and Φn be a LN formula obtained by the above-described transformations. Then Φ and Φn are equisatisfiable.
Results of such kind permit to use existing satisfiability checkers for classical predicate and program logics, based on n-ary mappings, to check satisfiability of formulas for quasiary logics.
In this paper, we have developed special program specification algebras and logics defined for classes of quasiary mappings. These algebras and logics reflect such features of software systems as partiality of data, partiality and unrestricted arity of predicate and functions, sensitivity to unassigned variables. For the constructed logics some laws of classical logic fail. We have studied relations of quasiary logics to logics of n-ary mapping. Obtained results demonstrate that logics of quasiary mappings are more powerful and expressive than logics based on n-ary mappings. We have developed methods of reduction of the satisfiability problems in quasiary logics to the satisfiability problems for logics based on n-ary mappings. Such methods can be useful for construction and investigation of logics for program reasoning.
Future work on the topic will include construction of
calculi for important fragments of the considered logics.
Also, a prototype of software systems for theorem proving in
quasiary specification logics should be developed. First steps
in this direction are made in [