1M. Cristiá and G. Rossi$\\{log\\}$: Set Formulas as Programs $\\{log\\}$ is a
programming language at the intersection of Constraint Logic Programming, set
programming and declarative programming. But $\\{log\\}$ is also a
satisfiability solver for a theory of finite sets and finite binary relations.
With $\\{log\\}$ programmers can write abstract programs using all the power
of set theory and binary relations. These programs are not very efficient but
they are very close to specifications. Then, their correctness is more
evident. Furthermore, $\\{log\\}$ programs are also set formulas. Hence,
programmers can use $\\{log\\}$ again to automatically prove their programs
verify non trivial properties. In this paper we show this development
methodology by means of several examples.

#  $\\{log\\}$: Set Formulas as Programs

Maximiliano Cristiá and Gianfranco Rossi

(Month dd, yyyy
Revised Month dd, yyyy
Accepted Month dd, yyyy)

###### keywords:

set theory, declarative programming, set programming, formal verification,
$\\{log\\}$

MSClassification, separated, by, commas

##  1 Introduction

In 1999 Apt and Bezem [AB99] proposed a programming paradigm based on the
concept of _formulas as programs_ as an alternative approach to _formulas as
types_ or _proofs as programs_ [BC85, CH88, Tho91]. In the latter approach,
formal proofs of properties about the correct behavior of a program contain a
Lambda calculus term (i.e., a program) which is a correct implementation of
that behavior. Hence, by proving properties concerning the behavior of a
program one gets in addition correct programs for free. In the ’formulas as
programs’ approach, the formula (specification) is itself a program. No formal
proof is needed to get a program, but the specification might not verify some
desired properties making the program faulty. Clearly, both approaches have
their advantages and disadvantages. For example, in the ’proofs as programs’
approach one have the first version of the program after performing a formal
proof of some property and extracting the Lambda term (which is not always
easy), but this first version is correct by construction. On the other hand,
in the ’formulas as programs’ approach one quickly have a first version of the
program but it can be wrong, although it can be improved by experimenting with
it.

Set theory is deemed as a good vehicle to concisely and accurately describe
algorithms and software systems. Formal specification languages such as Z
[Spi92], B [Sch01], TLA+ [BRHR18] and VDM [Jon91] support this claim. In this
paper we show how set-based specifications can be made to fit in the ‘formulas
as programs’ paradigm.

$\\{log\\}$ is a constraint logic programming (CLP) language which provides
the fundamental forms of set designation, along with a number of basic
operations for manipulating them, as first-class entities. Various new
features have been added to the core part of the language since the initial
development of $\\{log\\}$ [DOPR96]. Among them, basic facilities for
representing and manipulating integer expressions (integrating the CLP(FD) and
CLP(Q) solvers), binary relations, partial functions, Cartesian products and
restricted intensional sets. But $\\{log\\}$ is also a _satisfiability
solver_. The CLP language and the satisfiability solver are two sides of the
same and only system. That is, $\\{log\\}$ is not the integration of a CLP
interpreter with a satisfiability solver; instead, it is based on mathematical
and computational models that produce such a tool.

This means that a piece of $\\{log\\}$ code is both _a program and a formula_.
We call this the _program-formula duality_. Therefore, when $\\{log\\}$
programmers write code they are writing both a program and a formula. In other
words, they are writing a program _as a_ formula. When seen as a program,
programmers can execute it; when seen as a formula, they can _automatically_
prove properties true of it. Hence, a $\\{log\\}$ programmer writes some code
and execute it to see how it works. If everything goes right, (s)he can use
$\\{log\\}$ again to automatically prove properties of that program. All with
the same and only formal text and with the same and only tool. Once a
$\\{log\\}$ program is shown to verify some property, we can be sure that all
of its executions are correct with respect to that property.

However, $\\{log\\}$ has some limitations. $\\{log\\}$ programs perform poorly
compared with logic, functional or imperative programs. We see $\\{log\\}$
programs as _functional prototypes_ or _executable specifications_. Not every
property true of a $\\{log\\}$ program can be automatically proved with
$\\{log\\}$. Further, proving some properties may take too much computing time
making the process unpractical. The capacity of $\\{log\\}$ in automatically
proving properties depends on the program-formula fitting inside of the
decision procedures implemented by the tool.

In this paper we will show this program-formula duality through some revealing
examples.

##  2 $\\{log\\}$

$\\{log\\}$ is a publicly available satisfiability solver and a set-based,
constraint-based programming language implemented in Prolog [Ros21].

$\\{log\\}$ implements a decision procedure for the theory of _hereditarily
finite sets_ ($\mathcal{SET}$), i.e., finitely nested sets that are finite at
each level of nesting [DPPR00]; a decision procedure for a very expressive
fragment of the theory of finite set relation algebras ($\mathcal{BR}$)
[CR20b, CR18]; a decision procedure for the theory of finite sets with
restricted intensional sets ($\mathcal{RIS}$) [CR17, CR21b]; a decision
procedure for the theory of hereditarily finite sets extended with cardinality
constraints ($\lvert\cdot\rvert$); a decision procedure for the latter
extended with integer intervals ($\lvert\cdot\rvert$); and uses Prolog’s
CLP(Q) to provide a decision procedure for the theory of integer linear
arithmetic [HMB96]. All these procedures are integrated into a single solver,
implemented in Prolog, which constitutes the core part of the $\\{log\\}$
tool. Several in-depth empirical evaluations provide evidence that $\\{log\\}$
is able to solve non-trivial problems [CR20b, CR18, CR17, CRF13]; in
particular as an automated verifier of security properties [CR21a, CR20a].

Figure 1 schematically describes the stack of the first-order theories
supported by $\\{log\\}$. The fact that a theory $T$ is over a theory $S$
means that $T$ extends $S$. E.g., CARD extends both LIA and SET. Figure 2
shortly describes the considered theories, showing for each of them the main
constant, function and predicate symbols. The precise definition of the first-
order logic languages on which the theories are based on are given in Appendix
A.

LIASETCARDRISRAINTERVALARRAYLIST

Legend

decidableundecidablework in progress

Figure 1: The stack of theories dealt with by $\\{log\\}$

  * •

LIA: Linear Integer Arithmetic (i.e., the theory that allows inequalities over
sums of constant multiples of variables).
Symbols: $\langle\mathsf{Z},+,*,-,=,\leq\rangle$, where $\mathsf{Z}$ is the
set of integer constants.

  * •

SET: Hereditarily finite hybrid untyped extensional sets.
Symbols:
$\langle\mathsf{U},\\{\\},\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\},=,\neq,\in,\notin,\cup,\parallel\rangle$,
where $\mathsf{U}$ is the set of ur-elements, i.e., non-set objects that are
used as set elements, and $\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\}$ is a
binary function symbol which serves as the extensional set constructor.

  * •

CARD: Hereditarily finite hybrid untyped extensional sets with cardinality.
Symbols: $\langle\mathsf{Z},+,*,-,=,\leq\rangle$,
$\langle\mathsf{U},\\{\\},\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\},=,\neq,\in,\notin,\cup,\parallel,|\cdot|\rangle$.

  * •

RIS: Hereditarily finite hybrid untyped extensional and intensional sets.
Symbols:
$\langle\mathsf{U},\\{\\},\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\},\\{\cdot|\cdot@\cdot\\},=,\neq,\in,\notin,\cup,\parallel\rangle$,
where $\\{\cdot|\cdot@\cdot\\}$ is a ternary function symbol which serves as
the intensional set constructor.

  * •

RA: Finite set relation algebras over discrete universe.
Symbols:
$\langle\mathsf{U},\\{\\},\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\},(\cdot,\cdot),=,\neq,\in,\notin,\cup,\parallel,\mathop{\mathrm{id}},\mathbin{\raise
2.58334pt\hbox{\small\oalign{\hfil$\scriptscriptstyle\mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}},{}^{\smile}\rangle$

  * •

INTERVAL: Hereditarily finite hybrid untyped extensional sets and integer
intervals with cardinality.
Symbols: $\langle\mathsf{Z},+,*,-,=,\leq\rangle$,
$\langle\mathsf{U},\\{\\},\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\},[\cdot,\cdot],=,\neq,\in,\notin,\cup,\parallel,|\cdot|\rangle$

  * •

ARRAY: Arrays encoded as binary relations.
Symbols: $\langle\mathsf{Z},+,*,-,=,\leq\rangle$,
$\langle\mathsf{U},\\{\\},\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\},\\{\cdot|\cdot@\cdot\\},[\cdot,\cdot],(\cdot,\cdot),=,\neq,\in,\notin,\cup,\parallel,|\cdot|,\mathop{\mathrm{id}},\mathbin{\raise
2.58334pt\hbox{\small\oalign{\hfil$\scriptscriptstyle\mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}},{}^{\smile}\rangle$

  * •

LIST: Lists encoded as binary relations.
Symbols: $\langle\mathsf{Z},+,*,-,=,\leq\rangle$,
$\langle\mathsf{U},\\{\\},\\{\cdot\mathbin{\scriptstyle\sqcup}\cdot\\},\\{\cdot|\cdot@\cdot\\},[\cdot,\cdot],(\cdot,\cdot),=,\neq,\in,\notin,\cup,\parallel,|\cdot|,\mathop{\mathrm{id}},\mathbin{\raise
2.58334pt\hbox{\small\oalign{\hfil$\scriptscriptstyle\mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}},{}^{\smile}\rangle$

Figure 2: The theories dealt with by $\\{log\\}$

The integrated constraint language offered by $\\{log\\}$ is a quantifier-free
first-order predicate language with terms of two sorts: terms designating sets
and terms designating ur-elements. Terms of either sort are allowed to enter
in the formation of _set terms_ (in this sense, the designated sets are
hybrid), no nesting restrictions being enforced (in particular, membership
chains of any finite length can be modeled).

Set terms in $\\{log\\}$ can be of the following forms:

  * •

A variable is a set term; variable names start with an uppercase letter.

  * •

$\\{\\}$ is the term interpreted as the empty set.

  * •

$\\{x/A\\}$ is called _extensional set_ and is interpreted as $\\{x\\}\cup A$;
$A$ must be a set term, $x$ can be any term accepted by $\\{log\\}$
(basically, any Prolog uninterpreted term, integers, ordered pairs, other set
terms, etc.).111Note that $\\{\leavevmode\vbox{\hrule
width=5.0pt}/\leavevmode\vbox{\hrule width=5.0pt}\\}$ is the concrete syntax
for the (abstract) set term $\\{\leavevmode\vbox{\hrule
width=5.0pt}\mathbin{\scriptstyle\sqcup}\leavevmode\vbox{\hrule
width=5.0pt}\\}$ of Figure 2.

As a notational convention, set terms of the form
$\\{t_{1}/\\{t_{2}\,/\,\cdots\\{t_{n}/t\\}\cdots\\}\\}$ are abbreviated as
$\\{t_{1},t_{2},\dots,t_{n}/t\\}$, while
$\\{t_{1}/\\{t_{2}\,/\,\cdots\\{t_{n}/\\{\\}\\}\cdots\\}\\}$ is abbreviated as
$\\{t_{1},t_{2},\dots,t_{n}\\}$.

  * •

$\mathsf{ris}(X\mathbin{\mathsf{in}}A,\phi)$ is called _restricted intensional
set_ (RIS) and is interpreted as $\\{x:x\in A\mathrel{\wedge}\phi\\}$ where
$\phi$ is any $\\{log\\}$ formula, $A$ must be a set term, and $X$ is a bound
variable local to the RIS. Actually, RIS have a more complex and expressive
structure [CR17, CR21b].

  * •

$\mathsf{cp}(A,B)$ is interpreted as $A\times B$, i.e., the Cartesian product
between $A$ and $B$.

  * •

$\mathsf{int}(A,B)$ is interpreted as $\\{x\in{\bbold Z}|A\leq x\leq B\\}$.

Set terms can be combined in several ways: binary relations are hereditarily
finite sets whose elements are ordered pairs and so set operators can take
binary relations as arguments; RIS and integer intervals can be passed as
arguments to set operators and freely combined with extensional sets.
$\\{log\\}$ is an untyped formalism; variables are not declared; typing
information can be encoded by means of constraints.222Recently, a type system
and a type checker have been added to the base language for those users who
feel more comfortable with typed formalisms.

Set operators are encoded as atomic predicates, and are dealt with as
constraints. For example: $\mathsf{un}(A,B,C)$ is a constraint interpreted as
$C=A\cup B$. $\\{log\\}$ implements a wide range of set and relational
operators covering most of those used in Z. For instance,
$\mathbin{\mathsf{in}}$ is a constraint interpreted as set membership (i.e.,
$\in$); $=$ is set equality; $\mathsf{dom}(F,D)$ corresponds to
$\mathop{\mathrm{dom}}F=D$; $\mathsf{subset}(A,B)$ corresponds to $A\subseteq
B$; $\mathsf{comp}(R,S,T)$ is interpreted as $T=R\mathbin{\raise
2.58334pt\hbox{\small\oalign{\hfil$\scriptscriptstyle\mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}}S$
(i.e., relational composition); and $\mathsf{apply}(F,X,Y)$ is equivalent to
$\mathsf{pfun}(F)\And[X,Y]\mathbin{\mathsf{in}}F$, where $\mathsf{pfun}(F)$
constrains $F$ to be a (partial) function.

A number of other set, relational and integer operators (in the form of
predicates) are defined as $\\{log\\}$ formulas, thus making it simpler for
the user to write complex formulas. Dovier et al. [DPPR00] proved that the
collection of predicate symbols $\\{=,\neq,\in,\notin,\cup,\parallel\\}$ is
sufficient to define constraints implementing the set operators $\cap$,
$\subseteq$ and $\setminus$. This result has been extended to binary relations
[CR20b] by showing that adding to the previous collection the predicate
symbols $\\{\mathop{\mathrm{id}},\mathbin{\raise
2.58334pt\hbox{\small\oalign{\hfil$\scriptscriptstyle\mathrm{o}$\hfil\cr\hfil$\scriptscriptstyle\mathrm{9}$\hfil}}},{}^{\smile}\\}$
is sufficient to define constraints for most of the classical relational
operators, such as $\mathop{\mathrm{dom}}$, $\mathop{\mathrm{ran}}$, , , etc..
Similarly, $\\{=,\neq,\leq\\}$ is sufficient to define $<$, $>$ and $\geq$. We
call predicates defined in this way, _derived constraints_.

######  Remark 2.1.

Establishing which predicates can be expressed as derived constraints and
which, on the contrary, cannot is a critical issue. Primitive constraints are
processed by possibly recursive _ad hoc_ rewriting procedures, that allow one
to implement a form of universal quantification which is not provided by the
language. Conversely, derived constraints are processed by simply replacing
them by quantifier-free first order formulas.

Choices about primitive vs. derived constraints can be different. For example,
in [CR16] we use $\mathsf{dom}$ and $\mathsf{ran}$ in place of $\mathsf{inv}$
and $\mathsf{id}$. However, since the $\mathsf{inv}$ predicate for binary
relations appears not to be definable in terms of the other primitive
predicates, $\mathsf{inv}$ has been included as a primitive constraint in
later work [CR20b], to enlarge the expressiveness of the constraint language.
At the same time, $\mathsf{dom}$ and $\mathsf{ran}$ are moved out of the
primitive constraints, since they turn out to be definable in terms of
$\mathsf{id}$, $\mathsf{comp}$ and $\mathsf{inv}$, thus reducing the number of
primitive constraints.

Proving that the selected collection of primitive constraints is the minimal
one, as well as comparing one choice to another in terms of, e.g., expressive
power, completeness, effectiveness, and efficiency, is a challenging issue for
future work.∎

Negation in $\\{log\\}$ is introduced by means of so-called _negated
constraints_. For example $\mathsf{nun}(A,B,C)$ is interpreted as $C\neq A\cup
B$ and $\mathbin{\mathsf{nin}}$ corresponds to $\notin$—in general, a
constraint beginning with ‘$\mathsf{n}$’ identifies a negated constraint. Most
of these constraints are defined as derived constraints in terms of the
existing primitive constraints; thus their introduction does not really
require extending the constraint language. For formulas to fit inside the
decision procedures implemented in $\\{log\\}$, users must only use this form
of negation.

Formulas in $\\{log\\}$ are built in the usual way by using conjunctions
($\&$) and disjunctions ($\mathbin{\mathsf{or}}$) of atomic constraints.

######  Example 2.2.

The following are two simple formulas accepted by $\\{log\\}$:

       a in A & a nin B & un(A,B,C) & C = {X / D}.

       un(A,B,C) & N + K > 5 & size(C,N) & B neq {}.

∎

As concerns constraint solving, the $\\{log\\}$ solver repeatedly applies
specialized rewriting procedures to its input formula $\Phi$ and returns
either $\mathit{false}$ or a formula in a simplified form which is guaranteed
to be satisfiable with respect to the intended interpretation. Each rewriting
procedure applies a few non-deterministic rewrite rules which reduce the
syntactic complexity of primitive constraints of one kind. At the core of
these procedures is set unification [DPR06]. The execution of the solver is
iterated until a fixpoint is reached, i.e., the formula is irreducible.

The disjunction of formulas returned by the solver represent all the concrete
(or ground) _solutions_ of the input formula. Any returned formula is divided
into two parts: the first part is a (possibly empty) list of equalities of the
form $X=t$, where $X$ is a variable occurring in the input formula and $t$ is
a term; and the second part is a (possibly empty) list of primitive
constraints.

##  3 Uses of $\\{log\\}$

In this section we show examples on how $\\{log\\}$ can be used as a
programming language (3.1) and as an automated theorem prover (3.2).

###  3.1 $\\{log\\}$ as a programming language

$\\{log\\}$ is primarily a programming language, at the intersection of
declarative programming, set programming [SDDS86] and constraint programming.
Specifically, $\\{log\\}$ is an instance of the general CLP scheme. As such,
$\\{log\\}$ programs are structured as a finite collection of _clauses_ ,
whose bodies can contain both atomic constraints and user-defined predicates.
The following examples show the _formula-program duality_ of $\\{log\\}$ code
along with the notion of clause.

######  Example 3.1.

If we want a program that updates function $F$ in $X$ with value $Y$ provided
$X$ belongs to the domain of $F$ and get an error otherwise, the $\\{log\\}$
code can be the following:

$\displaystyle\mathsf{update}(F,X,Y,F\leavevmode\vbox{\hrule
width=5.0pt},Error)\text{ :-}$ $\displaystyle\hskip
20.00003ptF=\\{[X,V]/F1\\}\And[X,V]\mathbin{\mathsf{nin}}F1\And
F\leavevmode\vbox{\hrule width=5.0pt}=\\{[X,Y]/F1\\}\And$ $\displaystyle\hskip
20.00003ptError=ok$ $\displaystyle\hskip 20.00003pt\mathbin{\mathsf{or}}$
$\displaystyle\hskip 20.00003pt\mathsf{dom}(F,D)\And
X\mathbin{\mathsf{nin}}D\And$ $\displaystyle\hskip 20.00003ptError=err.$

That is, $\mathsf{update}$ returns the modified $F$ in
$F\leavevmode\vbox{\hrule width=5.0pt}$ and the error code in $Error$—think of
$F\leavevmode\vbox{\hrule width=5.0pt}$ as the value of $F$ in the next state.
As $\And$ and $\mathbin{\mathsf{or}}$ are logical connectives and $=$ is
logical equality, the order of the ‘instructions’ is irrelevant w.r.t. the
functional result—although it can have an impact on the performance. Variable
$F1$ is an existentially quantified variable representing the ‘rest’ of $F$.
If the ordered pair $[X,V]$ does not belong to $F$ then the unification
between $F$ and $\\{[X,V]/F1\\}$ will fail thus making $\mathsf{update}$ to
execute the other branch.

Now we can call $\mathsf{update}$ by providing inputs and waiting for outputs:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{update}(\\{[setlog,5],[hello,earth],[tokeneer,model]\\},
hello,world,G,E). \crcr}$

returns:

$\displaystyle G=\\{[hello,world],[setlog,5],[tokeneer,model]\\},E=ok$ ∎

As a programming language, $\\{log\\}$ can be used to implement set-based
specifications (e.g., Z specifications). As a matter of fact, many of such
specifications can be easily translated into $\\{log\\}$ (see [CR21d]). This
means that $\\{log\\}$ can serve as a programming language in which a
_prototype_ of a set-based specification can be easily implemented. In a
sense, the $\\{log\\}$ implementation of a set-based specification can be seen
as an _executable specification_.

######  Remark 3.2.

A $\\{log\\}$ implementation of a set-based specification is easy to get but
usually it will not meet the typical performance requirements demanded by
users. Hence, we see a $\\{log\\}$ implementation of a set-based specification
more as a _prototype_ than as a final program. On the other hand, given the
similarities between a specification and the corresponding $\\{log\\}$
program, it’s reasonable to think that the prototype is a _correct_
implementation of the specification333In fact, the translation process can be
automated in many cases.. ∎

Then, we can use these prototypes to make an early validation of the
requirements. Validating user requirements by means of prototypes entails
executing the prototypes together with the users so they can agree or disagree
with the behavior of the prototypes. This early validation will detect many
errors, ambiguities and incompleteness present in the requirements and
possible misunderstandings or misinterpretations generated by the software
engineers. Without this validation many of these issues would be detected in
later stages of the project thus increasing the project costs. Think that if
one of these issues is detected once the product has been delivered it means
to correct the requirements document, the specification, the design, the
implementation, the user documentation, etc.

###  3.2 $\\{log\\}$ as an automated theorem prover

$\\{log\\}$ is also a _satisfiability solver_. This means that $\\{log\\}$ is
a program that can decide if formulas of some theory are _satisfiable_ or not.
In this case the theory is the theory of finite sets and binary relations,
combined with linear integer arithmetic.

Being a satisfiability solver, $\\{log\\}$ can be used as an automated theorem
prover. To prove that formula $\phi$ is a theorem, $\\{log\\}$ has to be
called to prove that $\neg\;\phi$ is unsatisfiable.

######  Example 3.3.

We can prove that set union is commutative by asking $\\{log\\}$ to prove the
following is unsatisfiable:

$\displaystyle\mathsf{un}(A,B,C)\And\mathsf{un}(B,A,D)\And
C\mathbin{\mathsf{neq}}D.$

As there are no sets satisfying this formula $\\{log\\}$ answers
$\mathsf{no}$. Note that the formula can also be written with the
$\mathsf{nun}$ constraint: $\mathsf{un}(A,B,C)\And\mathsf{nun}(B,A,C)$. ∎

Evaluating properties with $\\{log\\}$ helps to run correct simulations by
checking that the starting state is correctly defined. It also helps to _test_
whether or not certain properties are true of the specification or not.
However, by exploiting the ability to use $\\{log\\}$ as a theorem prover, we
can _prove_ that these properties are true of the specification.

For instance, since $\mathsf{update}$ in Example 3.1 is also a formula we can
_automatically_ prove properties true of it.

######  Example 3.4.

If $Error$ is equal to $err$ then $X$ does not belong to the domain of $F$. In
order to prove this property we need to call $\\{log\\}$ on its negation:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{update}(F,X,Y,F\leavevmode\kern
0.59998pt\vbox{\hrule width=5.0pt},err) \And\mathsf{dom}(F,D) \And X
\mathbin{\mathsf{in}}D. \crcr}$

Then, $\\{log\\}$ answers $\mathsf{no}$ because the formula is unsatisfiable.
Further, we can prove that $\mathsf{dom}(F,D)\And X\mathbin{\mathsf{nin}}D$ is
equivalent to $\mathsf{comp}(\\{[X,X]\\},F,\\{\\})$, which allows us to refine
$\mathsf{update}$ into a version not computing the domain of $F$. In fact,
$\mathsf{comp}(\\{[X,X]\\},F,\\{\\})$ is just a linear iteration over all the
elements of $F$. Then, we need to discharge the following proof obligation:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{dom}(F,D) \And X
\mathbin{\mathsf{nin}}D \Leftrightarrow\mathsf{comp}(\\{[X,X]\\},F,\\{\\})
\crcr}$

by proving that its negation is unsatisfiable:

$\displaystyle\mathsf{dom}(F,D)\And
X\mathbin{\mathsf{nin}}D\And\mathsf{ncomp}(\\{[X,X]\\},F,\\{\\})$
($\Rightarrow$)
$\displaystyle\mathsf{comp}(\\{[X,X]\\},F,\\{\\})\And\mathsf{dom}(F,D)\And
X\mathbin{\mathsf{in}}D$ ($\Leftarrow$)

Hence, now we can write $\mathsf{update}$ as follows:

$\displaystyle\mathsf{update}(F,X,Y,F\leavevmode\vbox{\hrule
width=5.0pt},Error)\text{ :-}$ $\displaystyle\hskip
20.00003ptF=\\{[X,V]/F1\\}\And[X,V]\mathbin{\mathsf{nin}}F1\And
F\leavevmode\vbox{\hrule width=5.0pt}=\\{[X,Y]/F1\\}\And$ $\displaystyle\hskip
20.00003ptError=ok$ $\displaystyle\hskip 20.00003pt\mathbin{\mathsf{or}}$
$\displaystyle\hskip 20.00003pt\mathsf{comp}(\\{[X,X]\\},F,\\{\\})\And$
$\displaystyle\hskip 20.00003ptError=err.$ ∎

Furthermore, $\\{log\\}$ can be used to automatically discharge verification
conditions in the form of invariants. Precisely, in order to prove that an
operation $T$ preserves the state invariant $I$ we have to discharge the
following proof obligation:

$I\mathrel{\wedge}T\Rightarrow I^{\prime}$ (1)

If we want to use $\\{log\\}$ to discharge (1) we have to ask $\\{log\\}$ to
check if the negation of (1) is _unsatisfiable_. In fact, we need to execute
the following $\\{log\\}$ _program_ :

$I\mathrel{\wedge}T\mathrel{\wedge}\neg\;I^{\prime}$ (2)

because $\neg\;(I\mathrel{\wedge}T\Rightarrow
I^{\prime})\equiv\neg\;(\neg\;(I\mathrel{\wedge}T)\mathrel{\vee}I^{\prime})\equiv
I\mathrel{\wedge}T\mathrel{\wedge}\neg\;I^{\prime}$.

######  Example 3.5.

An invariant property of $\mathsf{update}$ is that $F$ is a function.
Formally, we can prove the following:

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{pfun}(F)
\And\mathsf{update}(F,X,Y,F\leavevmode\kern 0.59998pt\vbox{\hrule
width=5.0pt},E) \Rightarrow\mathsf{pfun}(F\leavevmode\kern
0.59998pt\vbox{\hrule width=5.0pt}) \crcr}$

as always by proving that its negation is unsatisfiable:

$\mathsf{pfun}(F)\And\mathsf{update}(F,X,Y,F\leavevmode\vbox{\hrule
width=5.0pt},E)\And\mathsf{npfun}(F\leavevmode\vbox{\hrule width=5.0pt})$ ∎

As these examples show, $\\{log\\}$ is a programming and proof platform
exploiting the program-formula duality within the theory of finite sets and
binary relations.

In particular, many Z specifications can be easily translated into $\\{log\\}$
(see the on-line document [CR21d]). This means that $\\{log\\}$ can serve as a
_programming language_ in which _prototypes_ of those specifications can be
immediately implemented. Then, $\\{log\\}$ itself can be used to automatically
prove that the specifications preserve some state invariants.

##  4 Dealing with Binary Relations and Partial Functions

The relational fragment of $\\{log\\}$ is at least as expressive as the class
of full set relation algebras on finite sets [CR20b, CR18]. In spite of the
inherent undecidability of this class of relation algebras, $\\{log\\}$ is
able to automatically reason about practical problems expressed in relational
terms.

######  Example 4.1.

The overriding operator present in the Z formal notation is defined as
follows:

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr R \oplus S =
((\mathop{\mathrm{dom}}S) \mathbin{\hbox to0.0pt{\raise
0.21529pt\hbox{$-$}\hss}{\dres}}R) \cup S \crcr}$

where $R$ and $S$ are binary relations and $\mathbin{\hbox to0.0pt{\raise
0.21529pt\hbox{$-$}\hss}{\dres}}$ is domain anti-restriction. Given that the
operation that updates a table can be modeled as an overriding operation,
$\oplus$ is frequently used in Z specifications.

Overriding is available in $\\{log\\}$ in the form of the (derived) constraint
$\mathsf{oplus}$:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{oplus}(R,S,T) \Leftrightarrow T =
R \oplus S \crcr}$

Hence, we can specify in $\\{log\\}$ the $\mathsf{update}$ operation of
Example 3.1 as follows:

$\displaystyle\mathsf{updateOplus}(F,X,Y,F\leavevmode\vbox{\hrule
width=5.0pt},Error)\text{ :-}$ $\displaystyle\hskip
20.00003pt\mathsf{oplus}(F,\\{[X,Y]\\},F\leavevmode\vbox{\hrule
width=5.0pt})\And Error=ok$ $\displaystyle\hskip
20.00003pt\mathbin{\mathsf{or}}$ $\displaystyle\hskip
20.00003pt\mathsf{dom}(F,D)\And X\mathbin{\mathsf{nin}}D\And Error=err.$

Then we can use $\\{log\\}$ to prove that $\mathsf{update}$ refines
$\mathsf{updateOplus}$:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{update}(F,X,Y,G)
\Rightarrow\mathsf{updateOplus}(F,X,Y,G) \crcr}$

by proving the negation to be unsatisfiable. In this way we get a more
efficient code given that $\mathsf{oplus}$ is too powerful when one only wants
to update a single point in the relation. ∎

######  Remark 4.2.

Logical negation can be avoided in $\\{log\\}$ as long as we work with
primitive constraints, since for each of them $\\{log\\}$ implements also its
negation. On the other hand, if the formula to be negated is a compound
formula (i.e., a formula formed by conjunction and disjunction of atomic
predicates, such as, for instance, $\mathsf{updateOplus}$ in the above
example), then we must distribute “by hand” the negation all the way down to
the atoms at which point we use the negations of the primitive constraints.

Automating the generation of such kind of negated formulas is one of the
improvements that are planned as future work. ∎

The decidable fragment of the relational fragment of $\\{log\\}$ is still very
expressive. In fact, for a formula to be outside the decision procedure it
must contain an atom such as $\mathsf{comp}(R,S,\\{X/R\\})$ or
$\mathsf{comp}(S,R,\\{X/R\\})$ or a subformula that in some way hides such
atoms, i.e., it must contain a relational composition where one of the
operands shares a variable with the result of the composition.444The technical
details are more complex but this is the essence of the problem. For example,
if $\mathsf{dom}(\\{X/R\\},A)\And\mathsf{ran}(R,A)$ is present in the formula,
chances are that it will lay outside the decision procedure, since
$\mathsf{dom}$ and $\mathsf{ran}$ constraints are rewritten to formulas based
on $\mathsf{comp}$. When a formula lays outside the decision procedure
$\\{log\\}$ will enter an infinite loop. This means that $\\{log\\}$ gives
correct answers, but it might not give an answer.

The absence of $\mathsf{comp}$ constraints of the special form mentioned above
is only a sufficient condition for termination of $\\{log\\}$. In fact, not
all formulas containing such constraints go into an infinite loop. For
example, the formula
$\mathsf{comp}(\\{[X,Z]/R\\},\\{[Z,Y]/S\\},R)\mathrel{\wedge}\mathsf{id}(A,R)$,
where the first and the third operands share the same variable $R$, terminates
returning a finite number of solutions. Further investigation on the kind of
formulas that makes $\\{log\\}$ to enter an infinite loop is left for future
work. For now, we can observe that these patterns seldom occur in practice.
Indeed, an extensive empirical evaluation of a $\\{log\\}$ shows that the
solver is able to automatically prove hundreds of theorems of set theory and
relation algebra on finite sets, and to automatically find solutions to
systems of constraints of the same theories, as well [CR20b].

##  5 Dealing with Set Cardinalities

Some times it is necessary to reason about the size of data structures and not
only about their contents. For example, within the algebra of finite sets one
can partition a given set into two disjoint subsets: $C=A\cup
B\mathrel{\wedge}A\cap B=\emptyset$. But there is no way to state that $A$ and
$B$ must be of the same cardinality. In practice, these constraints might
appear, for instance, when part of a given data structure must be put into a
cache when its size reaches certain threshold. Specifically, cardinality
constraints appear in the verification of some distributed algorithms [BLL+19,
AGP17] and are at the base of the notions of integer interval, arrays and
lists.

$\\{log\\}$ implements a decision procedure for the algebra of finite sets
with cardinality [CR21c]. In this regard $\\{log\\}$ combines the rewrite
rules of the CLP(SET) scheme with a decision algorithm for formulas including
cardinality developed by C. Zarba [Zar02]. Zarba proves that a theory of
finite sets equipped with the classic set theoretic operators, including
cardinality, combined with linear integer constraints is decidable. The
$\\{log\\}$ decision procedure first uses all the power of $\\{log\\}$ to
produce a simplified, equivalent formula that can be passed to Zarba’s
algorithm which makes a final judgment about its satisfiability, in case it
contains cardinality constraints. At implementation level Zarba’s algorithm is
implemented by integrating the Prolog Boolean SAT solver developed by Howe and
King [HK12] with SWI-Prolog’s implementation of the CLP(Q) system [Hol95]. As
a result the implementation integrates three Prolog-based systems: Howe and
King’s SAT solver, CLP(Q) and $\\{log\\}$.

Hence, $\\{log\\}$ can be used to automatically prove verification conditions
based on the cardinality operator.

######  Example 5.1.

$\\{log\\}$ has been tested against +250 verification conditions arising
during the analysis of distributed algorithms [Pis20]. For instance, it can
automatically discharge the following proof obligation.

$\displaystyle\mathsf{size}(U,N)\And N>0\And N>3*T\And$
$\displaystyle\mathsf{subset}(F,U)\And\mathsf{size}(F,M)\And M\leq T\And$
$\displaystyle\mathsf{subset}(Cgs,U)\And\mathsf{size}(Cgs,K)\And 2*K\geq
N-T+1\And$ $\displaystyle\mathsf{subset}(Bgr,U)\And\mathsf{size}(Bgr,J)\And
2*J\geq N+3*T+1\And$
$\displaystyle\mathsf{inters}(Cgs,Bgr,L)\And\mathsf{size}(L,0)$ ∎

As a consequence of the fact that the new decision procedure is still based on
set unification, it can deal with set of sets nested at any level. For
example, the decision procedure is able to give all the possible solutions for
a goal such as $\mathsf{size}(\\{\\{X\\},\\{Y,Z\\}\\},N)$, where $X$, $Y$, $Z$
and $N$ are variables.

The formulas returned by $\\{log\\}$ represent all the concrete (or ground)
_solutions_ of the input formula. If these formulas do not contain any
$\mathsf{size}$ or integer constraints, then a concrete solution for such
formulas is obtained using the empty set for all set variables occurring in
them (with the exception of the variables $X$ in atoms of the form $X=t$).
Unfortunately, this is no longer true when considering also the
$\mathsf{size}$ and integer constraints. For example the answer to the
following formula:

$\displaystyle\mathsf{size}(A,M)\And 1\leq M\And M\leq
2\And\mathsf{size}(B,N)\And 5\leq N\And$
$\displaystyle\mathsf{subset}(C,B)\And\mathsf{size}(C,K)\And 7\leq K.$

is

$\displaystyle\mathsf{true}$
$\displaystyle\begin{split}\text{$\mathsf{Constraint:\,}$}&\mathsf{size}(A,M),M\geq
0,1\leq M,M\leq 2,\mathsf{size}(B,N),N\geq 0,\\\ &5\leq
N,\mathsf{subset}(C,B),\mathsf{size}(C,K),K\geq 0,7\leq K\end{split}$

That is, $\\{log\\}$ returns the formula itself. This means the formula is
satisfiable and that all the possible solutions can be obtained by fixing
values for the variables as long as all the constraints are met. However, this
answer does not point out an evident concrete solution for the formula.

For some applications such as model-based testing [CRF13] determining the
satisfiability of a formula is not enough. A more or less concrete solution is
needed. For this reason $\\{log\\}$ provides a way in which the solver returns
formulas for which is always easy to find a solution. We call such a solution
a _minimal solution_ because the cardinalities of all the set variables in
$\mathsf{size}$ constraints are the smallest as to satisfy the formula. When
$\\{log\\}$ is executed in the minimal solution mode, the answer to the above
goal is a more concrete solution:

$\displaystyle A=\\{\leavevmode\vbox{\hrule width=5.0pt}N8\\},$ $\displaystyle
M=1,$ $\displaystyle B=\\{\leavevmode\vbox{\hrule
width=5.0pt}N7,\leavevmode\vbox{\hrule width=5.0pt}N6,\leavevmode\vbox{\hrule
width=5.0pt}N5,\leavevmode\vbox{\hrule width=5.0pt}N4,\leavevmode\vbox{\hrule
width=5.0pt}N3,\leavevmode\vbox{\hrule width=5.0pt}N2,\leavevmode\vbox{\hrule
width=5.0pt}N1\\},$ $\displaystyle N=7,$ $\displaystyle
C=\\{\leavevmode\vbox{\hrule width=5.0pt}N7,\leavevmode\vbox{\hrule
width=5.0pt}N6,\leavevmode\vbox{\hrule width=5.0pt}N5,\leavevmode\vbox{\hrule
width=5.0pt}N4,\leavevmode\vbox{\hrule width=5.0pt}N3,\leavevmode\vbox{\hrule
width=5.0pt}N2,\leavevmode\vbox{\hrule width=5.0pt}N1\\},$ $\displaystyle K=7$
$\displaystyle\text{$\mathsf{Constraint:\,}$}\leavevmode\vbox{\hrule
width=5.0pt}N7\mathbin{\mathsf{neq}}\leavevmode\vbox{\hrule
width=5.0pt}N6,\leavevmode\vbox{\hrule
width=5.0pt}N7\mathbin{\mathsf{neq}}\leavevmode\vbox{\hrule
width=5.0pt}N5,...,\leavevmode\vbox{\hrule
width=5.0pt}N3\mathbin{\mathsf{neq}}\leavevmode\vbox{\hrule
width=5.0pt}N1,\leavevmode\vbox{\hrule
width=5.0pt}N2\mathbin{\mathsf{neq}}\leavevmode\vbox{\hrule width=5.0pt}N1$

This formula is a finite representation of a subset of the possible solutions
for the input formula from which it is trivial to get concrete solutions.

##  6 Restricted Intensional Sets

Intensional sets are widely recognized as a key feature to describe complex
problems, possibly leading to more readable and compact programs than those
based on conventional data abstractions. As a matter of fact, various
specification or modeling languages provide intensional sets as first-class
entities.

$\\{log\\}$ provides a narrower form of intensional sets, called Restricted
Intensional Sets (RIS), that are similar to the set comprehensions available
in the formal specification language Z. The basic form of a RIS term is:

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{ris}(X
\mathbin{\mathsf{in}}A, \phi, u) \crcr}$

where $D$ is a set, $\phi$ is a $\\{log\\}$ formula, and $u$ is a term
containing $X$. The intuitive semantics of this RIS is “the set of instances
of the term $u(X)$ such that $X$ belongs to $D$ and $\phi$ holds for $X$”,
i.e., $\\{y:\mathop{\mathstrut{\exists}}\nolimits x(x\in
A\mathrel{\wedge}\phi\mathrel{\wedge}y=u(x)\\}$.

RIS have the restriction that $D$ must be a _finite set_. This fact, along
with a few restrictions on variables occurring in $\phi$ and $u$, guarantees
that the RIS is a finite set, given that it is at most as large as $D$. It is
important to note that, although RIS are guaranteed to denote finite sets,
nonetheless, RIS may be not completely specified. In particular, as the domain
can be a variable or a partially specified set, RIS are finite but
_unbounded_.

$\\{log\\}$ formulas containing RIS remain decidable if the formulas inside
them are decidable555Among others, more technical, restrictions [CR17,
CR21b]..

The next example shows the classes of problems RIS are meant to solve.

######  Example 6.1.

First, we can use $\\{log\\}$ with RIS as a _programming language_. We can
think in a program outputting the even numbers ($E$) present in a set of
numbers ($S$) that is the input to the program:

$E=\mathsf{ris}(X\mathbin{\mathsf{in}}S,x\mathbin{\mathsf{mod}}2=0,X)$ (3)

The RIS term can be written more compactly as
$\mathsf{ris}(X\mathbin{\mathsf{in}}S,x\mathbin{\mathsf{mod}}2=0)$, since in
this case its third argument coincides with its control variable (i.e., the
first argument). Then if $S$ is bound to $[-2,2]$, $\\{log\\}$ will answer
$E=\\{-2,0,2\\}$.

Second, we can use $\\{log\\}$ with RIS as a _solver_ for set formulas. For
instance, we want $\\{log\\}$ to find the most general solution for the
following formula:

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{ris}(X
\mathbin{\mathsf{in}}A, 0 \>\mathsf{is}\> X \mathbin{\mathsf{mod}}2) =
\\{-2,0,2\\} \crcr}$

Note that, in a sense, we are asking $\\{log\\}$ to find the input values that
make program (3) to return a given output. In this case the answer will be:

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr S = \\{-2,0,2 /
N\\}, \mathsf{ris}(X \mathbin{\mathsf{in}}N, X \mathbin{\mathsf{mod}}2 = 0\\}
= \\{\\}\crcr}$

where $N$ is a new variable (implicitly existentially quantified).
Substituting $N$ by $\\{\\}$ yields a ground solution (i.e.,
$S=\\{-2,0,2\\}$).

Third, we can use $\\{log\\}$ with RIS to _prove_ properties of $\\{log\\}$
formulas. For instance, to prove that
$\mathsf{un}(\\{x:S|x<m\\},\\{x:S|x>m\\},B)\Rightarrow m\notin B$, we can
prove the following $\\{log\\}$ formula:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{un}(\mathsf{ris}(X
\mathbin{\mathsf{in}}S, X < M),\mathsf{ris}(X \mathbin{\mathsf{in}}S, X >
M),B) \mathrel{\wedge}M \mathbin{\mathsf{in}}B \crcr}$

which is found to be unsatisfiable. ∎

As LIA is decidable, RIS are a convenient mechanism to model and reason about
programs dealing with integers.

######  Example 6.2.

RIS can be used to get the subset of a set verifying some LIA formula, which
cannot be done rather efficiently in a pure algebraic fragment of set theory.

$\displaystyle\mathsf{ris}(X\mathbin{\mathsf{in}}S,\mathsf{integer}(X))$
[$S\cap{\bbold Z}$] $\displaystyle\mathsf{ris}(X\mathbin{\mathsf{in}}S,M\leq
X\And X\leq N)$ [$S\cap[M,N]$]
$\displaystyle\mathsf{ris}(X\mathbin{\mathsf{in}}S,0\leq X)$ [$S\cap{\bbold
N}$] $\displaystyle\mathsf{ris}(X\mathbin{\mathsf{in}}S,0\leq 3*X+2*Y)$ ∎

The same can be done with binary relations. As an example,
$\mathsf{ris}([X,Y]\mathbin{\mathsf{in}}R,X\leq Y)$ represents the binary
relation $R\cap(\leavevmode\vbox{\hrule
width=5.0pt}\leq\leavevmode\vbox{\hrule width=5.0pt})$.

######  Remark 6.3.

The language of RIS, called $\mathcal{L}_{\mathcal{RIS}}$, is parametric with
respect to any first-order theory $\mathcal{X}$ providing at least equality
and a decision procedure for $\mathcal{X}$-formulas. In practice, however,
many interesting theories are undecidable and only semi-decision procedures
exist for them. This is the case, for instance, for the theory RA of sets and
binary relations implemented by $\\{log\\}$. Hence, the condition on the
availability of a decision procedure for _all_ $\mathcal{X}$-formulas can be
often relaxed. Instead, the existence of some algorithm capable of deciding
the satisfiability of a significant fragment of $\mathcal{X}$-formulas can be
assumed. If such an algorithm exists and the user writes formulas inside the
corresponding fragment, all the theoretical results for RIS still apply. ∎

##  7 Universal Quantification in $\\{log\\}$

Formulas that $\\{log\\}$ can deal with are quantifier-free first-order
formulas over finite sets and integer linear arithmetic.

However, $\\{log\\}$ provides also some form of universal quantification by
means of RIS. In effect, the introduction of RIS in $\\{log\\}$ allows for the
definition of _restricted universal quantifiers_ (RUQ). In general, if $A$ is
a set, then a RUQ is a formula of the following form:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathop{\mathstrut{\forall}}\nolimits x
\in A: \phi\crcr}$

It is easy to prove the following:

$(\mathop{\mathstrut{\forall}}\nolimits x\in A:\phi)\Leftrightarrow
A\subseteq\\{x:x\in A\mathrel{\wedge}\phi\\}$ (4)

Given that $\\{x:x\in A\mathrel{\wedge}\phi\\}$ is the interpretation of
$\mathsf{ris}(X\mathbin{\mathsf{in}}A,\phi)$, the r.h.s. of (4) can be
expressed as the $\\{log\\}$ formula:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{subset}(A,\mathsf{ris}(X
\mathbin{\mathsf{in}}A,\phi)) \crcr}$

for which $\\{log\\}$ provides the derived constraint $\mathsf{foreach}$ thus
making RUQ easier to write:

$\mathsf{foreach}(X\mathbin{\mathsf{in}}A,\phi)\mathrel{\widehat{=}}\mathsf{subset}(A,\mathsf{ris}(X\mathbin{\mathsf{in}}A,\phi)).$
(5)

There is also a more powerful form of $\mathsf{foreach}$:

$\mathsf{foreach}(X\mathbin{\mathsf{in}}A,\mathsf{V},\phi,\psi)\mathrel{\widehat{=}}\mathsf{subset}(A,\mathsf{ris}(X\mathbin{\mathsf{in}}A,\mathsf{V},\phi,\psi)).$
(6)

where $\mathsf{V}$ is a vector of existentially quantified variables inside
the $\mathsf{foreach}$ and $\psi$ is a so-called _functional predicate_. A
predicate $\psi(x_{1},\dots,x_{n+1})$ is a functional predicate iff for any
given $x_{1},\dots,x_{n}$ there exists at most one $x_{n+1}$ making $\psi$
true. Functional predicates enjoy a nice property concerning their negation
[jar-ris], which considerably extends the class of decidable formulas
including $\mathsf{foreach}$ constraints.

######  Example 7.1.

We use $\mathsf{foreach}$ to encode and automatically reason about important
security properties [CR21a]. The Bell-LaPadula (BLP) security model proposes
two security properties for secure operating systems. The simplest is called
security condition of which we show a simplified version666Just look at the
complexity of the formula, not its interpretation in terms of computer
security.:

$\mathop{\mathstrut{\forall}}\nolimits(s,o,x)\in b:x=\mathsf{r}\Rightarrow
f_{2}(o)\leq f_{1}(s)\mathrel{\wedge}f_{4}(o)\subseteq f_{3}(s)$ (7)

where $b$ is a ternary relation and $f_{i}$ are functions. In $\\{log\\}$ we
can encode a ternary relation with a binary relation where the second
components are ordered pairs. Then $(s,o,x)\in b$ becomes
$[S,[O,X]]\mathbin{\mathsf{in}}B$. Therefore, (7) is encoded as follows:

$\displaystyle\mathsf{seccond}(F1,F2,F3,F4,B)\text{ :- }$ $\displaystyle\hskip
20.00003pt\mathsf{foreach}([S,[O,X]]\mathbin{\mathsf{in}}B,[No,Co,Ns,Cs],$
$\displaystyle\hskip 40.00006ptNo\leq Ns\And\mathsf{subset}(Co,Cs),$
$\displaystyle\hskip
40.00006pt\mathsf{apply}(F1,S,Ns)\And\mathsf{apply}(F2,O,No)\And$
$\displaystyle\hskip
40.00006pt\mathsf{apply}(F3,S,Cs)\And\mathsf{apply}(F4,O,Co))$

where $\mathsf{apply}$ is a derived constraint which is defined as
$\mathsf{apply}(F,X,Y)\mathrel{\widehat{=}}[X,Y]\mathbin{\mathsf{in}}F\And\mathsf{pfun}(F)$.
Note that all the $\mathsf{apply}$ constraints are placed in the last argument
given that they are functional predicates. ∎

######  Remark 7.2.

Example 7.1 brings in the point of when a binary relation can be _applied_ to
an element of its domain. Usually the condition for function application is,
precisely, for the binary relation to be a function. However, there is a
weaker condition in which the binary relation is _locally_ functional; that
is, the binary relation is a function in (at least) one point. Therefore, in
$\\{log\\}$ the user can work also with the following derived constraint:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{applyTo}(F,X,Y)
\mathrel{\widehat{=}}\crcr\hskip 20.00003ptF = \\{[X,Y] / G\\} \And[X,Y]
\mathbin{\mathsf{nin}}G \And\mathsf{comp}(\\{[X,X]\\},G,\\{\\}). \crcr}$

Using $\mathsf{apply}$ as in Example 7.1 implies that $\mathsf{seccond}$
checks that $F1$-$F4$ are functions every time it is called. In a real
implementation this is not the case because the fact that $F1$-$F4$ are
functions would be a pre-condition. Hence, a more realistic specification
would use $\mathsf{applyTo}$ instead of $\mathsf{apply}$. We can use
$\\{log\\}$ to automatically prove that if $F$ is a function then
$\mathsf{applyTo}$ refines $\mathsf{apply}$

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{pfun}(F)
\And\mathsf{applyTo}(F,X,Y) \Rightarrow\mathsf{apply}(F,X,Y) \crcr}$

This allows to formally replace $\mathsf{apply}$ by $\mathsf{applyTo}$ in
$\mathsf{seccond}$. Moreover, this results in a more efficient implementation
as $\mathsf{applyTo}$ is linear in the size of $F$ while $\mathsf{apply}$ is
quadratic. As a matter of fact, discharging all the verification conditions of
the BLP model using $\mathsf{applyTo}$ is almost 10 times faster than when
using $\mathsf{apply}$. ∎

The $\mathsf{foreach}$ constraint can be used to model and reason about order.
In fact if $F$ is a function with domain and range in ${\bbold Z}$, then we
can use $\\{log\\}$ to define a predicate stating whether or not $F$ is a
strictly increasing injective function ($\mathsf{siif}$).

######  Example 7.3.

The following formula captures the notion of strictly increasing function $F$:

$\displaystyle\mathop{\mathstrut{\forall}}\nolimits(a,c)\in
F,\mathop{\mathstrut{\forall}}\nolimits(x,y)\in F:a<x\Rightarrow c<y$

which is immediately rendered in $\\{log\\}$ by the following predicate:

$\displaystyle\mathsf{siif}(F)\text{ :- }$ $\displaystyle\hskip
20.00003pt\mathsf{pfun}(F)$ $\displaystyle\hskip
20.00003pt\mathrel{\wedge}\mathsf{foreach}([A,C]\mathbin{\mathsf{in}}F,$
$\displaystyle\hskip 20.00003pt\hskip
20.00003pt\mathsf{foreach}([X,Y]\mathbin{\mathsf{in}}F,A\geq
X\mathbin{\mathsf{or}}C<Y)))$ ∎

Although $\mathsf{foreach}$ can be defined as a derived constraint based on
the constraint $\mathsf{un}$, in $\\{log\\}$ we introduce a set of specialized
rewrite rules to process this specific kind of predicates more efficiently
[jar-ris]. As a matter of fact, the formula
$\mathsf{foreach}(x\in\\{t\mathbin{\scriptstyle\sqcup}A\\},\phi(x))$ can be
seen as an iterative program whose iteration variable is $x$, the range of
iteration is $\\{t\mathbin{\scriptstyle\sqcup}A\\}$, and the body is $\phi$.
In fact, the rewrite rule for this formula basically iterates over
$\\{t\mathbin{\scriptstyle\sqcup}A\\}$ and evaluates $\phi$ for each element
in that set. If one of these elements does not satisfy $\phi$ then the loop
terminates immediately, otherwise it continues until the empty set is found or
a variable is found.

##  8 Finite Integer Intervals

The theory INTERVAL (cf. Figures 1 and 2) deals with hereditarily finite
hybrid untyped extensional sets and integer intervals with cardinality. The
bounds of integer intervals can be either integer constants or variables
ranging over integer numbers, and as such they can be constrained through
integer linear arithmetic constraints.

$\\{log\\}$ provides a decision procedure of the theory INTERVAL. Integer
intervals in $\\{log\\}$ are represented by terms of the form
$\mathsf{int}(A,B)$, where $A$ and $B$ are integer constants or variables,
which is interpreted as the close interval $[A,B]$. Interval terms can be
manipulated as sets through set constraints (e.g.,
$\mathsf{int}(0,B)=\\{1,2/S\\}$ or
$\mathsf{inters}(\mathsf{int}(3,N),\mathsf{int}(10,20),A)\And
A\mathbin{\mathsf{neq}}\\{\\}$). Moreover, interval bounds can be manipulated
as integers through integer constraints (e.g., $A=\mathsf{int}(M,N)\And
N>=M+3$).

The decision procedure for the theory INTERVAL allows $\\{log\\}$ to be used
to program and automatically reason about problems such as the following.

######  Example 8.1.

Consider two workers who are assigned two disjoint sets of tasks from a set of
$N$ tasks. If $A$ and $B$ are the sets of tasks already performed by each
worker, then we can model the problem as follows.

$\displaystyle\mathsf{init}(A,B)\text{ :- }$ $\displaystyle\hskip
20.00003ptA=\\{\\}\And B=\\{\\}.$
$\displaystyle\mathsf{addToA}(N,A,B,J,A\leavevmode\vbox{\hrule
width=5.0pt},B)\text{ :- }$ $\displaystyle\hskip
20.00003pt(J\mathbin{\mathsf{nin}}\mathsf{int}(1,N)\mathbin{\mathsf{or}}J\mathbin{\mathsf{in}}A\mathbin{\mathsf{or}}J\mathbin{\mathsf{in}}B)\And
A\leavevmode\vbox{\hrule width=5.0pt}=A$ $\displaystyle\hskip
20.00003pt\mathbin{\mathsf{or}}$ $\displaystyle\hskip
20.00003ptJ\mathbin{\mathsf{in}}\mathsf{int}(1,N)\And
J\mathbin{\mathsf{nin}}A\And J\mathbin{\mathsf{nin}}B\And
A\leavevmode\vbox{\hrule width=5.0pt}=\\{J/A\\}.$
$\displaystyle\mathsf{finish}(N,A,B,\\{\\},\\{\\})\text{ :- }$
$\displaystyle\hskip
20.00003pt\mathsf{un}(A,B,\mathsf{int}(1,N))\And\mathsf{write(^{\prime}Jobdone^{\prime})}.$
$\displaystyle\mathsf{\%\
Invariant1:}\mathsf{un}(A,B,C)\And\mathsf{subset}(C,\mathsf{int}(1,N))$
$\displaystyle\mathsf{\%\ Invariant2:}\mathsf{disj}(A,B)$

For brevity we do not show $\mathsf{addToB}$ which would symmetric to
$\mathsf{addToA}$. Then, we can use $\\{log\\}$ to run some simulations:

$\displaystyle\mathsf{init}(A,B)\And\mathsf{addToA}(10,A,B,3,A1,B1)\And\mathsf{addToB}(10,A1,B1,7,A2,B2).$

Finally we can use $\\{log\\}$ to automatically prove the indicated
invariants.

If $A$ and $B$ must done $N/2$ tasks each, then we can add a
$\mathsf{size}$-based pre-condition to $\mathsf{addToA}$ and
$\mathsf{addToB}$, which would be still inside the decision procedures
implemented by $\\{log\\}$. ∎

######  Example 8.2.

Assume some objects are identified with numbers from 1 up. We want to write a
condition stating that a certain set of these objects, $A$, contains objects
with consecutive numbers. It can be written with an INTERVAL-based formula:

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr A =
\mathsf{int}(M,N) \And 1 \leq M \crcr}$

Moreover, if $A$ does not verify that condition we would like to compute the
missing objects from it:

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr A =
\mathsf{int}(M,N) \And 1 \leq M
\crcr\mathbin{\mathsf{or}}\crcr\mathsf{nint}(A) \And\mathsf{min}(A,M)
\And\mathsf{max}(A,N) \And\mathsf{un}(A,Miss,\mathsf{int}(M,N)) \crcr}$

where $\mathsf{nint}$ is a predicate stating that $A$ is not an integer
interval, and $\mathsf{min}$ and $\mathsf{max}$ compute the minimum and
maximum of $A$; all of which can be stated as INTERVAL formulas. ∎

The key idea for obtaining a decision procedure for the theory INTERVAL is
extending the set unification algorithm of CLP($\mathcal{SET}$) [DPPR00] with
the following identity:

$A=[m,n]\Leftrightarrow A\subseteq[m,n]\mathrel{\wedge}\lvert A\rvert=n-m+1$

In fact, it suffices to be able to deal with constraints of the form
$A\subseteq[m,n]$ in a decidable manner to have a decision procedure for
integer intervals.

Exploiting extended set unification with intervals $\\{log\\}$ allows, for
instance, to reconstruct integer intervals even out of underspecified sets:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{un}(\\{X,Y,Z\\},\\{1,4\\},\mathsf{int}(M,N))
\crcr}$

of which some solutions are:

$\offinterlineskip\halign to=433.62pt{\strut$\@zlign#$\hfil\cr X = 0, Y = 2, Z
= 3, M = 0, N = 4 \crcr X = 2, Y = 3, Z = 5, M = 1, N = 5 \crcr X = 2, Y = 3,
Z = 1, M = 1, N = 4 \crcr}$

######  Remark 8.3.

In some cases there are a few different ways of writing the same term or
formula. For instance, the RIS term
$\mathsf{ris}(X\mathbin{\mathsf{in}}S,M\leq X\And X\leq N)$ of Example 6.2 can
be written as the INTERVAL formula $\mathsf{inters}(S,\mathsf{int}(M,N),A)$,
in which case we have $A=\mathsf{ris}(X\mathbin{\mathsf{in}}S,M\leq X\And
X\leq N)$. Which is the best language construct to express programs and
properties depends on, some times, contradictory concepts such as efficiency
and readability. At least $\\{log\\}$ provides a way to go from one construct
to another. That is, if a user writes a formula containing the RIS in
question, (s)he can substitute the RIS by $A$ if
$\mathsf{inters}(S,\mathsf{int}(M,N),A)$ is conjoined to the formula, after
using $\\{log\\}$ to prove the substitution is correct. ∎

It is worth noting that a combination between the subset relation and integer
intervals is the key to encode forms of universal quantification in
$\\{log\\}$ by means of a quantifier-free formula, allowing us to preserve
decidability (and thus full automation in proofs). The following example
illustrates this idea.

######  Example 8.4.

If $X,Y\in D$, $Y$ is the successor of $X$ (in $D$) if the following holds:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\neg\;\mathop{\mathstrut{\exists}}\nolimits
Z \in D: X < Z \mathrel{\wedge}Z < Y \crcr}$

which is equivalent to:

$\mathop{\mathstrut{\forall}}\nolimits Z\in D:Z\leq X\mathrel{\vee}Y\leq Z$
(8)

In this case we need to quantify over integer numbers. A way to get rid of
this universal quantifier (hence, obtaining a quantifier-free $\\{log\\}$
formula) is to use a combination between the subset relation and integer
intervals as follows:

$\displaystyle\mathsf{succ}(D,X,Y)\text{ :-}$ $\displaystyle\hskip
20.00003ptD=\\{X,Y/E\\}\And\mathsf{un}(Inf,Sup,E)\And\mathsf{disj}(Inf,Sup)\And$
$\displaystyle\hskip
20.00003ptM\mathbin{\mathsf{is}}X-1\And\mathsf{subset}(Inf,\mathsf{int}(\leavevmode\vbox{\hrule
width=5.0pt},M))\And$ $\displaystyle\hskip
20.00003ptN\mathbin{\mathsf{is}}Y+1\And\mathsf{subset}(Sup,\mathsf{int}(N,\leavevmode\vbox{\hrule
width=5.0pt})).$

To confirm that $\mathsf{succ}$ is indeed an encoding of (8) we can execute
some tests:

$\displaystyle\mathsf{succ}(\\{4,7,1,8,-3\\},1,Y)\rightarrow Y=4$
$\displaystyle\mathsf{succ}(\\{4,7,1,8,-3\\},2,Y)\rightarrow\mathsf{no}$ [by
$2\notin D$]
$\displaystyle\mathsf{succ}(\\{4,7,1,8,-3\\},8,Y)\rightarrow\mathsf{no}$ [by
$max(D)=8$] $\displaystyle\mathsf{succ}(\\{4,7,1,8,-3\\},4,Y)\rightarrow Y=7$
$\displaystyle\mathsf{succ}(\\{4,7,1,8,-3\\},X,7)\rightarrow X=4$ ($\dagger$)
$\displaystyle\mathsf{succ}(\\{4,7,1,8,-3\\},X,Y)\rightarrow X=4,Y=7\mathchar
24635\relax\;X=7,Y=8\mathchar 24635\relax\;\dots$ ($\ddagger$)

Note that ($\dagger$ ‣ 8.4) shows that $\\{log\\}$ does not really distinguish
between inputs and outputs; and ($\ddagger$ ‣ 8.4) shows that $\\{log\\}$ is
able to return all solutions one after the other. Furthermore, to collect
stronger evidences that $\mathsf{succ}$ is correct we can use $\\{log\\}$ to
automatically prove some properties true of it:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{succ}(D,X,Y)
\Rightarrow(\mathop{\mathstrut{\forall}}\nolimits Z \in D: Z \leq X
\mathrel{\vee}Y \leq Z) \crcr}$

whose negation is:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{succ}(D,X,Y) \And Z
\mathbin{\mathsf{in}}D \And X < Z \And Z < Y \crcr}$

to which $\\{log\\}$ answers $\mathsf{no}$. And further we can prove:

$\offinterlineskip\halign
to=433.62pt{\strut$\@zlign#$\hfil\cr\mathsf{succ}(D,X,Y)
\And\mathsf{succ}(D,Y,Z) \Rightarrow X < Z \crcr}$

whose negation is:

$\mathsf{succ}(D,X,Y)\And\mathsf{succ}(D,Y,Z)\And Z\leq X$ ∎

Finally, integer intervals are a key component in the definition of arrays and
list as sets; hence, to implement the theories ARRAY and LIST in $\\{log\\}$
(cf. Figure 1). In particular, if $\mathsf{array}(A,n)$ is a predicate stating
that $A$ is an array of length $n$ whose components take values on some
universe $\mathsf{U}$, then it can be defined as follows:

$array(A,n)\Leftrightarrow A:[1,n]\rightarrow\mathsf{U}$

i.e., as a partial function between the integer interval $[1,n]$ and
$\mathsf{U}$. Since $\\{log\\}$ supports a broad class of set relation
algebras, including partial functions and the domain operator, then it would
be possible to use $\\{log\\}$ to automatically reason about broad classes of
programs with arrays. Lists could be introduced in a similar way.

However, supporting arrays and lists in $\\{log\\}$ is a line of future
research.

##  9 Concluding Remarks

The CLP language $\\{log\\}$ provides decision procedures for expressive
classes of extensional and intensional hereditarily finite hybrid sets,
including binary relations, integer intervals and Cartesian products, extended
with cardinality constraints and integer constraints for integer linear
arithmetic.

In this paper we have shown how $\\{log\\}$, with its decision procedures, can
be exploited: $(i)$ as a _programming language_ , in which a _prototype_ of a
set-based specification can be immediately implemented; $(ii$) as a
_satisfiability solver_ for formulas of the different theories, in particular
for formulas representing the implementation of a set-based specification for
which $\\{log\\}$ can be used to _prove_ that certain properties are true of
the specification. In this paper we have provided evidence for this claim by
showing a number of simple working examples written in $\\{log\\}$.

Besides the possible future work pointed out throughout the paper, we are
investigating the possibility to add interactive theorem proving capabilities
to $\\{log\\}$ [CKR] in order to make it capable of proving properties outside
of the implemented decision procedures.

## References

  * [AB99] Krzysztof R. Apt and Marc Bezem.  Formulas as Programs, pages 75–107.  Springer Berlin Heidelberg, Berlin, Heidelberg, 1999.
  * [AGP17] Francesco Alberti, Silvio Ghilardi, and Elena Pagani.  Cardinality constraints for arrays (decidability results and applications).  Formal Methods Syst. Des., 51(3):545–574, 2017.
  * [BC85] Joseph L. Bates and Robert L. Constable.  Proofs as programs.  ACM Trans. Program. Lang. Syst., 7(1):113–136, January 1985.
  * [BLL+19] Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, and Sharon Shoham.  Verification of threshold-based distributed algorithms by decomposition to decidable logics.  In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II, volume 11562 of Lecture Notes in Computer Science, pages 245–266. Springer, 2019.
  * [BRHR18] Michael J. Butler, Alexander Raschke, Thai Son Hoang, and Klaus Reichl, editors.  Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018, Proceedings, volume 10817 of Lecture Notes in Computer Science. Springer, 2018.
  * [CH88] Thierry Coquand and Gérard P. Huet.  The calculus of constructions.  Inf. Comput., 76(2/3):95–120, 1988.
  * [CKR] Maximiliano Cristiá, Ricardo Katz, and Gianfranco Rossi.  Proof automation in the theory of finite sets and finite set relation algebra.  Comput. J. accepted for publication March, 2nd, 2021. Preliminary version available here https://arxiv.org/pdf/2101.07700.
  * [CR16] Maximiliano Cristiá and Gianfranco Rossi.  A decision procedure for sets, binary relations and partial functions.  In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 179–198. Springer, 2016.
  * [CR17] Maximiliano Cristiá and Gianfranco Rossi.  A decision procedure for restricted intensional sets.  In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 185–201. Springer, 2017.
  * [CR18] Maximiliano Cristiá and Gianfranco Rossi.  A set solver for finite set relation algebra.  In Jules Desharnais, Walter Guttmann, and Stef Joosten, editors, Relational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29 - November 1, 2018, Proceedings, volume 11194 of Lecture Notes in Computer Science, pages 333–349. Springer, 2018.
  * [CR20a] Maximiliano Cristiá and Gianfranco Rossi.  An automatically verified prototype of the Tokeneer ID station specification.  CoRR, abs/2009.00999, 2020.
  * [CR20b] Maximiliano Cristiá and Gianfranco Rossi.  Solving quantifier-free first-order constraints over finite sets and binary relations.  J. Autom. Reasoning, 64(2):295–330, 2020.
  * [CR21a] Maximiliano Cristiá and Gianfranco Rossi.  Automated proof of Bell-LaPadula security properties.  J. Autom. Reason., 65(4):463–478, 2021.
  * [CR21b] Maximiliano Cristiá and Gianfranco Rossi.  Automated reasoning with restricted intensional sets.  Journal of Automated Reasoning, Apr 2021.
  * [CR21c] Maximiliano Cristiá and Gianfranco Rossi.  Integrating cardinality constraints into constraint logic programming with sets.  CoRR, abs/2102.05422, 2021.  Under consideration in Theory Pract. Log. Program.
  * [CR21d] Maximiliano Cristiá and Gianfranco Rossi.  $\\{log\\}$: Applications to software specification, prototyping and verification, 2021.
  * [CRF13] Maximiliano Cristiá, Gianfranco Rossi, and Claudia S. Frydman.  {log} as a test case generator for the Test Template Framework.  In Robert M. Hierons, Mercedes G. Merayo, and Mario Bravetti, editors, SEFM, volume 8137 of Lecture Notes in Computer Science, pages 229–243. Springer, 2013.
  * [DOPR96] Agostino Dovier, Eugenio G. Omodeo, Enrico Pontelli, and Gianfranco Rossi.  A language for programming in logic with finite sets.  J. Log. Program., 28(1):1–44, 1996.
  * [DPPR00] Agostino Dovier, Carla Piazza, Enrico Pontelli, and Gianfranco Rossi.  Sets and constraint logic programming.  ACM Trans. Program. Lang. Syst., 22(5):861–931, 2000.
  * [DPR06] Agostino Dovier, Enrico Pontelli, and Gianfranco Rossi.  Set unification.  Theory Pract. Log. Program., 6(6):645–701, 2006.
  * [HK12] Jacob M. Howe and Andy King.  A pearl on SAT and SMT solving in Prolog.  Theor. Comput. Sci., 435:43–55, 2012.
  * [HMB96] Christian Holzbaur, Francisco Menezes, and Pedro Barahona.  Defeasibility in CLP(Q) through generalized slack variables.  In Eugene C. Freuder, editor, CP, volume 1118 of Lecture Notes in Computer Science, pages 209–223. Springer, 1996.
  * [Hol95] Christian Holzbaur.  OFAI CLP(Q,R) manual.  Technical report, edition 1.3.3. Technical Report TR-95-09, Austrian Research Institute for Artificial Intelligence, 1995.
  * [Jon91] Clifford B. Jones.  Systematic software development using VDM (2. ed.).  Prentice Hall International Series in Computer Science. Prentice Hall, 1991.
  * [Pis20] Ruzica Piskac.  Efficient automated reasoning about sets and multisets with cardinality constraints.  In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, volume 12166 of Lecture Notes in Computer Science, pages 3–10. Springer, 2020.
  * [Ros21] Gianfranco Rossi.  $\\{log\\}$.  http://people.dmi.unipr.it/gianfranco.rossi/setlog.Home.html, 2021\.
  * [Sch01] S. Schneider.  The B-method: An Introduction.  Cornerstones of computing. Palgrave, 2001.
  * [SDDS86] Jacob T. Schwartz, Robert B. K. Dewar, Ed Dubinsky, and Edith Schonberg.  Programming with Sets - An Introduction to SETL.  Texts and Monographs in Computer Science. Springer, 1986.
  * [Spi92] J. M. Spivey.  The Z notation: a reference manual.  Prentice Hall International (UK) Ltd., Hertfordshire, UK, UK, 1992.
  * [Tho91] Simon Thompson.  Type theory and functional programming.  International computer science series. Addison-Wesley, 1991.
  * [Zar02] Calogero G. Zarba.  Combining sets with integers.  In Alessandro Armando, editor, Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002, Santa Margherita Ligure, Italy, April 8-10, 2002, Proceedings, volume 2309 of Lecture Notes in Computer Science, pages 103–116. Springer, 2002.


$\displaystyle=\binom{s_{3}+1}{1}\binom{s_{2}-1}{1}+\binom{s_{3}+2}{2}\cdot
2.$

######  Example 6.4.

For $n=4$, Corollary 6.2 yields

$\displaystyle(1+$ $\displaystyle s_{4})(1+s_{3}+s_{4})(1+s_{2}+s_{3}+s_{4})$
$\displaystyle=\hbox{$\binom{s_{4}+1}{1}\binom{s_{3}+1}{1}\binom{s_{2}+1}{1}+\binom{s_{4}+1}{1}\binom{s_{3}+1}{2}\cdot
2+\binom{s_{4}+1}{2}\binom{s_{2}+1}{1}\cdot
2+\binom{s_{4}+1}{2}\binom{s_{3}+1}{1}\cdot 4+\binom{s_{4}+1}{3}\cdot 6$}$
$\displaystyle=\hbox{$\binom{s_{4}+1}{1}\binom{s_{3}-1}{1}\binom{s_{2}-1}{1}+\binom{s_{4}+1}{1}\binom{s_{3}}{2}\cdot
2+\binom{s_{4}+2}{2}\binom{s_{2}-1}{1}\cdot
2+\binom{s_{4}+2}{2}\binom{s_{3}-1}{1}\cdot 4+\binom{s_{4}+3}{3}\cdot 6$}.$

######  Remark 6.5.

The weak compositions ${\bf j}=(j_{1},\ldots,j_{n})$ of $n-1$ that dominate
$(1,\ldots,1)$ is one family of objects enumerated by the Catalan numbers [40,
Problem 80]. There are $C_{n-1}:=\frac{1}{n}\binom{2n-2}{n-1}$ such
compositions, and thus that many terms in (6.1) and (6.2), respectively.

######  Remark 6.6.

When $\operatorname{s}$ is a composition, by Corollary 3.7, we have that the
RHS of (6.3) gives the volume of
$\mathcal{F}_{\operatorname{oru}(\operatorname{s})}$. Indeed in this case, by
Corollary 3.3 we have that

$\displaystyle\operatorname{vol}\mathcal{F}_{\operatorname{oru}(\operatorname{s})}(1,0,\ldots,0,-1)$
$\displaystyle=\\#\mathcal{F}_{\operatorname{oru}(\operatorname{s})}^{\mathbb{Z}}(0,s_{n},s_{n-1},\ldots,s_{2},-\sum_{i}s_{i})$
(6.8)
$\displaystyle=\\#\mathcal{F}_{\operatorname{oru}_{n}}^{\mathbb{Z}}(s_{n},s_{n-1},\ldots,s_{2},-\sum_{i}s_{i}),$

where the second equality follows since the netflow on the first vertex of
$\operatorname{oru}(\operatorname{s})$ is zero and so the edges of vertex
$v_{0}$ do not contribute. Thus, we can view (6.3) and (6.4) as decomposition
formulas for the volume. This is the approach used by
Kapoor–Mészáros–Setiabrata in [26] to prove Equation (6.2).

######  Remark 6.7.

Note that (6.3) and (6.4) hold when some $s_{i}$ are zero. Moreover, each term
of the RHS of the first formula (6.3) is nonnegative for $s_{i}\geq 0$,
however terms of the RHS of the second formula can be negative. See Examples
6.3 and 6.4 for $\operatorname{s}=(1,0,1)$ and $\operatorname{s}=(0,1,0,2)$,
respectively.

###  6.2. Towards a Lidskii-type decomposition of the
$\operatorname{s}$-permutahedron

In the previous section we used the Lidskii formulas to give an enumerative
decomposition for the number of $\operatorname{s}$-decreasing trees, which
index the vertices of the $\operatorname{s}$-permutahedron
$\text{Perm}_{\operatorname{s}}$. We note that the enumerative decomposition
(6.4) can be translated into a partition of the Hasse diagram of the
$\operatorname{s}$-weak order into intervals. For every $\bf j$ there are
$\prod_{i=1}^{n-1}(j_{1}+\dots+j_{i}-i+1)$ pieces that are products of the
Gale orders on
$\mathchoice{\left(\kern-4.79996pt{\binom{[s_{n}+1]}{j_{1}}}\kern-4.79996pt\right)}{\bigl{(}\kern-3.00003pt{\binom{[s_{n}+1]}{j_{1}}}\kern-3.00003pt\bigr{)}}{\bigl{(}\kern-3.00003pt{\binom{[s_{n}+1]}{j_{1}}}\kern-3.00003pt\bigr{)}}{\bigl{(}\kern-3.00003pt{\binom{[s_{n}+1]}{j_{1}}}\kern-3.00003pt\bigr{)}}$,
$\mathchoice{\left(\kern-4.79996pt{\binom{[s_{n-1}-1]}{j_{2}}}\kern-4.79996pt\right)}{\bigl{(}\kern-3.00003pt{\binom{[s_{n-1}-1]}{j_{2}}}\kern-3.00003pt\bigr{)}}{\bigl{(}\kern-3.00003pt{\binom{[s_{n-1}-1]}{j_{2}}}\kern-3.00003pt\bigr{)}}{\bigl{(}\kern-3.00003pt{\binom{[s_{n-1}-1]}{j_{2}}}\kern-3.00003pt\bigr{)}}$,
$\dots$,
$\mathchoice{\left(\kern-4.79996pt{\binom{[s_{2}-1]}{j_{n-1}}}\kern-4.79996pt\right)}{\bigl{(}\kern-3.00003pt{\binom{[s_{2}-1]}{j_{n-1}}}\kern-3.00003pt\bigr{)}}{\bigl{(}\kern-3.00003pt{\binom{[s_{2}-1]}{j_{n-1}}}\kern-3.00003pt\bigr{)}}{\bigl{(}\kern-3.00003pt{\binom{[s_{2}-1]}{j_{n-1}}}\kern-3.00003pt\bigr{)}}$,
where
$\mathchoice{\left(\kern-4.79996pt{\binom{[m]}{k}}\kern-4.79996pt\right)}{\bigl{(}\kern-3.00003pt{\binom{[m]}{k}}\kern-3.00003pt\bigr{)}}{\bigl{(}\kern-3.00003pt{\binom{[m]}{k}}\kern-3.00003pt\bigr{)}}{\bigl{(}\kern-3.00003pt{\binom{[m]}{k}}\kern-3.00003pt\bigr{)}}$
denotes the collection of multisets of $[m]$ of size $k$.

The _Gale order_ on
$\mathchoice{\left(\kern-4.79996pt{\binom{[m]}{k}}\kern-4.79996pt\right)}{\bigl{(}\kern-3.00003pt{\binom{[m]}{k}}\kern-3.00003pt\bigr{)}}{\bigl{(}\kern-3.00003pt{\binom{[m]}{k}}\kern-3.00003pt\bigr{)}}{\bigl{(}\kern-3.00003pt{\binom{[m]}{k}}\kern-3.00003pt\bigr{)}}$
is given by $A\leq B$ if $a_{i}\leq b_{i}$ for all $i\in[k]$, where
$a_{1},\dots,a_{k}$ (respectively $b_{1},\dots,b_{k}$) are the elements of $A$
(respectively $B$) ordered increasingly (see [16]). We denote this by
$\textit{Gale}(k,m)$.

See Figure 14 for the example of $s=(1,3,2)$. The central blue piece
corresponds to ${\bf j}=(1,1)$, which is the product of $\textit{Gale}(1,3)$
and $\textit{Gale}(1,2)$ where each is a chain of respective sizes $3$ and
$2$. The two side pieces each correspond to ${\bf j}=(2,0)$, and they are the
Hasse diagrams of $\textit{Gale}(2,3)$.

Figure 14. Subdivision of the complex of $\operatorname{s}$-trees for
$s=(1,3,2)$ that yields Equation (6.7).

##  7\. Further directions

#### Relation with the $\operatorname{s}$-associahedron

Ceballos and Pons also conjectured ([8, Conjecture 2]) that there exists a
geometric realization of the $\operatorname{s}$-permutahedron (when
$\operatorname{s}$ is a strict composition) such that the
$\operatorname{s}$-associahedron can be obtained from it by removing certain
facets. Our realizations seem very promising for providing a geometric
relation between $\operatorname{s}$-permutahedra and
$\operatorname{s}$-associahedra but this is still work in progress.

#### Other poset structures on $\operatorname{s}$-decreasing trees

In this article, we considered a specific triangulation of the flow polytope
$\mathcal{F}_{\operatorname{oru}(\operatorname{s})}$ induced by a fixed
framing of $\operatorname{oru}(\operatorname{s})$ described in Definition 3.4.
It would be interesting to study DKK triangulations of
$\mathcal{F}_{\operatorname{oru}(\operatorname{s})}$ arising from other
framings. For example, Bell et al. [3] showed that both the
$\operatorname{s}$-Tamari lattice and the principal order ideal $I(\nu)$ in
Young’s lattice, where $\nu_{i}=1+s_{n-i+1}+s_{n-i+2}+\cdots+s_{n}$, can be
realized as the graph dual to DKK triangulations of a flow polytope of the
$\nu$-caracol graph. Do other interesting posets on
$\operatorname{s}$-decreasing trees arise from other framed triangulations of
$\mathcal{F}_{\operatorname{oru}(\operatorname{s})}$?

#### The case where $\operatorname{s}$ is a weak composition

The $\operatorname{s}$-weak order of Ceballos and Pons is defined for weak
compositions but our realizations, which rely on a triangulation of the flow
polytope $\mathcal{F}_{\operatorname{oru}(\operatorname{s})}$ (see Sections
3.2, 4.2, and 5.2) hold only for strict compositions, since the graph
$\operatorname{oru}(\operatorname{s})$ is not defined for weak compositions.
Furthermore, although Corollary 3.7 does not hold for weak compositions,
Equation (6.5) does, so it would be interesting to extend our story to the
case of weak compositions.

##  8\. Acknowledgements

This work began under the collaborative project MATH-AMSUD with code
22-MATH-01 ALGonCOMB and we are very grateful for their support. We thank
Viviane Pons for helpful comments and suggestions and for proposing this
problem during the open problem session of the VIII Encuentro Colombiano de
Combinatoria ECCO 2022. We extend our gratitude to all of the organizers of
ECCO 2022. We also thank Cesar Ceballos, Balthazar Charles, Arnau Padrol,
Vincent Pilaud, Germain Poullot, Francisco Santos, Yannic Vargas, and the
combinatorics team of LIGM for helpful comments and proofreading of previous
versions of this manuscript. For this work we used the open-source software
Sage [13]. Rafael S. González D’León is very grateful for the summer research
stipend program of Loyola University Chicago since part of this work happened
under their support.

## References

  * [1] Welleda Baldoni and Michèle Vergne  “Kostant partitions functions and flow polytopes”  In _Transform. Groups_ 13.3-4 Springer, 2008, pp. 447–469
  * [2] Matthias Beck and Sinai Robins  “Computing the Continuous Discretely”, Undergraduate Texts in Mathematics  Springer, 2007
  * [3] Matias Bell, Rafael S. González D’León, Francisco A. Mayorga Cetina and Martha Yip  “A unifying framework for the $\nu$-Tamari lattice and principal order ideals in Young’s lattice”  In _Combinatorica_ , 2023  DOI: https://doi.org/10.1007/s00493-023-00022-x
  * [4] François Bergeron and Louis-François Préville-Ratelle  “Higher trivariate diagonal harmonics via generalized Tamari posets”  In _J. Comb._ 3.3, 2012, pp. 317–341  DOI: 10.4310/JOC.2012.v3.n3.a4
  * [5] Miklós Bóna  “Real zeros and normal distribution for statistics on Stirling permutations defined by Gessel and Stanley”  In _SIAM J. Discrete Math._ 23.1, 2008/09, pp. 401–406  DOI: 10.1137/070702254
  * [6] Cesar Ceballos and Rafael S. González D’León  “Signature Catalan combinatorics”  In _J. Comb._ 10.4, 2019, pp. 725–773  DOI: 10.4310/JOC.2019.v10.n4.a6
  * [7] Cesar Ceballos, Arnau Padrol and Camilo Sarmiento  “Geometry of $\nu$-Tamari lattices in types $A$ and $B$”  In _Trans. Amer. Math. Soc._ 371.4, 2019, pp. 2575–2622  DOI: 10.1090/tran/7405
  * [8] Cesar Ceballos and Viviane Pons  “The $s$-weak order and $s$-permutahedra”  In _Sém. Lothar. Combin._ 82B, 2020, pp. Art. 76, 12
  * [9] Cesar Ceballos and Viviane Pons  “The $s$-weak order and $s$-permutahedra I: combinatorics and lattice structure”  In _arXiv preprint arXiv:2212.11556_ , 2022  DOI: 10.48550/arXiv.2212.11556
  * [10] Sylvie Corteel, Jang Soo Kim and Karola Mészáros  “Flow polytopes with Catalan volumes”  In _Comptes Rendus Mathematique_ 355.3 Elsevier, 2017, pp. 248–259
  * [11] Vladimir I. Danilov, Alexander V. Karzanov and Gleb A. Koshevoy  “Coherent fans in the space of flows in framed graphs”  In _24th International Conference on Formal Power Series and Algebraic Combinatorics (FPSAC 2012)_ , Discrete Math. Theor. Comput. Sci. Proc., 2012, pp. 481–490
  * [12] Mike Develin and Bernd Sturmfels  “Tropical convexity”  In _Documenta Mathematica_ 9, 2004, pp. 1–27
  * [13] The Developers  “Sage Mathematics Software” http://www.sagemath.org, 2022
  * [14] Eugène Ehrhart  “Sur les polyèdres rationnels homothétiques à n dimensions”  In _C. R. Acad. Sci. Paris_ 254, 1962, pp. 616–618
  * [15] Alex Fink and Felipe Rincón  “Stiefel tropical linear spaces”  In _Journal of Combinatorial Theory, Series A_ 135 Elsevier, 2015, pp. 291–331
  * [16] David Gale  “Optimal assignments in an ordered set: An application of matroid theory”  In _J. Combinatorial Theory_ 4, 1968, pp. 176–180
  * [17] Giorgio Gallo and Claudio Sodini  “Extreme points and adjacency relationship in the flow polytope”  In _Calcolo_ 15.3, 1978, pp. 277–288  DOI: 10.1007/BF02575918
  * [18] Ira Gessel and Richard P. Stanley  “Stirling polynomials”  In _J. Combinatorial Theory Ser. A_ 24.1, 1978, pp. 24–33
  * [19] Ira M Gessel  “A note on Stirling permutations”  In _arXiv preprint arXiv:2005.04133_ , 2020
  * [20] Ronald L. Graham, Donald E. Knuth and Oren Patashnik  “Concrete mathematics” A foundation for computer science  Addison-Wesley Publishing Company, Reading, MA, 1994, pp. xiv+657
  * [21] Birkett Huber, Jörg Rambau and Francisco. Santos  “The Cayley Trick, lifting subdivisions and the Bohne-Dress theorem on zonotopal tilings”  In _J. Eur. Math. Soc._ 2, 2000, pp. 179–198  DOI: 10.1007/s100970050003
  * [22] Jihyeug Jang and Jang Soo Kim  “Volumes of flow polytopes related to caracol graphs”  In _arXiv preprint arXiv:1911.10703_ , 2019
  * [23] Svante Janson, Markus Kuba and Alois Panholzer  “Generalized Stirling permutations, families of increasing trees and urn models”  In _J. Combin. Theory Ser. A_ 118.1, 2011, pp. 94–114  DOI: 10.1016/j.jcta.2009.11.006
  * [24] Michael Joswig  “Essentials of tropical combinatorics”  American Mathematical Society, 2021
  * [25] Michael Joswig  “The Cayley trick for tropical hypersurfaces with a view toward Ricardian economics”  In _Homological and Computational Methods in Commutative Algebra: Dedicated to Winfried Bruns on the Occasion of his 70th Birthday_ Springer, 2017, pp. 107–128
  * [26] Kabir Kapoor, Karola Mészáros and Linus Setiabrata  “Counting integer points of flow polytopes”  In _Discrete Comput. Geom._ 66.2, 2021, pp. 723–736  DOI: 10.1007/s00454-021-00289-1
  * [27] Markus Kuba and Alois Panholzer  “Analysis of statistics for generalized Stirling permutations”  In _Combin. Probab. Comput._ 20.6, 2011, pp. 875–910  DOI: 10.1017/S0963548311000381
  * [28] Karola Mészáros and Alejandro H. Morales  “Flow polytopes of signed graphs and the Kostant partition function”  In _Int. Math. Res. Not. IMRN_ , 2015, pp. 830–871  DOI: 10.1093/imrn/rnt212
  * [29] Karola Mészáros and Alejandro H. Morales  “Volumes and Ehrhart polynomials of flow polytopes”  In _Math. Z._ 293.3-4, 2019, pp. 1369–1401  DOI: 10.1007/s00209-019-02283-z
  * [30] Karola Mészáros, Alejandro H. Morales and Jessica Striker  “On flow polytopes, order polytopes, and certain faces of the alternating sign matrix polytope”  In _Discrete Comput. Geom._ 62.1, 2019, pp. 128–163  DOI: 10.1007/s00454-019-00073-2
  * [31] Alejandro H. Morales and William Shi  “Refinements and symmetries of the Morris identity for volumes of flow polytopes”  In _C. R. Math. Acad. Sci. Paris_ 359, 2021, pp. 823–851  DOI: 10.5802/crmath.218
  * [32] SeungKyung Park  “Inverse descents of $r$-multipermutations”  In _Discrete Math._ 132.1-3, 1994, pp. 215–229  DOI: 10.1016/0012-365X(94)90239-9
  * [33] SeungKyung Park  “$P$-partitions and $q$-Stirling numbers”  In _J. Combin. Theory Ser. A_ 68.1, 1994, pp. 33–52  DOI: 10.1016/0097-3165(94)90090-6
  * [34] SeungKyung Park  “The $r$-multipermutations”  In _J. Combin. Theory Ser. A_ 67.1, 1994, pp. 44–71  DOI: 10.1016/0097-3165(94)90003-5
  * [35] Alexander Postnikov  In _personal communication_ , 2010;2014
  * [36] Louis-François Préville-Ratelle and Xavier Viennot  “The enumeration of generalized Tamari intervals”  In _Trans. Amer. Math. Soc._ 369.7, 2017, pp. 5219–5239  DOI: 10.1090/tran/7004
  * [37] Francisco Santos  “The Cayley trick and triangulations of products of simplices”  In _Integer points in polyhedra—geometry, number theory, algebra, optimization_ 374, Contemp. Math.  Amer. Math. Soc., Providence, RI, 2005, pp. 151–177  DOI: 10.1090/conm/374/06904
  * [38] Carla D. Savage and Mirkó Visontai  “The $\mathbf{s}$-Eulerian polynomials have only real roots”  In _Trans. Amer. Math. Soc._ 367.2, 2015, pp. 1441–1466  DOI: 10.1090/S0002-9947-2014-06256-9
  * [39] Richard P. Stanley  “Acyclic flow polytopes and Kostant’s partition function”  In _Conference transparencies_ , 2000  URL: http://math.mit.edu/~rstan/trans.html
  * [40] Richard P. Stanley  “Catalan numbers”  Cambridge University Press, New York, 2015, pp. viii+215  DOI: 10.1017/CBO9781139871495
  * [41] Richard P. Stanley  “Decompositions of rational convex polytopes”  In _Ann. Discrete Math_ 6.6, 1980, pp. 333–342
  * [42] Richard P. Stanley  “Enumerative combinatorics. Volume 1” 49, Cambridge Studies in Advanced Mathematics  Cambridge: Cambridge University Press, 2012, pp. xiv+626
  * [43] Bernd Sturmfels  “On the Newton polytope of the resultant”  In _J. Algebraic Combin._ 3.2, 1994, pp. 207–236  DOI: 10.1023/A:1022497624378
  * [44] Dov Tamari  “The algebra of bracketings and their enumeration”  In _Nieuw Arch. Wisk. (3)_ 10, 1962, pp. 131–146