SPECIFICA DELLE MAPPE FINITE

Gianna Reggio

reggio@disi.unige.it

Applicazione/esempio grande• Madre di tutti gli esercizi/esempi

– la più usata specifica nelle applicazioni vere

– dare la specifica della struttura dati mappe finite, per semplicità da stringhe di caratteri in naturali

– si richiedono operazioni per rappresentare tutti i dati (caratteri, stringhe, naturali, mappe) costruttori

– operazioni sulle mappe: • mappa vuota (nessuna associazione)

• aggiungere/eliminare/modificare una associazione

• trovare il numero associato ad una stringa

• dominio/codominio di una mappa

• controllare se una mappa è vuota/è iniettiva

Come procedere• scomporre modularmente il compito in

– specificare i naturali– specificare le stringhe di caratteri– specificare la mappe basiche (cioè solo i

costruttori e l’operazione per ritrovare il numero associato ad una stringa)

“operazioni necessarie per costruire i termini per rappresentare tutti i valori di interesse”

– specificare una ad una le ulteriori operazioni e predicati

Linguaggio di specifica• Utilizzeremo un semplicissimo linguaggio di

specifica per presentare le varie specifiche

• Esercizio 24.5: individuare I vari costrutti di tale linguaggio, mano a mano che li utilizzeremo, precisandone sintassi e semantica.

Naturalispec NAT =

Sorts nat

Opns 0:nat

succ: nat -> nat

Axioms

Def(0)

Def(succ(x))

• Consideriamo solo i modelli term-generated di NATspecG NATg = generated { NAT }

• Esercizio 25: aggiungere a NAT le 5 operazioni (somma, sottrazione, moltiplicazione, divisione intera e resto della divisione intera).

• Esercizio 26: aggiungere il predicato ≤.

Aggiunta di <spec NAT1 = extend NAT

Preds _<_: nat x nat

Axioms

x < succ(x)

x < y x < succ(y)

• Esercizio 27: – 0 < succ(x) è valida in NAT1 ?– 0 < succ(x) è valida in generated { NAT1 } ?

Stringhe di caratterispec STRING =

Sorts char, string

Opns: string -- stringa vuota_:_ :char x string -> string

-- aggiunta elemento in testa

’A’,…,’Z’: char -- le 26 lettere-- permettono di rappresentare tutte le stringhe

Axioms-- tutte le operazioni sono totali

Def() Def(c:s)Def(’A’) … Def(’Z’)

Esercizi• Esercizio 28: Si consideri

spec STRING1 = extend STRINGAxiomsc = ‘A’ … ‘Z’ s = ( c:char. s’:string. s = c:s’)

è vero che i modelli di STRING1 e quelli di generated {STRING}

sono gli stessi ?• Soluzione. No, infatti l’algebra DOPPIA definita come segue

charDOPPIA = { A, …., Z }

stringDOPPIA = { *, + }

‘A’DOPPIA = A ... ‘B’DOPPIA = B

DOPPIA = * DOPPIA(c,s) = sè un modello di STRING1 ma non è term-generated.

Verificare per esercizio quanto affermato sopra.

Esercizi• Esercizio 29: Ogni modello di

generated {STRING}

rappresenta ottimamente la struttura dati delle stringhe ?

• Soluzione. No, infatti un’algebra banale (cioè dove ogni carrier contiene esattamente un singolo elemento, e dove le operazioni sono totali e definite nel modo ovvio) è un modello di tale specifica, e non rappresenta per niente le stringhe.

Stringhe di caratteri 2spec STRING2 = extend STRING

Axioms

‘A’≠‘B’ … ‘A’≠‘Z’ … ‘W’≠‘Z’

≠ c:s c1≠c2 s1≠s2 c1:s1 ≠ c2:s2

• Esercizio 30: Ogni modello di generated {STRING2}

rappresenta ottimamente la struttura dati delle stringhe ?

Mappe basiche (1)spec MAP = extend NAT, STRING2Sorts mapOpns []: map -- mappa che non contiene alcuna associazione _[_/_]: map x nat x string -> map-- aggiunta associazione o modifica associazione

__[_]:map x string -> nat-- ritorna il naturale associato ad una stringa-- se esiste

Axioms-- tutte le operazioni sono totali

Def([]) Def(m[n/s])[] ≠ m[n/s](m1 ≠ m2 n1 ≠ n2 s1 ≠ s2) m1[n1/s1] ≠ m2[n2/s2] è accettabile ??? NO!

Mappe basiche (2)• è possibile dare assiomi che richiedano tutte

le possibili identificazioni sugli elementi rappresentati da [] e _[_/_]

• Esercizio 31: Dare tali assiomi.

• oppure è possibile definire prima l’operazione _[_] e poi richiedere che due mappe sono uguali ses associano gli stessi naturali alle stesse stringhe

Mappe basiche (3)-- continuazione degli assiomi di MAP-- definizione di _[_]

Def([][s]) m[n/s][s] = n

s ≠ s’ m[n/s][s’] = m[s’]-- identificazioni sulle mappe

( s:string . m[s] = m’[s]) m = m’

Operazione xxxx sulle mappe