Try with: Web Interface Java Webstart

We outline some of the Princess functionality and use cases:

- Presburger Arithmetic, Quantifier Elimination
- Uninterpreted Predicates
- Craig Interpolation
- Uninterpreted functions and triggers

To illustrate what can be expressed using Presburger arithmetic, we first look at a very simple puzzle (found here):

"My grandson is about as many days as my son is weeks, and my grandson is as many months as I am in years. My grandson, my son and I together are 140 years. Can you tell me my age in years?"

Solving this puzzle boils down to finding the (integer) solutions of a system of linear equations, which is a problem that can be written in Presburger arithmetic. We can first check the existence of solutions:\exists int grandson_years, son_years, my_years,To feed this problem into Princess, we need to wrap the statement

grandson_months, son_weeks, grandson_days; (

grandson_days = grandson_months * 4 * 7 &

grandson_months = grandson_years * 12 &

son_weeks = son_years * 12 * 4 &

grandson_days = son_weeks &

grandson_months = my_years &

grandson_years + son_years + my_years = 140

)

```
\problem{
... }
```

around the formula. The Princess prover can then simply be
web-started
and be run on the formula, which results in something like this. Princess confirms that the
system of equations is solvable:No countermodel exists, formula is validOf course, we would also like to know the answer to the puzzle! To determine and output the age of the storyteller, we need to remove the quantifier for the variable

`my_years`

and declare it as an
implicitly existentially quantified constant instead:\existentialConstants {Now, Princess will also provide us a solution for

int my_years;

}

\problem {

\exists int grandson_years, son_years,

grandson_months, son_weeks, grandson_days; (

grandson_days = grandson_months * 4 * 7 &

grandson_months = grandson_years * 12 &

son_weeks = son_years * 12 * 4 &

grandson_days = son_weeks &

grandson_months = my_years &

grandson_years + son_years + my_years = 140

)

}

`my_years`

,
namely
84.
This
solution
is
given
as
a
conjunction
of
equations
over
the
existential
constants
(in
our
example,
there
is
only
a
single
constant
`my_years`

):

Formula is valid, satisfying assignment for the existential constants is:

my_years = 84

We might want to know whether 84 is the only solution of the puzzle,
or whether the storyteller could be younger or older than this. The
first way to achieve that is to add the option `+mostGeneralConstraint`

to the "Options" text field in the bottom of the Princess window. This
option makes Princess search for all
solutions of the formula, instead of stopping after she has found the
first one. This is realised by means of quantifier elimination.
For our example, the output will be the following:

```
```

Formula is valid, resulting most-general constraint:This means that 84 is the only solution to the puzzle.

my_years = 84

Concrete witness:

my_years = 84

Note: The option `+mostGeneralConstraint`

should be used with
care if also uninterpreted predicates are involved, as described below,
because it can easily lead to non-termination.

A second way to search for further solutions (which sometimes can be
more efficient) is to simply add a disequation or inequality like ```
my_years
<
84
```

to the
problem:

\existentialConstants {

int my_years;

}

\problem {

\exists int grandson_years, son_years,

grandson_months, son_weeks, grandson_days; (

grandson_days = grandson_months * 4 * 7 &

grandson_months = grandson_years * 12 &

son_weeks = son_years * 12 * 4 &

grandson_days = son_weeks &

grandson_months = my_years &

grandson_years + son_years + my_years = 140

)

&

my_years < 84

}

This time, Princess tells us that it was not able to solve the
problem (do not forget to remove the option `+mostGeneralConstraint`

again):

Formula is invalid, found a countermodel:Because Princess actually is complete for problems in Presburger arithmetic, she is able to tell us that no solution exists.

true

Princess can also handle problems containing uninterpreted predicates,
which makes the accepted language strictly more expressive than
Presburger arithmetic (in fact, too powerful to allow complete calculi;
intuitively, Princess can prove only those valid formulae for which no
induction is needed). As a simple example, we could introduce a binary
predicate `divides`

(which is not part of Presburger
arithmetic) and add axioms that describe the concept of divisibility:

\predicates {Run on this example, Princess will again tell us that it has found a proof of validity:

divides(int, int);

}

\problem {

//

// Axioms

//

\forall int x; divides(x, x)

-> \forall int x, y; (divides(x, y) -> divides(x, y+x) & divides(x, y-x))

->

//

// Problem to be proven

//

divides(7, 49)

}

Formula is valid, resulting constraint:

true

By adding existential constants, we can use Princess for factorising
numbers or for computing common divisors of two numbers (not that this
would be particularly efficient, however):

\existentialConstants {The result is something like:

int A, B;

}

\predicates {

divides(int, int);

}

\problem {

\forall int x; divides(x, x)

-> \forall int x, y; (divides(x, y) -> divides(x, y+x) & divides(x, y-x))

->

divides(A, 51) & A < 51 & A > 1 &

divides(B, 42) & divides(B, 49) & B > 1

}

Formula is valid, resulting constraint:

B = 7 & A = 17

Concrete witness:

B = 7 & A = 17

Somewhat more intricate, we can also express that we are interested
only in greatest common
divisors of two numbers:

divides(A, 42) & divides(A, 49) &Interestingly, this property is not provable with the given axioms for the predicate

\forall int x; (divides(x, 42) & divides(x, 49) & x > 1 -> x <= A)

`divides`

. This is because the two axioms
only tell for which arguments `divides`

holds, but not for
which arguments it does not
hold. Consequently, Princess is able to derive that 7 is a common
divisor of 42 and 49, but not that no larger number is a common divisor
as well.Note: Princess will not
terminate when run on the example and has to be stopped manually.

We need to add a third axiom stating that 0 is the only element of
the
interval `(-x, x)`

that is divided by `x`

:

\existentialConstants {Now, Princess is able to derive a solution:

int A;

}

\predicates {

divides(int, int);

}

\problem {

\forall int x; divides(x, x)

-> \forall int x, y; (divides(x, y) -> divides(x, y+x) & divides(x, y-x))

-> \forall int x, y; (divides(x, y) & y < x & y > -x -> y = 0)

->

divides(A, 42) & divides(A, 49) &

\forall int x; (divides(x, 42) & divides(x, 49) & x > 1 -> x <= A)

}

Formula is valid, resulting constraint:

A = 7

Concrete witness:

A = 7

Besides reasoning about the validity/satisfiability of problems, Princess is also able to extract Craig Interpolants from valid formulae. This functionality is described in the following documents: paper 1 (JAR), paper 2 (VMCAI). Interpolants summarise the information flow that takes place when proving the validity of a formula, and are useful for a variety of applications related to program verification, for instance approximative image computation and the construction/refinement of abstractions.

In order to compute interpolants, a formula first has to be
partitioned into a number of disjuncts. The individual parts are marked
and labelled using the keyword `\part`

; the labels can then
be used to
formulate a sequence of interpolation problems with the help of the
keyword `\interpolant`

.
For instance, in the following problem two disjuncts `left`

and `right`

have been marked, and we request the
computation of an interpolant for the implication ```
left ->
right
```

:

\functions {The output of Princess for this problem is something like:

int c, d;

}

\problem {

\part[left] (c > d & d > 0)

->

\part[right] c > 0

}

\interpolant {left; right}

Constructing countermodel ...The interpolant

Found proof (size 4), simplifying (4), interpolating ...

No countermodel exists, formula is valid

Interpolants:

c >= 2

`c >= 2`

has the property that ```
left
->
c
>=
2
```

and `c >= 2 -> right`

, and is a formula
over the common vocabulary of `left`

and `right`

;
the interpolant can thus be seen as an intermediate formula between `left`

and `right`

.
It is possible to have more than two `\part`

s in a
problem,
and to use multiple `\interpolant`

statements.
Consider the following program with variables ranging over unbounded
integers:

if (a == 2*x && a >= 0) { // point (1)In order to verify the assertion, the program is translated into a formula in Presburger arithmetic. Note that

b = a / 2; // point (2)

c = 3*b + 1; // point (3)

assert (c > a);

}

```
b
= a / 2
```

is converted into a
conjunction of two inequalities; also, we introduce labels for each
statement in the program:
\functions {In each

int x, a, b, c;

}

\problem {

\part[cond] (a = 2*x & a >= 0) &

\part[stmt1] (2*b <= a & 2*b >= a - 1) &

\part[stmt2] c = 3*b + 1

->

\part[assert] c > a

}

\interpolant {cond; stmt1, stmt2, assert}

\interpolant {cond, stmt1; stmt2, assert}

\interpolant {cond, stmt1, stmt2; assert}

`\interpolant`

clause, the labels left of the
semicolon specify the left partition, the labels right of the semicolon
the right partition. Given this input, Princess now computes three
interpolants, for the
three different partitionings that were specified:
Constructing countermodel ...

Found proof (size 8), simplifying (8), interpolating ...

No countermodel exists, formula is valid

Interpolants:

a >= 3 | (a >= 0 & \exists int v0; 2 * v0 = a)

3 * b >= a

c - a >= 1

The three interpolants represent invariants that hold true at different points of the original program: the first interpolants holds immediately after the if-condition (at point (1)), the second interpolants holds at point (2) after the first assignment, and the third interpolant at point (3) in front of the assertion.

- The input problem is transformed to disjunctive normalform; in
the example, something like
`!cond | !stmt1 | !stmt2 | assert`

. - It is checked that all the \part annotations are in front of
top-level disjuncts. If they are not, e.g., you end up with a disjunct
`(\part[X] foo) & (\part[Y] bar)`

, an error message will be raised. - The
`\part`

annotations are stripped away, and it is checked/proven whether the resulting formula/disjunction is valid or invalid. - If it was possible to prove that the input
formula is valid, the stated interpolation
problems are considered, each of which specifies a partitioning of
the disjuncts that were determined in step 1. I.e. for a clause
`\interpolant {A1, ..., An; B1, ..., Bm}`

, and assuming that`A1, ..., An, B1, ..., Bm`

are the disjuncts in step 1, a formula I is computed that satisfies the implication`!A1 & ... & !An -> I`

and`!A1 & ... & !Bm -> !I`

.`I`

is computed in such a way that it only contains symbols (constants, functions, predicates) that are common to the left partition`A1, ..., An`

and the right partition`B1, ..., Bm`

.

Because all the interpolants are generated from the same proof
(extracted in step 3), it is also guaranteed that the interpolants
satisfy the "chaining property," in case the input problem and```
\interpolant
```

clauses specify a chain. That means, if we have an
interpolation problem of the form

\problem {then the generated interpolants

\part[p1] f1

&

\part[p2] f2

&

// ...

&

\part[pn] fn

->

false

}

\interpolant { p1; p2, ..., p(n-1), pn }

\interpolant { p1, p2; ..., p(n-1), pn }

// ...

\interpolant { p1, p2, ..., p(n-1); pn }

`I1, I2, ..., I(n-1)`

satisfy the implications
`f1 -> I1`

`f2 & I1 -> I2`

`f3 & I2 -> I3`

`...`

`f(n-1) & I(n-2) -> I(n-1)`

`fn & I(n-1) -> false`

.

In addition to uninterpreted predicates, it is also possible to use uninterpreted functions for formulating problems in Princess. The Princess method to handle functions is described in an LPAR paper. To illustrate the use of functions, we consider another riddle (taken from this page):

Here's a variation on a famous puzzle
by Lewis Carroll, who wrote Alice's Adventures in Wonderland.

"A group of 100 soldiers suffered the following injuries in a battle: 70 soldiers lost an eye, 75 lost an ear, 85 lost a leg, and 80 lost an arm. What is the minimum number of soldiers who must have lost all 4?"

"A group of 100 soldiers suffered the following injuries in a battle: 70 soldiers lost an eye, 75 lost an ear, 85 lost a leg, and 80 lost an arm. What is the minimum number of soldiers who must have lost all 4?"

This puzzle could be formalised in the Princess syntax by declaring 16 constant symbols:

- A constant
`n0000`

representing the number of soldiers who kept eyes, ears, legs, and arms - A constant
`n1000`

, the number of soldiers who lost an eye, but kept everything else - A constant
`n0100`

, the number of soldiers who lost an ear, but kept everything else - and so on.

Since the declaration of so many constants is a bit cumbersome, instead we can use an uninterpreted function with four integer arguments:

\functions {Instead of a constant

int inj(int, // lost an eye?

int, // lost an ear?

int, // lost a leg?

int // lost an arm?

);

}

`n0000`

, we can now simply write `inj(0,0,0,0)`

,
etc.
The riddle can then be translated to a conjunction of equations,
together with a universally quantified formula that ensures that
the function `inj`

represents non-negative values. Since we
are interested in a lower bound of the value `inj(1,1,1,1)`

(the number of soldiers who lost all four),
we
additionally introduce an existential constant `MinNum`

and add the inequality `inj(1,1,1,1) >= MinNum`

as a
conclusion supposed to follow from the conditions of the riddle:

\existentialConstants {When running Princess on this input, she will check whether any value

int MinNum;

}

\functions {

int inj(int, int, int, int);

}

\problem {

// 100 soldiers altogether

inj(0,0,0,0) + inj(0,0,0,1) + inj(0,0,1,0) + inj(0,0,1,1) +

inj(0,1,0,0) + inj(0,1,0,1) + inj(0,1,1,0) + inj(0,1,1,1) +

inj(1,0,0,0) + inj(1,0,0,1) + inj(1,0,1,0) + inj(1,0,1,1) +

inj(1,1,0,0) + inj(1,1,0,1) + inj(1,1,1,0) + inj(1,1,1,1) = 100

&

// 70 soldiers lost an eye

inj(1,0,0,0) + inj(1,0,0,1) + inj(1,0,1,0) + inj(1,0,1,1) +

inj(1,1,0,0) + inj(1,1,0,1) + inj(1,1,1,0) + inj(1,1,1,1) = 70

&

// 75 soldiers lost an ear

inj(0,1,0,0) + inj(0,1,0,1) + inj(0,1,1,0) + inj(0,1,1,1) +

inj(1,1,0,0) + inj(1,1,0,1) + inj(1,1,1,0) + inj(1,1,1,1) = 75

&

// 85 soldiers lost a leg

inj(0,0,1,0) + inj(0,0,1,1) + inj(0,1,1,0) + inj(0,1,1,1) +

inj(1,0,1,0) + inj(1,0,1,1) + inj(1,1,1,0) + inj(1,1,1,1) = 85

&

// 80 soldiers lost an arm

inj(0,0,0,1) + inj(0,0,1,1) + inj(0,1,0,1) + inj(0,1,1,1) +

inj(1,0,0,1) + inj(1,0,1,1) + inj(1,1,0,1) + inj(1,1,1,1) = 80

&

// inj is non-negative

\forall int x1, x2, x3, x4; inj(x1, x2, x3, x4) >= 0

->

// MinNum is supposed to be a lower bound of the number of soldiers who must have lost all 4

inj(1, 1, 1, 1) >= MinNum

}

`MinNum`

exists such that the stated implication holds, for any valuation of the
function `inj`

that satisfies the given conditions. Indeed,
such values can be found:
Proving ...This means that any

Formula is valid, resulting constraint:

10 >= MinNum

Concrete witness:

MinNum = 10

`MinNum <= 10`

(and in particular
10) is a lower bound of `inj(1,1,1,1)`

; at least 10
soldiers must have lost all four.
Though we now know that 10 is a lower bound, we don't know yet whether
10 is the greatest lower
bound (that was asked for in the puzzle). There are different ways to
check whether the bound 10 is tight; most simply, we can add an
additional inequality to the Princess input, forcing the prover to
search for values `MinNum > 10`

:

[...]Princess won't be able to find any such values, indicating that 10 is indeed a tight bound. However, since Princess is not able to recognise that the search for values

\problem {

[...]

->

// MinNum is supposed to be a lower bound of the number of soldiers who must have lost all 4

inj(1, 1, 1, 1) >= MinNum & MinNum > 10

}

`MinNum > 10`

is futile,
proof search won't terminate for the input at all and has to be stopped
manually after some while (by pressing the Stop button in the GUI).
A more elegant way to find the greatest lower bound is to tell
Princess
to search for the most general
constraint satisfying the original problem input (in the same
way as it was done in the first
example on this page). For this, we have to ensure termination of
proof search, and remove the cause of non-termination that occurred in
the first attempt (when adding the inequality `MinNum > 10`

):
the
totality
axiom
that
Princess
implicitly
generated
for
the
function
symbol
`inj`

. Intuitively, such totality axioms have the
form ```
\forall
int
x1,
x2,
x3,
x4;
\exists
int
y;
inj(x1, x2, x3, x4) = y
```

, and
the somewhat unfortunate property that they can be instantiated
indefinitely and thus prevent proof search from terminating. At the
same
time, for many applications (in particular for our riddle) the totality
property of functions is not
required. More details are given in this paper, and in the
next section on this page.

To generate the most general constraint on `MinNum`

for
the riddle, perform the following steps:

- Remove the inequality
`MinNum > 10`

from the problem input. - Add the options
`-genTotalityAxioms`

and`+mostGeneralConstraint`

(in the "Options" text field in the bottom of the Princess window) to switch off totality axioms and tell Princess to search for the most general constraint.

Proving ...

Formula is valid, resulting most-general constraint:

10 >= MinNum

Concrete witness:

MinNum = 10

- Total functions, which
are declared using a signature like
`int f(int, ..., int)`

, and for which both the functionality and totality axiom is automatically generated.

- Partial functions, which
are declared by adding the keyword
`\partial`

. For instance, in the riddle we could have written:\functions {

Declaring a function as partial has the consequence that no axiom expressing totality is generated; this means that some formulae become unprovable that would normally be expected to hold. The Princess option

\partial int inj(int, int, int, int);

}`-genTotalityAxioms`

has the effect of turning all functions into partial functions.

- "Relational" functions, which are functions without the functionality axiom (in other words, relational functions are not actually functions, just arbitrary relations with function syntax). Relational functions are sometimes useful for implementing decision procedures for theories with the help of axioms. You should probably not use relational functions, unless you know what you are doing.

The first encoding of the soldier riddle (using the function `inj`

)
was
still
not
exactly
elegant,
since
we
had
to
spell out a set of long
equations by hand. The equations corresponding to the riddle can also
be written in a more symbolic way, by introducing further uninterpreted
functions. To simplify things, we now encode the four integer arguments
of
the function `inj`

(each ranging over the set {0, 1}, i.e.,
encoding a single bit) as a single integer ranging over {0, 1, ...,
15}. It is then easy to compute the number of all soldiers (the sum ```
inj(0)
+
inj(1)
+
...
+
inj(15)
```

) using two axioms and a further
uninterpreted function `sum`

. We use partial functions at
this point,
since totality is not needed in the formalisation:

\functions {Triggers: Note the expression

\partial int inj(int);

\partial int sum(int);

}

\problem {

sum(0) = 0

&

\forall int x; {sum(x)} (x>0 -> sum(x) = sum(x-1) + inj(x-1))

&

sum(16) = 100 // 100 soldiers altogether

&

[...]

}

`{sum(x)}`

used in the second axiom:
this expression is a trigger
and tells Princess in which way the axiom is supposed to be handled.
Generally, triggers consist of a single or multiple expressions
(normally sub-expressions in the body of the quantified formula) that
contain all quantified variables. Princess uses the term `sum(x) `

as
a
pattern;
whenever
an
instance
`sum(t)`

of the pattern
occurs during proof search, she will create a ground instance of the
quantified axiom in which `x`

has been replaced with the
term `t`

. This will lead to the sum `sum(16) `

incrementally
being
computed
from
`sum(15)`

and `inj(15)`

,
then `sum(14)`

, and so on, in the same way as a recursive
procedure is evaluated.
The other conditions of the riddle can be captured in a similar way,
although slightly more complicated axioms are needed. In particular, we
have to define a binary function `bit`

for extracting
individual bits of an integer. The resulting formalisation is shown in
the next listing:

/*It can be observed that most, but not all of the quantified axioms contain hand-written triggers. For the remaining axioms, we can rely on the fact that Princess will automatically generate triggers if none are provided. This functionality is controlled by the option

Solve with options "-generateTriggers=all +mostGeneralConstraint"

*/

\existentialConstants {

int MinNum;

}

\functions {

\partial int inj(int);

\partial int sum(int);

\partial int pSum(int, int);

\partial int bit(int, int);

}

\problem {

// Recursive extraction of individual bits in an integer number

\forall int x1, x2, b; {bit(2*x1 + x2, b)} (

x2 >= 0 & x2 < 2 ->

(b > 0 -> bit(2*x1 + x2, b) = bit(x1, b-1)) &

(b = 0 -> bit(2*x1 + x2, b) = x2)

)

// Recursive computation of the sum "inj(0) + inj(1) + ... + inj(15)"

&

sum(0) = 0

&

\forall int x; {sum(x)} (x>0 -> sum(x) = sum(x-1) + inj(x-1))

// Recursive computation of the sum of the inj(i), for those i where bit b is set

&

\forall int b; pSum(0, b) = 0

&

\forall int x, b; {pSum(x, b)} (

x>0 -> pSum(x, b) = pSum(x-1, b) + (\if (bit(x-1, b) = 1) \then (inj(x-1)) \else (0)))

& sum(16) = 100 // 100 soldiers altogether

& pSum(16, 0) = 70 // 70 soldiers lost an eye

& pSum(16, 1) = 75 // 75 soldiers lost an ear

& pSum(16, 2) = 85 // 85 soldiers lost a leg

& pSum(16, 3) = 80 // 80 soldiers lost an arm

&

// inj is non-negative

\forall int x; inj(x) >= 0

->

// MinNum is supposed to be a lower bound of the number of soldiers who must have lost all 4

inj(15) >= MinNum

}

`-generateTriggers`

:- With the option
`-generateTriggers=none`

, no triggers are generated automatically, but triggers manually provided are exploited. Resulting quantified formulae without triggers are handled by instantiation with free variables, which is a very powerful method, but often less efficient than the use of triggers. More details are given in this paper. - With the option
`-generateTriggers=total`

(the default), only such triggers are generated that purely consist of total functions. - With the option
`-generateTriggers=all`

, triggers are generated both for total and for partial functions. Since our last formalisation of the riddle contains partial functions, this option needs to be specified when running Princess on the problem.