1.15 Variabili
e Asserzioni sulle variabili e sui valori di uscita.
E’ spesso importante riflettere sul valore che una o più variabili possono avere ad un certo istante dell’esecuzione di un programma. Per questo motivo annoteremo i programmi scritti con le asserzioni sulle variabili:
chiamiamo cosí i commenti al programma in cui esprimiamo proprietà del valore delle variabili ad un certo istante dell’esecuzione del programma o di una sequenza di codice.
Le proprietà cui siamo interessati sono per lo piú relazioni di uguaglianza o confronto con valori immediati o espressioni dove compaiono altre variabili, cioè il valore di queste in quel medesimo istante.
Nello specificare queste proprietà non useremo un particolare linguaggio formale, ma useremo simboli matematici noti e stabiliremo alcune convenzioni che introdurremo via via che ne avremo bisogno. Da subito ci serve la convenzione per cui chiamiamo N il valore letto da tastiera o comunque dato in ingresso (vedremo piú in lá cosa puó voler dire in piú) per la variabile n; analogamente M per m e cosí via.
Vediamo degli esempi.
Riprendiamo qualcuno dei programmi che compaiono nei paragrafi precedenti e annotiamolo con asserzioni sulle variabili:
var m,n: integer;
begin
readln(m,n);
writeln(m+n);
end.
Lo annotiamo secondo quanto detto come segue:
var m,n: integer;
begin
{m ed n hanno valori non noti}
readln(m,n);
{m=M
e n=N }
writeln(m+n);
{m=M e n=N }
end.
Come abbiamo visto nell’esempio le asserzioni sono scritte nella forma sintattica di commenti {…} e riguardano i valori che le variabili m ed n hanno nel corso dell’esecuzione.
Accanto alle asserzioni sulle variabili specificheremo anche asserzioni sulla sequenza di dati in ingresso e sulla sequenza di dati in uscita. Per le sequenze di dati in ingresso stabiliremo di volta in volta un nome per esempio <D1, D2, …Dk> per una sequenza di k dati battuti sulla tastiera e per questi dati specificheremo al momento di inizio della esecuzione quindi come prima asserzione quali restrizioni di valori imponiamo per il corretto funzionamento dell’algoritmo specificato. L’asserzione sui dati in ingresso è anche detta Asserzione iniziale (AI).
Per i dati in uscita visualizzati su video spesso useremo semplicemente espressioni quali “a video sono comparsi i valori ….” come nell’esempio che segue. Per i programmi che abbiamo visto finora chiamamo Asserzione finale (AF) una asserzione sulla sequenza di tutti i dati prodotti sul video valida dopo l’esecuzione dell’ultima istruzione del programma.
Asserzione sui dati in uscita :
var m,n: integer;
begin
{AI m ed n hanno valori interi qualunque}
readln(m,n);
{m=M
e n=N }
writeln(m+n);
{m=M e n=N }
{AF a video é comparso il valore M+N}
end.
Il
programma visto ora è un esempio di programma completamente annotato con
asserzioni sulle variabili, sui dati di ingresso e sui dati in uscita.
Normalmente non saremo interessati ad una annotazione completa ma soltanto a
specificare le seguenti asserzioni:
· Asserzione iniziale (AI);
· Asserzione finale (AF);
· Asserzione Invariante di ciclo (IC): a questo tipo di
asserzione dedichiamo il paragrafo che segue.
1.15.2 Asserzioni
sulle variabili nelle istruzioni di ciclo.
Al paragrafo 1.8.1 abbiamo visto il programma:
var
i,n: integer;
begin
write('quante ripetizioni? ');
readln(n);
for
i:= 1 to n do writeln('Buongiorno, ragazzi!');
write(‘fine programma)
end.
Annotiamo questo programma come segue:
var
i,n: integer;
begin
{AI i ed n hanno valori interi qualunque}
write('quante ripetizioni? ');
readln(n);
{n=N
ed i ha valore non noto}
for i:= 1 to n do
{1<= i <= n e n=N e su video è comparso (i-1) volte
il
messaggio ‘Buongiorno, ragazzi’}
writeln('Buongiorno,
ragazzi!')
{i > n e n=N e su video è comparso n volte
il messaggio ‘Buongiorno, ragazzi’}
write(‘fine programma’)
{AF a video sono comparsi per n volte il
messaggio ‘Buongiorno, ragazzi’ ed
infine il messaggio ‘fine programma’}
end.
Le asserzioni all’interno dell’iterazione valgono ogni volta che l’esecuzione giunge al punto in cui sono specificate non importa se è la prima esecuzione dell’iterazione, la seconda o, per dire un numero, la settimae esecuzione dell’iterazione perché non viene specificato
{1<=
i <= n e n=N e su video è comparso 1 volta
il
messaggio ‘Buongiorno, ragazzi’}
oppure: {1<= i <= n e n=N e su video è comparso 2
volte
il
messaggio ‘Buongiorno, ragazzi’}
oppure: {1<= i <= n e n=N e su video è comparso 7 volte
il
messaggio ‘Buongiorno, ragazzi’}
bensí
in forma dipendente dal contatore i delle esecuzioni dell’iterazione viene
specificato per esempio:
{1<=
i <= n e n=N e su video è comparso (i-1) volte
il
messaggio ‘Buongiorno, ragazzi’}
Un altro esempio: la somma di N interi immessi da tastiera, con N immesso anch'esso da tastiera (naturalmente prima!). La annotazione non è completa.
var
i,n,x,somma: integer;
begin
write('quanti numeri vuoi sommare? ');
readln(n);
somma:=
0;
write('immetti ',n,' numeri: ');
for i:= 1 to n do begin
read(x);
somma:= somma + x;
{i è il numero di interi letti finora meno
il primo che era N, n=N,
x è l’ultimo dato letto, somma è la somma
di tutti i dati letti
finora
eccetto il primo che era N}
end;
writeln('la somma è ',somma)
end.