We describe the theory of nominative data, formulate the basic principles of the composition-nominative approach, and define the class of nominative data and functions. By using nominative data, we can increase the level of adequacy of representation data structures, functions, and compositions that are used in programming languages. Thus, in terms of composition-nominative approach, we can build systems of verification of programs based on a unified conceptual basis. Computer-aided verification of computer programs often uses SMT (satisfiability modulo theories) solvers. A common technique is to translate preconditions, postconditions, and assertions into SMT formulas in order to determine if required properties can hold. The SMT-LIB Standard was created for forming a common standard and library for solving SMT problems. Now, it is one of the most used libraries for SMT systems. Formulas in SMT-LIB format are accepted by the great majority of current SMT solvers. The theory of nominative data is of interest for software modelling and verification, but currently lacks support in the SMT-LIB format. In the article, we propose the declaration for the theory of nominative data for the SMT-LIB Standard 2.6. The goal is the development of SMT solvers with nominative data support.
Composition programming studies the systems at different levels of abstraction –
abstract, Boolean, and nominative (attribute) levels. Systems of the last level, based
on the composition-nominative methods [
It is therefore natural to expect program analysis and verification tools to be able to reason about programs, by means of deciding the validity of formulas containing variables of such types. Application of such tools requires a standard exchange format for these types of formulas.
Dafny [
The standardization of formats in logic has played a major role in accelerating
research in the past. Examples for successful standardization efforts are the DIMACS
format for Boolean formulas in conjunctive normal form (CNF), and the SMT-LIB
format [
SMT-LIB was created in 2003 with the expectation that the availability of common standards and a library of benchmarks would greatly facilitate the evaluation and the comparison of SMT (satisfiability modulo theories) systems. Now, SMT-LIB contains more than 100,000 benchmarks and continues to grow. Formulas in SMT-LIB format are accepted by the great majority of current SMT solvers.
In computer science and mathematical logic, the satisfiability modulo theories problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on. SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalized approach to constraint programming.
The following systems (listed alphabetically) were under active development in
2018: Alt-Ergo, AProVE, Boolector, CVC4, MathSAT 5, OpenSMT 2, raSAT,
SMTInterpol, SMT-RAT, STP, veriT, Yices 2, Z3 [
A new sublogic, or simply logic, is defined in the SMT-LIB language by a logic
declaration. Logic declarations have a similar format to theory declarations. Attributes
with the following predefined keywords are predefined attributes, with prescribed
usage and semantics in logic declarations [
Additionally a logic declaration can contain any number of user-defined attributes.
<logic_attribute> := :theories ( <symbol> + )
| :language <string>
| :extensions <string>
| :values <string>
| :notes <string>
| <attribute>
<logic> ::= ( logic <symbol> <logic_attribute> + )
SMT-LIB logics refer to one or more theories:
Functional arrays with extensionality (ArraysEx),
Bit vectors with arbitrary size (FixedSizeBitVectors),
Core theory, defining the basic Boolean operators (Core),
Floating point numbers (FloatingPoint),
Integer numbers (Ints),
Real numbers (Reals),
Real and integer numbers (Reals_Ints) [
We propose to add a theory of nominative data to SMT-LIB, serving as a standard format for formulas that include operations on nominative data. 2
One of the approaches to software specification is composition programming [
Thus, the composition-nominative approach provides a single methodological basis
to formalize the concept of program specification, bringing their features and their
further specification to programming languages of the lower level. This approach is
based on the following principles [
Development principle (from abstract to concrete): program notions should be introduced as a process of their development that starts from abstract understanding, capturing essential program properties, and proceeds to more concrete considerations.
The principle of priority of semantics over syntax: program semantic and syntactic aspects should be first studied separately, then in their integrity in which semantic aspects prevail over syntactic ones. 3
of nominative data is constructed by the following recursive definition → ),
Compositionality principle: programs can be constructed from simpler programs (functions) with the help of special operations, called compositions, which form a kernel of program semantics structures.
Nominativity principle: nominative (naming) relations are basic ones in constructing data and programs.
Here we have formulated only principles relevant to the topic of the article. A
richer system of principles is developed in [
It is demonstrated [
is the class of partial multi-valued (non-deterministic) functions.
For nominative data representation we use the form = [ ↦ | ∈ ], where is some set of indices. Nominative membership relation is denoted by ∈ . Thus, ↦ ∈
means that the value of in is defined and is equal to ; this can be written in another form as ( ) ↓= . The class \ is called the class of proper nominative data, or hierarchical nominative data; data from the class will be → called flat nominative data, or nominative sets
Main functions over the nominative data are the following functions: naming and denaming of
with a parameter ∈ , and binary operations and predicates, such as: union ∪D, subtraction \ , equality (= ) on . The function of construction of the empty nominative data [ ] , predicate of membership on : ∈ are also defined. Operation of renaming for the nominative data ([ 1 ↦ 1, … , ↦ , … ]) yields [ 1 ↦ 1, … ,
↦ , … ]. The main compositions of functions over nominative data are binary compositions: multiplication ° , iteration ∗ , merging and branching ternary composition . It is shown that the composition of multiplication corresponds to the consecutive application of functions, composition of branching – to the conditional operator if-then-else of programming languages, composition of iteration ∗ – to operator until-do, and composition of merging connecs nominative data resulting from function-arguments.
The special kind of computability – nominative computability – is introduced for
consideration and studied in [
{0, 1, [ ] , ,∪ , (= ) , , , ∈ }
Axiomatic theory of nominative data [
The class of 0 - formulas is the smallest class , containing the basic formulas and closed under the following rules: 1) if ∈ , then also ¬ ∈ , 2) if, , ∈ , then ∈ and ∈ , 3) if ∈ , then ↦ , ∃ → ∈ Y for all variables , , .
Class of -formulas is the smallest class , containing 0-formulas and closed in relation to the conditions 2) and 3) determining the class of 0-formulas and further conditions of existential quantification: if ∈ , then ∃ ∈ . 4
The theory of nominative data is of interest for software modelling and verification,
but currently lacks support in the SMT-LIB format. Therefore, we propose the theory
of nominative data for the SMT-LIB Standard 2.6 [
For convenience, the definition of nominative data in the SMT-LIB Standard is presented via the concepts of nominative pair ( ↦ y) and nominative set ([ 1 ↦ 1, … , ↦ , … ]). Nominative pair of two typed elements are the most basic collection datatype that we propose for an SMT-LIB theory. Semantically, assuming that the type 1 denotes the non-empty domain (name) and the type 2 denotes the domain (value) , the type denotes the domain ↦ . Table 1 contains all proposed operations on nominative pairs in mathematical and in concrete SMTLIB notation.
This table gives a signature of the proposed SMT-LIB theory of nominative pairs. In the first column of Table 1, we specify a mathematical notation for the functions used with nominative pairs. In the mathematical notation, we use the following notation: or are names in the nominative pairs, is the value in the nominative pair, and is the nominative pair. In the second column of Table 1, we specify a proposed SMT-LIB notation for each operation. In the third column of Table 1, we specify a signature for each operation. In the signature definition, we use the following notation: is a set of names in nominative pairs, and is a set of values in nominative pairs. :sorts ((Int 1) (NdPair 2))) :funs (
Note, that the type of an -ary predicate SMT-LIB is in specified by an −tuple ( 1 … ), while the type of an -ary function with result type 0 is given by an A Declaration for a nominative pair for theory of nominative data for the SMT-LIB (par (X Y) (ndpair X Y (NdPair X Y))) (par (X Y) (naming X Y (NdPair X Y))) (par (X Y) (pairrenaming
(NdPair X Y) X (NdPair X Y))) (par (X Y) (pairnameequal (NdPair X Y) (NdPair X Y) Bool)) (par (X Y) (pairvalueequal (NdPair X Y) (NdPair X Y) Bool)) (par (X Y) (pairequal (NdPair X Y) (NdPair X Y) Bool)))) :definition "Let Q be a set of sort symbols including NdPair and Bool, and let S be the set of all (ground) sort terms over Q. For any s in S and any function symbol f, let [[s]] and [[f]] respectively denote the interpretation of s and f in some given structure.
For any S like the above, NominativePair(S) is the theory consisting of all structures satisfying the following restrictions for all s, s' in S: - [[(NdPair s s')]] is the pair from [[s]] to [[s']]. - For all name n and data d
[[naming]](n, d) = [[(NdPair n d)]]. - For all nominative pair p from [[n]] to [[v]] and all name x [[paitrenaming]](p, x) = [[(NdPair x v)]].
- For all nominative pairs a from [[n1]] to [[v1]] and nominative pair b from [[n2]] to [[v2]],
Nominative set of nominative pairs is the collection datatype that we propose for SMT-LIB theory. Semantically, the nominative set types denote sets NdSet(A, B) of finite partial functions. The Table 2 contains all proposed operations on nominative sets in mathematical and in concrete SMT-LIB notation. This table gives a signature of the proposed SMT-LIB theory of nominative set.
In the first column of Table 2, we specify a mathematical notation for the functions used with nominative data. In the mathematical notation, we use the following notation: or are names in the nominative pairs, is the value in the nominative pair, and is the nominative set. In the second column of Table 2, we specify a proposed SMT-LIB notation for each operation. In the third column of Table 2, we specify a signature for each operation. In the signature definition, we use the following notation: is a set of names in nominative pairs, is a set of values in nominative pairs, and is a set of nominative pairs. :sorts ((Int 1) (NDSet 2)) :funs (((par (X) (emptyNdSet (NdSet X))) (par X) (naming X X (NdSet X) (NdSet X) :right_assoc) (par X) (denaming X (NdSet X) (NdSet X) :right_assoc) (par (X) (ndin (NdPair(X Y)) (NdSet Z) Bool)) (par (X) (ndsubset (NdSet X) (NdSet X) Bool :chainable)) (par (X) (ndunion (NdSet X) (NdSet X) (NdSet X) :right_assoc)) (par (X) (ndoverlay (NdSet X) (NdSet X) (NdSet X) :right_assoc)) (par (X) (ndsetminus (NdSet X) (NdSet X) (NdSet X) :right_assoc)) (par (X) (ndequal (NdSet X) (NdSet X) Bool :chainable)) (par (X (renaming X X (NdSet X) (NdSet X) :right_assoc)) :definition "Let Q be a set of sort symbols including Set, Int, and Bool, and let S be the set of all (ground) sort terms over Q. For any s in S and any function symbol f, let [[s]] and [[f]] respectively denote the Interpretation of s and f in some given structure.
For any S like the above, NominativeSet(S) is the theory consisting of all structures satisfying the following restrictions for all s in S: - [[(Set s)]] is the set of all finite subsets of [[s]]. - [[f]] is as expected if f is in {subset, in}.
- [[(NdSet s s')]] is the nominative set of all finite partial maps from [[s]] to [[s']].
- [[emptyNdSet]] is the function from [[s]] to [[s']] undefined everywhere.
- For all nominative sets m and name x,
[[naming]](x, m) = [[(NdPair x m)]] is the nominative set of all finite partial maps from [[x]] to [[m]].
- For all n > 0, nominative set a and nominative set b of [[b1]], ..., [[bn]], [[ndsubset]](b, a) = true if bi ndin a for all i = 1, ..., n false otherwise.
- For all n, m > 0, nominative set a of [[a1]], ..., [[an]] and nominative set b of [[b1]], ..., [[bm]],
[[ndunion]](b, a) = [[a1],…[an],[b1],…,[bm]].
- For all n, m > 0, nominative set a of [[(NdPair a1 b1)],…[( NdPair an bn)]] and nominative set b, [[ndoverlay]](a, b) = [[ndunion](b, { x indn [[(NdPair a1 b1)],…[( NdPair an bn)]] | there in not any d (NdPair ai d) ndin b })].
- For all k > 0, nominative set a of [[a1]], ..., [[an]] and nominative set b of [[b1]], ..., [[bm]], [[ndsetminus]](a, b) = {x ndin [[s1],…[sk]] | for all i <=k si idin a and not (si indin b)}.
- For all nominative set a of [[(NdPair a1 b1)],…[( NdPair an bn)]] and name x, [[renaming]](x, y, a) ={x ndin [[(NdPair a1 b1)],… [( NdPair am bm)]] | for all i<=m ([(NdPair ai bi)] dnin [[(NdPair a1 b1)],… [( NdPair an bn)]]) and (not ai = x) } ndunion { [[(NdPair y bj)] | [[(NdPair x bj)] ndin [[(NdPair a1 b1)],…[( NdPair an bn)]]}.
- For all k > 0, nominative set a [[a1]], ..., [[an]] and nominative set b, [[ndsubset]](a, b) = true false if for all i <=n ai idin b otherwise. - For all nominative sets a, b
[[ndequal]](a, b) = (a ndsubset b) and (b ndsubset a). - [[n]] is as expected if n is a numeral. - [[(NdSet s)]] is the set of all finite subsets of [[s]]. - [[f]] is as expected if f is in { emptyNdSet, naming, denaming, ndin, ndsubsetm ndunion, ndoverlay, ndsetminus, ndsubset, ndequal, renaming}. ")
Using proposed by the authors the SMT-LIB theory of nominative data, we can adequately determine the structure of programming data and operations on them.
For example, the following statement in terms of the theory of nominative data: ∀ ∃ ( ∈ ) can be specified in the form of the following SMT- LIB notation:
(forall ((a (NdPair Int))) (exists ((s (NdSet Int))) (ndin a s)))
The link to https://sites.google.com/knu.ua/nominative-data contains information
that relates the description of Extended SMT-Lib Standard with Theory of
Nominative Data [
In the article, we have proposed the extension of the SMT-LIB Standard with theory of nominative data. This theory is of interest for software modelling and verification. At the same time, the declaration for the SMT-LIB Standard for the theory of nominative data has not yet been proposed.
To construct the extension of the SMT-LIB Standard for the constructed theory of
nominative data, we have described the main principles of the
compositionnominative approach and the definition of the class of nominative data. Such data
form a basis for adequate definition of data structures, functions, and compositions of
programming languages [
We are developing SMT solvers with nominative data support. In the forthcoming articles we will demonstrate applications of the proposed theory.