Sviluppare invarianti per confrontare due stringhe

Question

Il seguente algoritmo dovrebbe confrontare due stringhe $ s_1 $ e $ s_2 $ ("/" per stringa vuota):

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

Voglio sviluppare invarianti in punti (1) e (2).

L'invariante a (1) scelgo è $$ s_1 = s_2 iff x = y land e = true. $$

Da esso, posso derivare un invariante a (2):

$$ (s_1 = s_2 iff x = y land e = true) land lnot (x neq lambda land y neq lambda land e = true). $$

Quindi ho provato a semplificare la 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 terres 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 land Y = lambda terres = 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) $$

I miei problemi sono

• La derivazione sopra è corretta? In tal caso, come semplificare ulteriormente questa formula? In particolare, come affrontare la seconda disgiunzione? È semplicemente $ s_1 neq s_2 land e = false $?
• Come seguono l'invariante a (3) e (4) da quello a (2)?
• Possiamo ottenere un invariante a (2) in un singolo congiunto anziché più disjuncts?