Calcolare gli assegnamenti
Ieri sera alla riunione del Milano XP User Group abbiamo parlato di come “calcolare” gli assegnamenti, ovvero, come fare in modo che uno statement conservi un invariante e allo stesso tempo faccia progresso verso la fine del loop. Ad esempio, supponiamo di voler calcolare una tabella di quadrati, con la limitazione che non possiamo usare la moltiplicazione. (Perché no? Magari perché sul nostro processore la moltiplicazione è lenta). Abbiamo due variabili s e n che soddisfano l’invariante s = n2. Vogliamo incrementare n, e conservare l’invariante. In altre parole, vogliamo trovare un’espressione E che soddisfi
{ s = n2 } s, n := E, n+1 { s = n2 }
In pratica questa è un’equazione in cui l’incognita E è l’espressione che manca per completare il programma
while n != N do
s, n := E, n+1
println "il quadrato di " n " è " s
end
L’obiettivo è essere in grado di calcolare l’espressione E che mi serve, senza doverci “pensare”. Qual’è allora la procedura? Per dimostrare
{ P } x := E { Q }
devo dimostrare che P implica Q[x:=E], dove Q[x:=E] significa sostituire x con E all’interno di Q. Nel nostro caso:
s = n2[s, n := E, n+1]
sse // applico la sostituzione
E = (n+1)2
sse // svolgo il quadrato
E = n2 + 2n + 1
sse // sfrutto l’invariante
E = s + 2n + 1
sse // le moltiplicazioni sono vietate
E = s + n + n + 1
Voilà: ho dimostrato che s=n2 implica s=n2[s, n := E, n+1] se scelgo E=s+n+n+1. Il programma desiderato è dunque
while n != N do
s, n := s+n+n+1, n+1
println "il quadrato di " n " è " s
end
Per saperne di più:
- Owen Astrachan, Pictures as Invariants
- Roland Backhouse, Algorithmic Problem Solving
September 18th, 2008 at 14:29
Interessante articolo, complimenti.
Per renderlo più leggibile cambierei la notazione dell’assegnamento da:
s, n := E, n + 1 in
s := E
n := n + 1
(stessa cosa nella notazione matematica) lo rende IMHO più leggibile, tra l’altro lo stesso Astrachan dice che uno dei motivi per cui è poco diffuso l’uso degli invarianti è dovuto alla notazione matematica non molto chiara.
September 18th, 2008 at 17:52
Ma in linguaggi come Ruby l’assegnamento simultaneo esiste e si usa:
x, y = y, x
al posto di
temp = x
x = y
y = temp
Il fatto è che non tutti gli assegnamenti si possono eseguire in un ordine arbitrario senza conseguenze…
September 21st, 2008 at 23:54
Matteo, alla tua affermazione In linguaggi come Ruby l’assegnamento simultaneo
esiste e si usa vorrei rispondere:
è anche per questo che la complessità di Ruby è elevata ed alcuni programmatori,
come me, si rifiutano di utilizzarlo.
Perché l’assegnamento simultaneo alza la complessità? A mio avviso perché il
cervello umano, almeno il mio, è una macchina
fondamentalmente sequenziale.
Nel tuo esempio, quando applichi la prima sostituzione, giungi alla formula
E=(n+1)2. Qui l’assegnamento simultaneo potrebbe
disorientare per un attimo chi ti sta seguendo. Ci si potrebbe infatti chiedere
se n a questo punto sia già stato incrementato oppure no.
A mio parere l’esposizione sarebbe molto più comprensibile se partisse da
{s=n2} s:=E {s=(n+1)2}
A suffragare la mia convinzione che l’assegnamento simultaneo alzi, inutilmente,
la complessità dell’argomento, penso possa esserci anche una considerazione di tipo teorico.
Su questo terreno, però, non mi trovo a mio agio e probabilmente
sto per dire delle grosse inesattezze: so che saprai correggimi se dovessi sbagliare.
A dimostrazione della complessità dell’assegnamento simultaneo, dicevo, sta il
fatto che la sua semantica non può essere compresa dall’insieme originale di assiomi
proposti da Hoare nel suo lavoro originale,
ma richiede, se non erro, l’introduzione di un nuovo schema di assiomi:
{P(x0/E0, x1/E1,…,xn/En)}
x0, x1,…,xn := E0, E1,…,En
{P(x0, x1,…,xn)}
Citerei quindi lo stesso Hoare. It seems likely that a language which can
be described by a few “self-evident” axioms […] will be preferable to a language
with many obscure axioms. Non che questo nuovo assioma sia particolarmente oscuro,
però è comunque un assioma in più.
Cambiando parzialmente argomento, nella riunione dell’XPUG Milano chiedevi suggerimenti per
accostare la logica di Hoare ai metodi agili. Qualcosa si può trovare ancora nella
già citata pubblicazione di Hoare, dove l’autore propugna l’adozione della verifica formale
di correttezza dei programmi sia per alzare la qualità del software, sia per fornire una forma
di documentazione automatica del codice. E’ quindi evidente l’analogia tra la logica di
Hoare e la pratica dei test unitari.
September 22nd, 2008 at 09:04
Ciao Franco, grazie per la risposta.
La mia risposta di prima era troppo sbrigativa. Il fatto è che non è semplice spiegare questa tecnica in poche righe. Per ridurre al minimo il numero di regole da imparare, ho usato l’assegnamento simultaneo; altrimenti se usi la sequenza
s := E ; n := n + 1
ti tocca avere una regola per l’assegnamento e una per la sequenza.
Lo schema di assiomi dell’assegnamento simultaneo è in realtà una generalizzazione di quello per l’assegnamento singolo. Devi solo fare il passaggio fra “sostituire una variabile con un espressione”, a “sostituire un vettore di variabili con le corrispondenti espressioni.”
Non sono sicuro di capire perché trovi complicato l’assegnamento simultaneo; considera ad esempio il problema di scambiare il valore di due variabili x e y. A me sembra che la sequenza
temp := x; x := y; y := temp
sia più difficile da scrivere e da leggere di
x,y := y,x
Sono d’accordo con le tue considerazioni sull’utilità della logica.
September 22nd, 2008 at 23:18
Matteo, anche io sono stato forse troppo sbrigativo nel mio intervento. Quel che intendevo dire è che l’assegnamento simultaneo complica inutilmente quell’esempio, e io penso anche molti altri, mentre ovviamente rende più semplice lo scambio di valori tra variabili. Personalmente ritengo più comprensibili i due assiomi dell’assegnamento e della sequenza che l’assioma dell’assegnamento simultaneo, proprio per la già citata conformazione sequenziale del mio cervello (forse bacato).
Tu dici che l’assioma dell’assegnamento simultaneo è una semplice generalizzazione di quello dell’assegnamento singolo. Io ho il sospetto che un logico potrebbe dimostrare l’indipendenza dei due assiomi, e quindi la sostanziale diversità tra essi. Ma questo è solo una mia ipotesi.
September 23rd, 2008 at 07:59
Matteo,
mi sono reso conto di aver detto una grossa stupidata :-(
Suppongo che dagli assiomi originali di Hoare non sia derivabile l’assioma dell’assegnamento multiplo. Ovviamente, però, prendendo per valido l’assioma dell’assegnamento multiplo si ha come caso particolare l’assegnamento semplice.