• English only

# Lecture 2

## Manually proving an example

For software verification. Programs must be represented as logical formulas. These logical formulas can be used for proving invariants. This lecture explains the base theory about Propositional logic, First Order logic and Relations.

Recall our example from Lecture 1, with a loop invariant:

    public static int sum(int a0, int n0)
/*:
requires "a0 > 0 & n0 > 0"
ensures "result > 0"
*/
{
int res = 0, a = a0, n = n0;
while //: inv "a > 0 & res >= 0 & (n = n0 | res > 0)"
(n > 0)
{
a = 2*a;
res = res + a;
n = n - 1;
}
return res;
}

To prove ensured properties in the program, one first has to prove that this program will terminate or not, and then by showing that the program doesn't violate the required property prove it is complete. In case of loops in the program, an invariant of a loop in terms of a logical formula is needed such that after any number of iterations of the loop the invariant continues to hold. To prove the invariant for the above while loop, we have to show that after each iteration of the loop this invariant still holds. As we can observe the following logical formula shows that above invariant is true.

## Logical preliminaries

We used these constructs in mathematics all the time. Formalizing them is useful for

• foundation of mathematics
• proving formulas automatically: need to represent formulas and make correct reasoning steps on them

### Propositional logic

Basic propositional operations:

A formula of the propositional calculus is a string generated by the following grammar:

We can simplify this grammar and only use conjunction, disjuntion and negation by observing that the implication and equivalency relations can be expressed as:

Example formula:

We further define the interpretation of a formula. Let F be a propositional formula and let be the set of atoms appearing in F. An interpretation for F is a function , that is, e assigns one of the truth values true or false to each atom.

we can also write the following:

where is in fact a binary math function.

We next give the definitions of satisfiability and validity: a propositional formula F is satisfiable if its value is true in some intepretation. A satisfying interpretation is called a model for F. F is valid if its value is true in all interpretations – a valid propositional formula is also called a tautology. The notation is:

Is “false implies true” a valid formula?

Checking satisfiability is done by using a SAT solver. Now the question that arises is how to check for validity using a SAT solver ?

There are two ways of tackling the problem. One would be to notice that there are possibilities in total and just check for everyone of them if . The other is to convert to CNF or DNF and then use the existing techniques for solving.

SAT solvers: http://www.satlive.org/

#### Conjunctive Normal Form. Disjunctive Normal Form

We give the grammars for conjunctive normal form (CNF) and disjunctive normal form (DNF) as:

is the grammar for CNF, and

is the grammar for DNF.

### First-order logic (predicate calculus)

Predicate calculus is interesting because it supports quantifiers ( symbols). We define a predicate as a function from some arguments to a boolean value.

Example: “p divides q” is a binary predicate on p and q.

Predicate calculus is concerned with properties of predicates (regardless of what these predicates are).

Constructs in predicate calculus:

The syntax for first-order logic is given by:

Drinker's paradox (made more politically correct): in every restaurant there is a guest such that if this guest is having a dessert, then everyone in the restaurant is having a dessert.

Suppose predicate P(y) denotes that guest y is having a dessert. Then we can formally write the drinker's paradox as:

To prove the drinker's paradox formula holds true we have to notice that it can be reduced to a simple implication. Although implication is confusing in language, in logics we must note that P \rightarrow Q is false only if .

#### Semantics for First-order logics

for quantifiers we have:

Tarskian semantics for first-order logic.

Is there an algorithm for first-order logic?

Checking (and enumerating) proofs.

What is a formal proof?

### Sets and relations

A set can be thought of as any collection of distinct objects considered as a whole. For example,

We can define many operations over sets such as.

The Cartesian product is a direct product of sets. Specifically, the Cartesian product of two sets X and Y, denoted X × Y, is the set of all possible ordered pairs whose first component is a member of X and whose second component is a member of Y:

We will use binary relations on program states to represent the meaning of programs. A binary relation on set S is a subset of .

The diagonal relation is .

Because relation is a set, all set operations apply. In addition, we can introduce relation composition, denoted by circle

Then

Sets and predicates are interchangable.

turns set into predicate.

turns predicate into a set.

Here we present few properties of transition relation

Composition of a relation is associative:

Composition of a relation is not commutative

Composition of a relation is distributive over union

The property that is also true about composition of variables.

## Programs as relations

Now back to meaning of programs.

Simple programming language

x = exp
if (F) c1 else c2
c1 ; c2
while (F) c1

Consider a program that manipulates two integer variables.

What is the state - map from names to values.

What is the meaning of

• x=y+3
• x=x+y
• x=y+3 ; x=x+y

Observe how the following update commands are translated to binary relations:

If the above update commands appear one after another in a program then by relation composition they can be represented as the one relation:

## Programs as formulas

Can we represent relations symbolically?

In general? In our examples?

Accumulation of equalities.

## Guarded command language

Our simple language:

x = exp
if (F) c1 else c2
c1 ; c2
while (F) c1

Guarded command language:

assume(F)
c1 [] c2
c1 ; c2
assert(F)
havoc(x)
c1*

Relational semantics of guarded commands.

The following is the interpretation of special commands uses in Guarded Command Language.

Example of Guarded Command Language

Transforming language into guarded commands:

• conditionals:
if (F) c1 else c2

(assume(F); c1)  []
(assume(~F); c2)
• loops:
while (F) c1

(assume(F); c1)*;
assume(~F)
• loops, if we have loop invariants
while [inv I] (F) c1

assert(I);
havoc x1,...,xn;
assume(I);
(assume(~F) []
assume(F);
c1;
assert I;
assume(false));

Transformations such as these are used in Jahob, ESC/Java, Spec#.

## Weakest Preconditions

Weakest precondition of a set of states is the

What happens if r is deterministic (a function on states)?

Set of states - formula with state variables for one state.

Relation on states - formula with state variables for two states.

Important property: conjunctivity.

Weakest preconditions for guarded commands.

Weakest preconditions of assignments make wp very appealing.