X = Y and E = truewhile X != /\ and Y != /\ and E == t" />
Latest update

# Inference rules for deriving invariants in Hoare logic

2018-03-13 17:10:41

The following algorithm is supposed to compare two strings \$S_1\$ and \$S_2\$ ("/\" for empty string):

X = S1

Y = S2

E = true

// (1) S1 = S2 <=> X = Y and E = true

while X != /\ and Y != /\ and E == true

X = tail(X)

Y = tail(Y)

else

E = false

// (2) S1 = S2 <=> X = /\ and Y = /\ and E = true

if !(X == /\ and Y == /\)

E = false

// (3) S1 != S2 and E = false

else // an empty else

// (3') S1 = S2 <=> E = true

// (4) S1 = S2 <=> E = true

return E

There are five invariants:

(1). \$S_1 = S_2 \iff X = Y \land E = true\$

(2). \$S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true\$

(3). \$S_1 \neq S_2 \land E = false\$

(3'). \$S_1 = S_2 \iff E = true\$

(4). \$S_1 = S_2 \iff E = true\$

I can understand these invariants and how they are derived from the previous ones in an intuitive and thus informal way. For example, we can derive (3') from (2) as follows:

At point (2), we know that \$S_1\$ equals \$S

• There are two ways to answer the question.

The first is on the level of propositional logic. You have three statements, \$S_1=S_2\$, \$(X=\Lambda\wedge Y=\Lambda)\$, and \$E=true\$. Let's call them \$A\$, \$B\$, and \$C\$ for short. (2) is \$A\Leftrightarrow(B\wedge C)\$ and (3') is \$A\Leftrightarrow C\$. At point (3') we know \$B\$. Every assignment of the propositional variables that satisfies \$B\$ and (2) also satisfies (3'). In other words, at the position (3') we know

\$(A\Leftrightarrow(B\wedge C))\wedge B\$

from which

\$(A\Leftrightarrow C)\$

follows semantically. If the propositional proof system of your choice is complete, the above can also be derived using its rules.

The second answer addresses Hoare logic instead of propositional logic. Hoare logic has its own derivations. The neat thing is that most of them can be automated. And they work backwards. In the case at hand, (3') is derived from (4) by copy. After all, at the end of the else clause, the same invariant must hold as after the

2018-03-13 19:29:53