Fondamenti di Informatica, 1 Luglio 2014

Non e' ammesso l'uso di alcun testo, appunti, calcolatrici o qualsivoglia app per smartphone. Le risposte vanno scritte nel foglio di bella copia. Si raccomanda la massima SINTETICITA'. L'eccessiva verbosita' verra' considerata negativamente.
Occorre essersi prenotati sul portale studenti del nostro ateneo. Se cio' non e' stato fatto, comunicatelo immediatamente al docente o all'assistente in aula.

I risultati verranno indicati nella pagina web del corso. Date ed orari degli orali, sul Forum.

Esercizio 1
(a) Nel contesto della Logica Proposizionale (Calcolo Proposizionale), fornire le definizioni di

assegnamento proposizionale
tautologia
fbf (formula ben formata) soddisfacibile
fbf contraddittoria

(b)
Ricopiare la seguente deduzione sostituendo correttamente i "???"

                    [A]1      [A→B]3 
                --------------------------- (→E)
                            ???                             [¬B]2
                     ------------------------------------------------- (¬E)
                                             ???      
                                            -----
                                             ???
                                      ----------------- (→I)2
                                             ???
                                   ------------------------ (???)3
                                        (A→B) → ((¬B)→¬A)

(c) Nel contesto della Logica Proposizionale, dire, fornendone giustificazione, se la seguente affermazione e' corretta o meno:

Se non esiste alcuna derivazione di α da un insieme di ipotesi Γ , allora Γ |- ¬α

Esercizio 2
(a) Che cosa e', a cosa serve la Logica di Hoare? Che forma hanno in giudizi della Logica di Hoare? Qual e' la definizione di giudizio valido nella Logica di Hoare?
(b) La seguente regola della Logica di Hoare contiene un errore. Individuarlo, correggerlo e giustificare la correzione. Mostrare inoltre come, utilizzando la regola cosi' com'e' si potrebbe derivare un giudizio non valido partendo da giudizi validi.

{A ∧ E} I₁ {B} {B ∧ ¬E} I₂ {B}
-------------------------------------------------
{A} if E then I₁ else I₂ fi {B}

(c) Fornire l'invariante di ciclo per il ciclo while contenuto nel seguente codice e che permetta di dimostrare che al termine dell'esecuzione del codice la variabile booleana "pari" contenga true se e solo se a e' pari.

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

Esercizio 3
Definire la grammatica regolare G che genera il linguaggio sull'alfabeto {a,b} composto dalle stringhe caratterizzate dal fatto che il penultimo carattere e' b.
Definire poi un ASFD che riconosca le stringhe del linguaggio generato da G.