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.