Formal Verification

{P (a/x)}
x := a
{P}

{x=a & y=b}
{x=a & y=b & x+y=a+b}
{y=b & x+y=a+b}
x := x+y
{y=b & x=a+b}
{x-y=a & y=b & x=a+b}
{x-y=a & x=a+b}
y := x-y
{y=a & x=a+b}
{y=a & x=a+b & x-y=b}
{y=a & x-y=b}
x := x-y
{y=a & x=b}


{x=a & y=b}
x:= x+y;
y:= x-y;
x:= x-y;
{x=b & y=a}



if (cond)
 stmt1
else
 stmt2
end if

(If-else-block}

If we already know:

{P & cond}



There is no algorithm that accepts a program P and an input X and is able to determine with 100% Yes or No, does P halt specifically on input X?

Let's say there is such an algorithm.  Call it HALT (P,X).

I will write a new program G(P).  It takes a program.

if (HALT (G,G))
  while (1);
else
 nothing;

Let's say I run G(G).  I pass G's source as the input to G.
Line 50:  If G halts on its own input, go into an on-purpose infinite loop.  So, if G(G) halts, it cannot possibly halt.
I guess G(G) doesn't halt, when I try it, the if statement is false, and so the program terminates immediately, so it does halt.

This is a contradiction, and the only assumption I made was that HALT (P,X) exists.

if (cond)
 stmt1
else
 stmt2
end if

(If-else-block}

If we already know:

{P & cond}
stmt1
{Q}

{P & ~cond}
stmt2
{R}

Then we can derive:

{P}
if cond
 stmt1
else
 stmt2
endif
{Q v R}

do
 stmt1
until cond
 stmt2
end do

If know that

{P v Q}
stmt1
{R}

AND

{R & ~cond}
stmt2
{Q}

I can derive:

{P}
do
 stmt1
until cond
 stmt2
end do
{R & cond}

...provided the loop terminates and this proof technique does not
address termination at all.

Euler:

1/1 + 1/4 + 1/9 + 1/16 + ... = pi^2 / 6