• Fornire la soluzione dell'esercizio 1(c) nel caso in cui l'istruzione for X1 do δ esegua X1 volte l'istruzione δ, ma durante l'esecuzione il valore di X1 non viene modificato (supponendo sempre che X1 non possa mai capitare a sinistra di un assegnamento in δ)
• Fornire la soluzione dell'esercizio 1(c) nel caso in cui nell'istruzione for X1 do δ sia permesso alla variabile X1 di trovarsi a sinistra di un assegnamento in δ, ed inoltre il valore di X1 venga decrementato automaticamente dall'istruzione ad ogni ciclo. Il ciclo termina quando X1 contiene 0.

• Estendere il linguaggio WHILE con un'istruzione if then else, specificando informalmente la sua semantica e formalizzando poi questa con assiomi e/o regole di inferenza.
  
• Soluzione.
• Estendere il linguaggio WHILE con un'istruzione tipo lo switch di JAVA, specificando informalmente la sua semantica e formalizzando poi questa con assiomi e/o regole di inferenza.

pari:=true;
b:=a;
while b≠0
   do  b:=b-1;
       pari:=not pari
endw

p:=a;
s:=b;
while p≠0
     do
        p:=p-1;
        s:=s+1
endw

{(Dispari(q)∧ Pari(r)}  r:=r+1; q:=r+r  {Dispari(r)∧ Pari(q)}

x3 := 0
while (x3 ≠ x1) and (x3 ≠ x2) do
	x3 := x3 + 1
end
if x1 ≠ x3 then
	M := x1
else
	M := x2

Programma ::=  Istr; | Istr;Programma
Istr ::=  m[x]<-0 | m[x]<-1 | m[x]<-m[y] | m[x]<-m[y]ANDm[z] | m[x]<-m[y]ORm[z] |  if B then Istr
B ::= m[x]=0 | m[x]=1 | m[x]=m[y]

m[x] <- 0     (nella cella di memoria di indirizzo x poni 0)
m[x] <- 1     (nella cella di memoria di indirizzo x poni 1)
m[x] <- m[y]  (nella cella di memoria di indirizzo x poni il contenuto della
               cella di indirizzo y)
m[x] <- m[y]ANDm[z]  (nella cella di memoria di indirizzo x poni l'OR del contenuto della
               cella di indirizzo y con quello della cella z)
m[x] <- m[y]ORm[z]  (nella cella di memoria di indirizzo x poni l'OR del contenuto della
               cella di indirizzo y con quello della cella z)
               

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

int fattIt(int n)
{ int f=1; /* definizione della variabile accumulatore */
int i=0; /* variabile contatore */
while (i!=n)
{ i++;
f *= i;
}
return f;
}

{s+c=a+b,c<>0}  s:=s+1; c:=c-1  {s+c=a+b}

pari:=true;
b:=a;
while b≠0
   do  b:=b-1;
       pari:=not pari
endw

{r≥0 ∧ b>0 ∧ (a= b*q + r) ∧ r≥b} q:=q+1; r:=r-b {r≥0 ∧ b>0 ∧ (a= b*q + r)}

Dimostrare tale giudizio (usando la regola del rafforzamento della precondizione, due volte la regola per l'assegnamento, la regola per la sequenza di istruzioni e la regola per l'indebolimento della postcondizione).

s:=a;
c:=b;
while c≠0 do
    s:=s+1;
    c:=c-1
endw

1. Quest'espressione e' un assioma della SOS del linguaggio WHILE
2. Quest'espressione e' una regola della SOS del linguaggio WHILE
3. Quest'espressione sarebbe un assioma della SOS del linguaggio WHILE se il vettore a sinistra avesse tutti 0
4. Quest'espressione non e' neanche una fbf della SOS del linguaggio WHILE

1. corretto
2. completo
3. ne' corretto ne' completo
4. in realta' questa affermazione e' scorretta

                a⃗, begin δ1 end ⇓ b⃗       b⃗, begin δ1; end ⇓ c⃗
(∃i.ai=0)  ------------------------------------------------------------
                         a⃗, begin cucu'δ1;δ2 end ⇓ c⃗


                a⃗, begin δ2 end ⇓ b⃗       b⃗, begin δ2; end ⇓ c⃗
(∀i.ai≠0)  ------------------------------------------------------------
                         a⃗, begin cucu'δ1;δ2 end ⇓ c⃗