Definitezza• Vogliamo poter richiedere la “definitezza” delle

funzioni• introduciamo nuovi atomi Def(t) con t T(X)

la cui validità vuol dire che t è definito in A rispetto a V, cioè tA,V sA

• Oppure per ogni sort s S introduciamo un – predicato standard Defs:s

– con interpretazione fissa e coincidente con tutto il carrier di s

• Si ha che– t1 =e t2 equivalente a t1 = t2 Def(t1)

– Def(t) equivalente a t =e t

• Esercizio 13: Precisare cosa significa l’“equivalente” usato sopra. Provare poi le due affermazioni.

La logica• Completiamo la nostra logica con

l’uguaglianza esistenziale.Come derivati abbiamo l’uguaglianza forte e atomi per richiedere la definitezza dei termini

• Esercizio 14: Completare la definizione di L(X) e per includere le nuove formule e dare la corrispondente validità.

Esempi• “nuove” formule su list e X = {x: int, l: list}

– Def(0), Def(empty)– top(push(x,l)) = x top(push(x,l)) =e x– top(empty) = 0, pop(empty) = empty– push(top(l),pop(l)) = l (*)

• * è valida in L (L |= * ) ?– No, poiché

• V1 t.c. V1(l) = 0 L |=V1 * • V2 t.c. V2(l) = L |≠V2 *

– Invece isEmpty(l) push(top(l),pop(l)) = lè valida in L

• Esercizio 15: dettagliare le affermazioni precedenti.• Esercizio 16: Esibire delle formula con ugualianza e

definitezza valide e non valide in L.

Strettezza• Funzioni (e predicati) in quest’approccio sono stretti, cioè

restituiscono un valore (sono veri) solo su argomenti definiti• Prop. Fissate una segnatura = (S,F,P), una S-famiglia X di

variabili, termini ti T(X)si, una -algebra A e una valutazione

V: XA.1) Per ogni f: s1 … sn s F, A|=V Def(f(t1,…,tn)) implica A|=V Def(ti)

2) Per ogni p: s1 … sn P, A|=V p(t1,…,tn) implica A |=V Def(ti)

• Prova1) A|=V Def(f(t1,…,tn)) se e solo se f(t1,…,tn)A,V sA cioè, per definizione di

interpretazione, se e solo se t1A,V= a1s1

A,…,tnA,V = ansn

A e f(t1,…,tn)A,V = f A(a1,…,an)sA, allora ti

A,VsiA e quindi A|=V Def(ti).

2) Analogamente (per esercizio)

• Quindi l’uguaglianza forte (che vale anche quando entrambi i lati non sono definiti) non può essere un predicato, mentre l’uguaglianza esistenziale sì.

Osservazioni• La logica parziale del prim’ordine ha lo stesso

potere espressivo di quella totale. • Nel definire la validità di una formula abbiamo

scelto di allontanarci il meno possibile dalla logica classica (totale).– Per questo non abbiamo cambiato il dominio di

valutazione delle formule, che possono essere solo vere o false: Logica a due valori

– Quindi abbiamo scelto che un’applicazione di predicato ad un termine indefinito valesse falso.Attenzione: questo non vuol dire che tutte le formule in cui compare un termine indefinito sono false, per esempio A|≠V Def(t) implica A|=V Def(t)

Logiche a tre valori• Una scelta più radicale sarebbe stata passare ad

una logica a 3 valori, in cui una formula può essere vera, falsa o indefinita.

• Logiche a 3 valori permettono di discriminare situazioni che le logiche a 2 valori inevitabilmente identificano.

• Però ai fini delle specifiche del sw funzionale e sequenziale, non sono strettamente necessarie (e quindi non le facciamo)

Specifiche• Una specifica Sp è una coppia (,Ax), dove

Ax L(X), detti assiomi di Sp.

• I modelli di Sp (semantica di Sp) sono tutte le -algebre che soddisfano tutti gli assiomi di Sp, cioè Mod(Sp) = {A | A -algebra e A|= ax per ogni ax Ax}

Esempio: specifica di “liste di interi”1• Splist =(list,PROPlist)

• PROPlist

– Def(0), Def(succ(x)) -- 0, succ totali

– 0 ≠ succ(x), x ≠ succ(x)

t1 ≠ t2 equiv. a t1 = t2

• Ci sono assiomi inutili ?

*

Proprietà di ogni funzione

– x = y succ(x) = succ(y) – x ≠ y succ(x) ≠ succ(y) -- succ iniettiva

– Def(empty), Def(push(x,l)) -- empty, push totali

– -- pop e top parziali• l ≠ empty Def(pop(l)) Def(top(l)) Def(pop(empty)) Def(top(empty))

– pop(push(x,l)) = l top(push(x,l)) = x

Esempio: specifica di “liste di interi” 2• Definizione di isEmpty

A) isEmpty(empty), isEmpty(push(x,l))B) isEmpty(l) <=> l = empty

F1 <=> F2 equiv. a

F1 F2 F2 F1

Esercizio 17: dare un ulteriore insieme di assiomi che definisca isEmpty. Esercizio 18: definire il predicato isIn.Esercizio 18bis: definire ulteriori combinatori derivati che si pensa possano essere utili.

C) isEmpty(l) l ≠ empty • Sono equivalenti le tre definizioni ?

– B e C yes– A e B no

• In una list-algebra esistono elementi che non

sono rappresentati nè da empty nè da push(x,l)

Modelli term-generated• Fra i modelli di una specifica sono particolarmente

interessanti i modelli term-generated (generati dai termini), cioè quei modelli in cui ogni elemento dei carrier è interpretazione di un termine senza variabili.

• Una -algebra A è detta term-generated se _A,: T()A surgettiva

• GMod(Sp) = { A | A Mod(Sp) e A è term-generated }

– Ci sono solo gli elementi necessari per interpretare le asserzioni sull segnatura

– Viceversa, ogni elemento in tali modelli è rappresentabile utilizzando la segnatura

– Permettono di utilizzare tecniche induttive

Occorre saper• Leggere/comprendere una specifica ?

Padronanza della semantica

• Controllare se un’algebra è un modello di una specificamodel-checking

• Ragionare sulle formule– Proprietà derivate

• Se un’algebra soddisfa una formula, allora deve soddisfare anche altre formule– Assiomi della logica

• formule che valgono in ogni algebra

Sistemi deduttivi

• Controllare se una specifica verifica una certa proprietà (tutti i suoi modelli la verificano)Sistemi deduttivi

• Trovare le proprietà di una struttura dati (assiomi di una specifica) ?guidelines

Esercizi• solita segnatura list

• Assumendo che I predicati isEmpty ed isIn rappresentino le due ovvie condizioni– Dire usando la lingua italiana/inglese che proprietà sulle

liste esprimono le seguenti formule• isEmpty(l) ˚ isIn(x,l)

• isEmpty(l) ˚ x:int . isIn(x,l) x:int . (isEmpty(l) ˚ isIn(x,l))

• isEmpty(l) ˚ x:int . isIn(x,l)

– Dare una formula che richieda che• se un numero diverso da zero appartenesse ad una lista, allora anche 0

apparterebbe alla medesima lista• il top di una lista appartenga alla lista stessa• Se un numero appartiene ad una lista, allora esiste una lista il cui top è

proprio tale numero

Model-checking• Data una specifica Sp = (,Ax), ed una -

algebra A come si fa a verificare se A è un modello di Sp?

• Basta usare la definizione– Si controlla se ogni assioma in Ax è valido in A

– Controllando se è valido per ogni valutazione delle sue variabili libere

Esempio• solita segnatura list ed algebra L

• L |= isIn(x,l) isIn(x,push(y,l))– Le variabili libere sono FV ={ x,y:int, l:list }– Si fissa una valutazione V per FV in A– Siano V(x), V(y) N e V(l) N*– Si applica la definizione di validità e di interpretazione un

passo alla volta• L |=V isIn(x,l) isIn(x,push(y,l)) sse

L |≠V isIn(x,l) o L |=V isIn(x,push(y,l))

• L |≠V isIn(x,l) sse (xL,V,lL,V) isInL sse • …..

• Esercizio 19: completare la verifica della validità della formula.

• Esercizio 20: L |= isIn(y,l) isIn(y,push(x,l))

• Esercizio 21: L |= isIn(x,l) isIn(x,push(x,l))