Loop invariants in logic

Question

I am working on some questions about hoare calculus/logic. The given program $\pi$ is:

$ x:=0; y:=1; WHILE \; \lnot x=n \; DO (y:=2y+x + 1; \; x:= x + 1) $

The hoare-logic rules that I can use are in the list below)
H1 {[$t$\x]$\varphi$} x := $t$ {$\varphi$}, provided that $t$ is free for $x$ in $\varphi$
H2 from {$\varphi$} $\pi_1$ {$\psi$} and {$\psi$} $\pi_2$ {$\chi$} follows {$\varphi$} ($\pi_1;\pi_2$) {$\chi$}
H3 from {$\varphi \wedge \epsilon$} $\pi_1$ {$\psi$} and {$\varphi \wedge \neg \epsilon$} $\pi_2$ {$\psi$} follows {$\varphi$} IF $\epsilon$ THEN $\pi_1$ ELSE $\pi_2$ {$\psi$}
H4 from {$\varphi \wedge \epsilon$} $\pi$ {$\varphi$} follows {$\varphi$} WHILE $\epsilon$ DO $\pi$ {$\neg \epsilon \wedge \varphi$}
H5 if $\varphi \rightarrow \varphi`$ and $\psi \rightarrow \psi`$ are true in M = (D, I), then: from {$\varphi`$} $\pi$ {$\psi`$} follows {$\varphi$} $\pi$ {$\psi$}

The questions are:

1) Show that $y = 3 \cdot 2 ^x - x - 2$ is a loop variant for the while-loop from the program $\pi$.
2) Prove $\{true\} \; \pi \{y = 3 \cdot 2^n -n - 2 \} $ .

An update for my solution for the first question, so far. Made some edits.

1) $ \{y = 3 \cdot 2 ^x - x - 2\} \; y:=2y+x + 1; \; x:= x + 1 \; \{y = 3 \cdot 2 ^x - x - 2\} $ Start

2) $ \{y=3⋅2x^{+1}−(x+1)−2\} \; x:= x + 1 \; \{y = 3 \cdot 2 ^x - x - 2\} $ H1. substitute $[x+1/x]$ in the precondition, starting from the right.

3) $ \{2y +x+1 = 3 \cdot 2 ^{x+1} - x - 3\} \; y:=2y+x + 1; \; \{y = 3 \cdot 2 ^x - x - 2\}$ H1. Substitution: $[y:=2y+x + 1;/y]$ in the precondition, starting from the right.

4) $ \{2y +x+1 = 3 \cdot 2 ^{x+1} - x - 3\} y:=2y+x + 1; \; x:= x + 1 \{y = 3 \cdot 2 ^x - x - 2\} $ H2 on 2,3

5) $ \{y = 3 \cdot 2 ^x - x - 2 \land \lnot x = n\} y:=2y+x + 1; \; x:= x + 1 \{y = 3 \cdot 2 ^x - x - 2\} $ H5 on 4

6) $\{y = 3 \cdot 2 ^x - x - 2\} WHILE \lnot x = n\ DO \; y:=2y+x + 1; \; x:= x + 1 \{y = 3 \cdot 2 ^x - x - 2\} $ H4, apply the loop

Question 2. I have continued the numbering:

7) $ \{y=1\} y:=1 \; \{y:=1\} \; $ H1

8) $ \{0=0\} x:=0 \{x:=0\} $ H1

9) $ \{0=0\} x:=0; \; y:=1 \{ x:=0 \} $ H2, 7,8

10) $ \{TRUE\} \; x:= 0 \; ;y:=1; \; \{y = 3 \cdot 2 ^x - n - 2\} \; $ H5,9

11) $ \{TRUE\} \; x:= 0 \; ;y:=1; \; WHILE \lnot x = n\ DO \; y:=2y+x + 1; \; x:= x+1 \{y = 3 \cdot 2 ^x - x - 2\} $ H2 on 6 and 10

Answer 1

Here's what we want to prove:

{y = 3*2^x - x - 2}
y := 2*y + x + 1;
x := x + 1;
{y = 3*2^x - x - 2}

Indeed, this follows easily after sticking another assertion between the two assignments:

{y = 3*2^x - x - 2}
y := 2*y + x + 1;
{y = 3*2^(x + 1) - x - 3}
x := x + 1;
{y = 3*2^x - x - 2}

To see why the first 3 lines hold, observe that: \begin{align*} &y = 3 \cdot 2^x - x - 2 \\ &\implies 2y + x + 1 = 2(3 \cdot 2^x - x - 2) + x + 1 \\ &\implies 2y + x + 1 = (3 \cdot 2^{x + 1} - 2x - 4) + x + 1 \\ &\implies 2y + x + 1 = 3 \cdot 2^{x + 1} - x - 3 \end{align*} Likewise, to see why the last $3$ lines hold, observe that: \begin{align*} &y = 3 \cdot 2^{x + 1} - x - 3 \\ &\implies y = 3 \cdot 2^{x + 1} - (x + 1) - 2 \end{align*}

---

For the second question, combine H4 with your loop invariant (after noting that the initial conditions satisfy the loop invariant) so that you can replace $x$ with $n$.