Invariants

Invariants

Example 8.1. Suppose the following assignment is executed with (u, v) = (20,15). We can annotate before and after the assignment.

-- before: u, v = 20, 15 u, v :=u+5,v-5

--after: u, v = 25, 10

After assignment (u, v) = (25, 10). But what do you observe about the value of the function u + v?

before: u + v = 20 + 15 = 35

after:  u + v = 25 + 10 = 35

The assignment has not changed the value of u + v. We say that u + v is an invariant of the assignment. We can annotate before and after the assignment with the invariant expression.

--before: u + v = 35 u, v : = u + 5, v - 5

--after : u + v = 35

We can say, u + v is an invariant: it is 35 before and after. Or we can say u + v =35 is an invariant: it is true before and after.

Example 8.2. If we execute the following assignment with (p, c = 10, 9), after the assignment, (u, v) = (11, 10).

--before : p, c = 10 , 9 p, c := p + 1, c+1

--after: p, c = 11 , 10

Can you discover an invariant? What is the value of p - c before and after?

before: p — c = 10 — 9 = 1

after: p — c = 11 — 10 = 1

We find that p - c = 1 is an invariant.

In general, if an expression of the variables has the same value before and after an assignment, it is an invariant of the assignment. Let P(u, v) be an expression involving variables u and v. P(u, v)[u, v:= el, e2] is obtained from P(u, v) by replacing u by el and v by e2 simultaneously. P(u, v) is an invariant of assignment u, v := el, e2 if

P(u,v) [u,v := el, e2] = P(u,v)

Example 8.3. Show that p - c is an invariant of the assignment

p, c := p + 1, c + 1

Let P(p, c) = p - c. Then

P (p, c) [p, c := p + 1, c + l]

=p — c [p, c := p + 1, c + l]

=(p + 1) — (c + 1)

=p — c

=P(P , c)

Since (p - c)[p, c := p+l, c+l] = p

-c, p - c is an invariant of the assignment p, c := p + 1, c + 1.

Example 8.4. Consider two variables m and n under the assignment

m, n := m + 3, n - 1

Is the expression m + 3n an invariant?

Let P(m, n) = m + 3n. Then

P(m, n) [m, n := m + 3, n — l]

= m + 3n [m, n := m + 3, n — l]

= (m + 3) + 3(n — l)

=m + 3 + 3n — 3

=m + 3n

=P(m, n)

Since (m + 3n) [ m, n : = m + 3, n - 1] = m + 3n, m + 3n is an invariant of the assignment m, n := m + 3, n - l.