Pages: [1]   Go Down
Print
Author Topic: Esercizio 1 {semantica}  (Read 496 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
Kada
Matricola
*
Offline Offline

Posts: 15


« on: 02-01-2019, 22:44:11 »

salve, avrei dei dubbi su questo esercizio. Questo é il testo:

Supponiamo di voler introdurre nel linguaggio WHILE un nuovo tipo di istruzione della seguente forma:   for X1 do δ
La semantica informale di tale istruzione e' la seguente: se l'esecuzione di δ produce, tra le altre cose, un decremento della variabile X1, si ripete l'esecuzione di δ tante volte quanto e' il valore di X1.
Descrivere formalmente la semantica delle istruzioni for fornendo una o piu' regole di inferenza.

Questa é la soluzione presentata:

Occorre aggiungere il seguente assioma e la seguente regola di inferenza
('<>' indica "diverso da", mentre '|' rappresenta la freccia in giu', mentre su 'a' e 'b' si suppone ci sia la freccetta che indica il vettore)
                            

                                a1 = 0
              ____________________________________________
                   a, begin for x1 do delta end | a



    a1 <> 0     (a1, .. , an), begin delta end (a1 - 1, a'2, .. , a'n)     (a1 - 1, a'2, .. , a'n), for X1 delta b
________________________________________________________________________________________________________
               (a1, .. , an), begin for X1 delta end | b



i dubbi che ho, rispetto alla soluzione proposta sono:

1) nella prima regola, per poter dire che il comando FOR non fa nulla quando X1 = 0, non devo aggiungere come premessa cosa fa DELTA, visto che uno dipende strettamente dall'altro? Cosí com'é scritta, sembra dire "se X1 = 0, sia il DELTA che il FOR non producono effetti". In realtá, il DELTA viene eseguito comunque. é il ciclo FOR che non parte.

2) sempre nella prima regola, scrivendo "a, begin for x1 do delta end | a", sto dicendo che il vettore a resta invariato, ma in realtá non possiamo saperlo. L'unica cosa che sappiamo é che la variabile X1 non viene decrementata e che, quindi, il FOR non viene eseguito. Cosa accade alle variabili X2, ..., Xn dipende da DELTA che, pur non decrementando X1, potrebbe modificare le altre. Questo secondo dubbio alimenta il primo.

3) nella seconda regola, scrivendo "(a1 - 1, a'2, .. , a'n), for X1 delta b", dico che il vettore di stato viene modificato, ma non lascio intuire quante volte viene eseguito il FOR, né cosa accade alle variabili. Noi sappiamo che, se DELTA decrementa X1, DELTA verrá ripetuto tante volte quanto é il valore di X1. Quindi, alla fine, X1 sará 0.


per questi motivi, io l'ho risolto cosí:


                         a1 = 0     (a1, a2, ... , an), begin delta end | (a1, a'2, ... , a'n)
                 ____________________________________________________________________
                        (a1, a2, ... , an), begin for X1 do delta end | (a1, a'2, ... , a'n)



a1 <> 0  (a1, a2,...,an), begin delta end | (a1 - 1, a'2,.., a'n)  (a1 - 1, a'2,..., a'n), begin for X1 do delta end | (0, a"2,..., a"n)
___________________________________________________________________________________________________________________
                                     (a1, a2, ... , an), begin for X1 do delta end | (0, a"2, ... , a"n)



ho detto/scritto delle fesserie? se si, perché?
grazie anticipatamente.
« Last Edit: 07-01-2019, 23:15:32 by Kada » Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.066



WWW
« Reply #1 on: 08-01-2019, 12:58:46 »

Quote
1) nella prima regola, per poter dire che il comando FOR non fa nulla quando X1 = 0, non devo aggiungere come premessa cosa fa DELTA, visto che uno dipende strettamente dall'altro? Cosí com'é scritta, sembra dire "se X1 = 0, sia il DELTA che il FOR non producono effetti". In realtá, il DELTA viene eseguito comunque. é il ciclo FOR che non parte.

Sono le tue regole che definiscono il senso preciso dell'istruzione.
Dalla descrizione informale comunque si evince che il delta non viene eseguito se X1=0.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.066



WWW
« Reply #2 on: 08-01-2019, 13:00:31 »

Quote
2) sempre nella prima regola, scrivendo "a, begin for x1 do delta end | a", sto dicendo che il vettore a resta invariato, ma in realtá non possiamo saperlo. L'unica cosa che sappiamo é che la variabile X1 non viene decrementata e che, quindi, il FOR non viene eseguito. Cosa accade alle variabili X2, ..., Xn dipende da DELTA che, pur non decrementando X1, potrebbe modificare le altre. Questo secondo dubbio alimenta il primo.

La semantica che si vorrebbe dare e' che se X1 e' zero,  allora l'effetto dell'istruzione FOR e' nullo.
In questo caso il delta non deve essere eseguito
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.066



WWW
« Reply #3 on: 08-01-2019, 13:05:53 »


Quote
                         a1 = 0     (a1, a2, ... , an), begin delta end | (a1, a'2, ... , a'n)
                 ____________________________________________________________________
                        (a1, a2, ... , an), begin for X1 do delta end | (a1, a'2, ... , a'n)


Questo puoi scriverlo solo se vuoi che anche con X1=0 esegui comunque il delta.
Ma questo non e' quanto specificato dalla semantica informale.
Se fai cosi', il ciclo viene eseguito X1 volte.....


Quote
a1 <> 0  (a1, a2,...,an), begin delta end | (a1 - 1, a'2,.., a'n)  (a1 - 1, a'2,..., a'n), begin for X1 do delta end | (0, a"2,..., a"n)
___________________________________________________________________________________________________________________
                                     (a1, a2, ... , an), begin for X1 do delta end | (0, a"2, ... , a"n)

Questa regola e' esattamente equivalente a quella della soluzione.
E' solo inutilmente piu' lunga da scrivere.


Logged
Kada
Matricola
*
Offline Offline

Posts: 15


« Reply #4 on: 08-01-2019, 14:08:35 »

Quote
2) sempre nella prima regola, scrivendo "a, begin for x1 do delta end | a", sto dicendo che il vettore a resta invariato, ma in realtá non possiamo saperlo. L'unica cosa che sappiamo é che la variabile X1 non viene decrementata e che, quindi, il FOR non viene eseguito. Cosa accade alle variabili X2, ..., Xn dipende da DELTA che, pur non decrementando X1, potrebbe modificare le altre. Questo secondo dubbio alimenta il primo.

La semantica che si vorrebbe dare e' che se X1 e' zero,  allora l'effetto dell'istruzione FOR e' nullo.
In questo caso il delta non deve essere eseguito

ah ok. credevo che il delta andasse eseguito in ogni caso e che poi, a seconda del risultato, si dovesse valutare se eseguire il for. cosí mi torna, grazie.



Quote
a1 <> 0  (a1, a2,...,an), begin delta end | (a1 - 1, a'2,.., a'n)  (a1 - 1, a'2,..., a'n), begin for X1 do delta end | (0, a"2,..., a"n)
___________________________________________________________________________________________________________________
                                     (a1, a2, ... , an), begin for X1 do delta end | (0, a"2, ... , a"n)

Questa regola e' esattamente equivalente a quella della soluzione.
E' solo inutilmente piu' lunga da scrivere.




scrivendo B come vettore di stato finale (come fatto nella soluzione), si perde parte della nostra conoscenza, ovvero il fatto che x1 alla fine sará zero. non dovremmo specificarlo?
« Last Edit: 08-01-2019, 14:20:43 by Kada » Logged
Pages: [1]   Go Up
Print
Jump to: