{y>=0}
  z := 1;
  c := y;
{z=x^(c-y)}        
  while (c not= 0) do
{c not= 0, z=x^(y-c)}
  z := z*x;
  c := c-1
{z=x^(y-c)}
  end
{c=0,z=x^(y-c)}    


Vediamo un po' in dettaglio come si puo' arrivare alla dimostrazione.

Quallo a cui vogliamo arrivare e' dimostrare la validita' del seguente 
giudizio della logica di Hoare:

{y>=0}
z := 1;
c := y;
while (c not= 0) do
z := z*x;
c := c-1
end
{z=x^y} 

Essendo il nostro programma composto da varie istruzioni, e' ovvio che 
occorrera' dimostrare dei giudizi per le varie istruzioni e poi utilizzare la
regola (composizione), vedi [US].

Quindi occorrera' dimostrare la validita' di

{y>=0}
z := 1;
c := y;
{D}

e di 

{D}
while (c not= 0) do
z := z*x;
c := c-1
end
{z=x^y}    

per una formula D opportuna.

Per dimostrare la validita' di un giudizio relativo all'istruzione while,
l'unica possibilita' e' utilizzare  la regola (iterazione), vedi [US].
Tale regola impone che la precondizione di un while sia necessariamente
identica alla postcondizione (la cosiddetta condizione invariante), tranne che per
la negazione della condizione del while (c not= 0 nel nostro caso).

Nel nostro caso quindi il giudizio relativo alla nostra istruzione while 
deve necessariamente avere la seguente forma:

{z=x^y}
while (c not= 0) do
z := z*x;
c := c-1
end
{z=x^y /\ c=0 }

A questo punto, sempre la regola (iterazione) ci dice che per dimostrare la
validita' di questo giudizio occorre dimostrare la validita' del giudizio
relativo alla premessa della regola, e cioe' la validita' di

{z=x^y /\ (c not= 0)}
z := z*x;
c := c-1
{z=x^y}

Essendo questo un giudizio relativo ad una seguenza di assegnamenti,
l'unica possibilita' per dimostrarne la validita' e' di utilizzare
l'assioma (assegnamento), vedi [US].
Questo pero' non e' possibile, poiche' nel giudizio

{z=x^y /\ (c not= 0)}
z := z*x;
c := c-1
{z=x^y}

la formula z=x^y (l'invariante), se vera prima delle istruzioni, dovrebbe rimanere vera 
anche dopo le istruzioni.
E' chiaro invece che se z vale x^y prima dell'esecuzione dei due assegnamenti,
non potra' avere lo stesso valore dopo.
Osserviamo pero' che i nostri due assegnamenti sono il corpo di un ciclo in cui
all'inizio c e' maggiore o uguale a zero, ed alla fine c vale 0.
Capiamo quindi che se al posto di utilizzare {z=x^y} come post-condizione
dell'istruzione while utilizziamo {z=x^(y-c)} il senso della post-condizione
finale rimane invariato (poiche' alla fine del ciclo c vale 0).
Inoltre la pre-condizione  del while diventerebbe ora {z=x^(y-c)}.
Tale condizione e' vera all'inizio del ciclo poiche' all'inizio del
ciclo z vale 1 e c vale y (infatti 1=x^(y-y) ).
La formula z=x^(y-c) e' una invariante di ciclo, poiche'
si puo' vedere che il giudizio

{z=x^(y-c) /\ (c not= 0)}
z := z*x;
c := c-1
{z=x^(y-c)}

e' valido: infatti, ad ogni ciclo, z viene sostituita con z*x, e c con c-1.
Questo fa si' che l'uguaglianza z=x^(y-c) rimanga vera dopo ogni ciclo.
Per dimostrarlo piu' formalmente utilizziamo l'assioma (assegnamento)
(per semplicita' utilizziamo un solo assioma per entrambi gli assegnamenti)

Il seguente e' una istanza corretta dell'assioma (assegnamento):

{z*x=x^(y-(c-1)) /\ ((c-1)+1 not= 0)}   
z := z*x;
c := c-1
{z=x^(y-c) /\ ((c+1) not= 0)} 

(notare che ( z*x=x^(y-(c-1)) /\ ((c-1)+1 not= 0) ) e' (z=x^(y-c)/\((c+1) not= 0))[(z*x)/z,(c-1)/c]
e che
z*x=x^(y-(c-1)) coincide, semplificando l'espressione, con z=x^(y-c) /\ ((c-1) not= 0).)

Quindi, utilizzando l'assioma (assegnamento), abbiamo che 

{z=x^(y-c) /\ (c not= 0)}
z := z*x;
c := c-1
{z=x^(y-c) /\ ((c+1) not= 0)}

e' un giudizio valido.

Pero' non e' esattamente quel che ci serviva (c'e' la parte ((c+1) not= 0) in piu' nella post-condizione).
Notiamo pero' che, banalmente, la seguente formula e' vera:
(z=x^(y-c) /\ ((c+1) not= 0)) -->  z=x^(y-c)
Possiamo quindi utilizzare la regola di indebolimento della post-condizione, vedi [US]2.6,
per ottenere

{z=x^(y-c) /\ (c not= 0)}
z := z*x;
c := c-1
{z=x^(y-c)}

Per completare la dimostrazione di correttezza del nostro codice occorre ora dimostrare che

{y>=0}
z := 1;
c := y;
{z=x^(y-c)}

e' un giudizio valido.

Questo si ottiene facilmente utilizzando l'assioma (assegnamento).
Il seguente e' infatti una istanza corretta dell'assioma (assegnamento):

{y>=0 /\ 1=1 /\ y=y}
z := 1;
c := y;
{y>=0 /\ z=x^(y-c) /\ c=y}

(notare che (y>=0 /\ 1=1 /\ y=y) e'  (y>=0 /\ z=x^(y-c) /\ c=y)[1/z,y/c],
tenendo conto che 1=x^(y-y) )

Ora, poiche' le seguenti formule sono vere:
(y>=0) --> (y>=0 /\ 1=1 /\ y=y)
(y>=0 /\ z=x^(y-c) /\ c=y) --> z=x^(y-c)
possiamo utilizzare le regole di rafforzamento della pre-condizione e di
indebolimento della post-condizione, vedi [US]2.6,
per ottenere

{y>=0}
z := 1;
c := y;
{z=x^(y-c)}

che e' esattamente cio' che ci serve.

L'uso della regola (iterazione) e dell'indebolimento della post-condizione
(poiche' e' vero che (c=0 /\ z=x^(y-c)) --> z=x^y ),
permette di derivare il giudizio che 
ci serve, e che dimostra la correttezza del nostro codice relativamente
alla specifica richiesta:

{y>=0}
  z := 1;
  c := y;
  while (c not= 0) do
  z := z*x;
  c := c-1
  end
{z=x^y}


Ovviamente, in una dimostrazione meno formale, molti passaggi 
si potrebbero tranquillamente evitare, giustificandoli in modo informale.