Alloy

Intestazione (1)

• Al modello descritto è stato dato il nome di azienda_compravendita_materieprime

• come espresso dalla traccia, tale modello è volto a rappresentare le aziende che si occupano di compravendita di materie prime

• in quanto documento Alloy, la specifica si presenta come un’unità in codice sorgente (cfr. source code) e contiene:

- signatures: definiscono tipi e relazioni tra tipi

- predicati: determinano espressioni riutilizzabili poi nei fatti o nelle asserzioni

Intestazione (2)

- fatti: specificano vincoli cui il modello deve sottostare

- asserzioni: rappresentano quelle particolari proprietà

del sistema che è necessario controllare (check)

• il modello è stato sviluppato sotto l’ipotesi principale che un lavoratore mantenga le proprie amicizie nonostante i cambiamenti di ruolo; in particolare, questo si riscontra nelle scelte fatte nella costruzione del metodo di verifica del sistema informativo introdotto nell’azienda

Signature (1)

• Le signatures utilizzate nel modello sono:

- sig Settore{ }: identifica il settore d’appartenenza dei lavoratori dell’azienda

  - sig Direttore{

amici: set Lavoratore

}: rappresenta l’entità direttore all’interno dell’azienda e lo rapporta ad un gruppo di lavoratori tramite la relazione binaria amici

   

Signature (2)

- sig Lavoratore{ settore: Settore,friendBook: set Lavoratore

} : identifica i lavoratori dell’azienda e li caratterizza* con il proprio settore d’appartenenza e la

propria lista d’amici (costituita da un insieme di altri lavoratori)

* le field definitions sappiamo essere parti di una signature dedicate alla definizione di relazioni; poichè sappiamo anche che un atomo in sè è completamente featureless, usiamo delle relazioni per rappresentarne proprietà

Signature (3)

- sig Schedario{

manager: set Lavoratore ,

impiegati: set Lavoratore ,

fattorini: set Lavoratore

} : ha il compito di suddividere i ruoli tra i lavoratori dell’azienda; li classifica come manager, impiegati o fattorini

Predicati (1)

• I predicati espressi per l’azienda sono:- pred essereAmici(x: Lavoratore, y:Lavoratore){

one (x.friendBook & y) }: i lavoratori x e y sono amici quando c’è

un’intersezione (&) tra la lista di amici di x e y, ovvero quando y compare tra gli amici di x

- pred AmiciDir (x: Direttore, y: Lavoratore) {some (x.amici & y)

}: un lavoratore y è amico di un direttore x quando c’è intersezione tra gli amici di x e y, ovvero quando y

compare tra gli amici di x

Predicati (2)

- pred stessoSettore(x: Lavoratore, y: Lavoratore){one (x.settore & y.settore)

}: due lavoratori appartengono allo stesso settore quando hanno lo stesso valore dell’

attributo/relazione settore- pred amiciNelloStessoSettore(x: Lavoratore,

y:Lavoratore){essereAmici(x,y) && stessoSettore(x,y)

}: i lavoratori x e y sono amici e lavorano nello stesso settore quando rispondono al predicato essereAmici e condividono lo stesso settore

Predicati (3)

- pred superiore(x: Lavoratore, y: Lavoratore, z: Schedario){ one (y & z.manager) && one (x & z.fattorini) || one (y & z.manager) && one (x & z.impiegati) || one (y & z.impiegati) && one (x & z.fattorini)}: un lavoratore y è superiore di un lavoratore x

quando, dato lo schedario z, y risulta manager e x fattorino o impiegato oppure quando y risulta impiegato e x fattorino

Predicati (4)

- pred amiciDiUnSuperioreNelloStessoSettore(x: Lavoratore, y: Lavoratore, z: Schedario){

superiore(y,x,z) && amiciNelloStessoSettore (x,y)

}: il lavoratore y è amico di x, che è un suo superiore all’interno dello stesso settore, se x e y rispondono ai predicati superiore e amiciNelloStessoSettore

Predicati (5)

- pred piuRuoli(x: Lavoratore, z: Schedario){

( one (z.manager & x) && one (z.impiegati & x)) ||

( one (z.impiegati & x) && one (z.fattorini & x)) ||

( one(z.fattorini & x) && one (z.manager & x))

}: uno stesso lavoratore ricopre più ruoli quando è contemporaneamente manager e impiegato o

fattorino oppure impiegato e fattorino

Fatti (1)

• I vincoli espressi per il modello sono essenzialmente due

• il primo è relativo alla cardinalità dell’entità Settore e dell’entità Schedario; il secondo racchiude tutte le costrizioni che si è ritenuto opportuno esprimere sul sistema azienda e che riguardano principalmente i lavoratori e il loro cambiamento di ruolo dovuto ad una promozione o eventualmente ad una retrocessione

Fatti (2)

• Il primo fatto è così espresso:fact cardinalità{

#Settore=3#Schedario=1

} • questo vincola il numero di settori dell’azienda a tre, come

espresso dalla traccia, e il numero di schedari a uno• in effetti, il fatto che lo schedario fosse unico è stata una

nostra ipotesi; abbiamo supposto che il sistema azienda tenesse memoria dei propri lavoratori in una sorta di catalogo unico aggiornabile periodicamente

Fatti (3)

• in alternativa, si poteva ipotizzare che l’azienda avesse a disposizione più schedari identici tra loro anzicchè uno solo

• in tal caso, però, sarebbe stato necessario aggiungere il predicato

pred sempreStessoRuoloInDueSchedariDiversi ( x: Lavoratore, z1: Schedario, z2: Schedario) {

(one(z1.manager & x) && one(z2.manager & x)) ||

(one(z1. impiegati & x) && one(z2.impiegati & x)) ||

(one(z1. fattorini & x) && one(z2.fattorini & x)) }

Fatti (4)

e il vincolo:

all l:Lavoratore | all s1: Schedario |s2: Schedario |

sempreStessoRuoloInDueSchedariDiversi(l, s1, s2)

Fatti (5)

• Il secondo fatto, invece, dice: fact{all x: Lavoratore | some y: x.friendBook | x in

y.friendBookno l: Lavoratore | l in l.friendBookno d: Direttore | some l: Lavoratore | AmiciDir (d,l)no l: Lavoratore | one s: Schedario | piuRuoli(l,s)no l: Lavoratore | all al: Lavoratore | one s:

Schedario | amiciDiUnSuperioreNelloStessoSettore(l,al,s)

}

Fatti (6)

• I vincoli che esprime riguardano il fatto che:- per ogni lavoratore, se x è amico di y allora y è amico di x- nessun lavoratore può essere amico di sè stesso- nessun direttore può essere amico di qualche lavoratore- nessun lavoratore può ricoprire più ruoli; - per nessun lavoratore deve valere che sia amico di un suo superiore all’interno dello stesso settore

Asserzioni (1)

• L’assert sviluppata esprime l’aspetto fondamentale su cui si basa il funzionamento del sistema informativo dell’azienda

• infatti, con no l: Lavoratore | all al: Lavoratore |

amiciNelloStessoSettore(l,al) si intende che nessun lavoratore può avere amici (nè dello stesso ruolo nè di ruolo diverso, naturalmente) all’interno del suo stesso settore perchè possa venir promosso; solo in questo modo si può garantire che, sia con un avanzamento di ruolo che con una retrocessione, egli non venga avvantaggiato da un suo amico nè lo avvantaggi

Asserzioni (2)

• In accordo con l’ipotesi iniziale, per cui i rapporti di amicizia restano invariati anche dopo un cambiamento di ruolo, è stato necessario asserire che un lavoratore, per essere promosso, non fosse amico di nessun altro lavoratore nel proprio settore in modo da evitare la situazione in cui un lavoratore con amici dello stesso ruolo nel proprio settore venga promosso, il che sarebbe una prova del fallimento del sistema informativo

• ad es. se un fattorino fosse amico di altri fattorini del proprio settore, al momento della promozione sarebbe un impiegato con amici fattorini, il che è illecito

Varianti del modello (1)

• È possibile risolvere il problema operando in maniera alternativa, cioè osservando la questione da un altro punto di vista

• nelle pagine precedenti abbiamo fornito al sistema le informazioni necessarie per rispondere correttamente alla specifica, compiendo un controllo a monte dell’operazione di assegnamento

• la variante proposta, considera la situazione compiendo il controllo a posteriori; se si ammette la possibilità di relazioni di amicizia tra lavoratori dello stesso ruolo e si asserisce che un assegnamento è valido solo se non vi sono amici dello stesso settore e di ruoli differenti, in realtà si compie lo stesso controllo (nel secondo caso in maniera implicita)

Varianti del modello (2)

• In conclusione, l’amicizia tra lavoratori dello stesso ruolo nello stesso settore o la si blocca tramite l’asserzione o non la si consente a coloro che vengono promossi

• nella prima versione si afferma che l’assegnamento è valido se un lavoratore non ha amici nel proprio settore, il che non porterà mai alla situazione in cui ci siano due amici che non siano nello stesso ruolo

• nella seconda si afferma che un lavoratore può avere amici nel proprio settore nel proprio ruolo, e che l’assegnamento valido si ha solo se esso non crea la situazione in cui ci sia un’amicizia tra due lavoratori nello stesso settore ma in ruoli diversi