Voor onze analyse gaan we bewijzen dat voor elk programma in de taal While een semantisch equivalent programma in de taal Piet bestaat. 
Dit gaan we doen door voor elke constructie in While een programma in Piet te geven en vervolgens te bewijzen dat deze semantisch equivalent zijn met behulp van bewijsrijen in sos.
