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          
  if head(X) == head(Y)           
    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?

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.

About your attempt: you used the equivalence

$$
\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.

StackExchange Computer Science Q#89061, answer score: 3