Developing invariants for comparing two strings

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

X = S1
Y = S2

E = true
// (1)
while X != /\ and Y != /\ and E == true
X = tail(X)
Y = tail(Y)
else
E = false
// (2)
if !(X == /\ and Y == /\)
E = false
// (3) S1 != S2 \land E = false
// (4) S1 = S2 <=> E = true
return E


I want to develop invariants at points (1) and (2).

The invariant at (1) I choose is $$S_1 = S_2 \iff X = Y \land E = true.$$

From it, I can derive an invariant at (2):

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

Then I tried to simplify the formula:

$$(S_1 = S_2 \iff X = Y \land E = true) \land (X = \Lambda \lor Y = \Lambda \lor E = false)\\ \equiv \big((S_1 = S_2 \iff X = Y \land E = true) \land (X = \Lambda)\big) \lor \\ \big((S_1 = S_2 \iff X = Y \land E = true) \land (Y = \Lambda)\big) \lor \\ \big((S_1 = S_2 \iff X = Y \land E = true) \land (E = false)\big) \\ \equiv (S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true) \lor \\ (S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true) \lor \\ \big((S_1 = S_2 \iff X = Y \land E = true) \land (E = false)\big)\\ \equiv \big(S_1 = S_2 \iff (X = \Lambda \land Y = \Lambda) \land (E = true)\big) \lor \\ \big((S_1 = S_2 \iff X = Y \land E = true) \land (E = false)\big)$$

My problems are

• Is the derivation above correct? If so, how to further simplify this formula? In particular, how to deal with the second disjunction? Is it simply $S_1 \neq S_2 \land E = false$?
• How does the invariant at (3) and (4) follow from the one at (2)?
• Can we obtain an invariant at (2) in a single conjunct instead of multiple disjuncts?
• what does "invariant" mean here? – alim Mar 9 '18 at 6:22
• @alim I use the meaning as in loop invariant: they are true whenever reached. – hengxin Mar 9 '18 at 11:09

I would not simplify $(2)$ at all. Just apply the rules for if, =, and command composition. Use weakening (pre- or post- rules) when convenient to do so.

Below, I added an empty else branch for clarity.

// (2): (S1 = S2 <=> X = Y \land E = true)
//            \land \lnot(X != /\ \land Y != /\ \land E = true)
if !(X == /\ and Y == /\)
// (3a): (2) \land (X != /\ \lor Y != /\)
// (3b): S1 != S2 \land false = false
E = false
// (3): S1 != S2 \land E = false
// (4): S1 = S2 <=> E = true
else
// (3c): (2) \land X = /\ \land Y = /\
// (4): S1 = S2 <=> E = true
// (4): S1 = S2 <=> E = true
return E


Above, we used weakening, so we are left with proving:

• $3a\implies 3b$. By contradiction, assume $\lnot 3b:\ S_1=S_2$ and $3a$. Since $S_1=S_2$, then by $2$ (part of $3a$) we have that $X=Y \land E=true$. We also know that at least one of $X,Y$ is not empty from $3a$, hence both are not empty since they are equal. This contradicts the last part of $2$, namely $\lnot(X\neq\Lambda \land Y\neq\Lambda \land E=true)$.
• $3 \implies 4$. Two truths are always equivalent.
• $3c \implies 4$. Replacing both $X,Y$ in $2$ with $\Lambda$, the first part of property $2$ immediately simplifies into $4$.

The first item can also be proved more formally, but I think you get the idea.

$$\begin{array}{l} \big((S_1 = S_2 \iff X = Y \land E = true) \land (X = \Lambda)\big) \\ \equiv (S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true) \end{array}$$
However, this does not hold in general, e.g. for $X={\sf x}, Y={\sf y}, S_1=\Lambda, S_2={\sf h}, E=true$. Or, more in general, when $X$ is non empty, and $S_1\neq S_2$. In such case, the former is false, but the latter is true.
• Your arguments sound reasonable to me. However, why is "but the latter is true" in the counterexample you give? Isn't $S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true$ an invariant at point (2)? – hengxin Mar 10 '18 at 6:32
• @hengxin That property indeed seems to hold at (2). I'm only saying that the logical justification you gave is not correct, since the equivalence you used does not hold, in general. The claim "but the latter is true" follows from $S_1=S_2$ being false, and $Y=\Lambda$ being false, so both sides of $\iff$ become false, hence the $\iff$ itself becomes true. – chi Mar 10 '18 at 7:27