\documentstyle[fuzz, italian, makeidx]{article}

\marginparwidth 0pt
\oddsidemargin -0.2in
\evensidemargin -0.2in
\marginparsep 0pt
\topmargin -0.9in
\textwidth 6.75in
\textheight 9.8in

\makeindex

\begin{document}

\begin{titlepage}
\begin{center}

{\Large Universit\`a di Bologna \\[0.5cm]
 C.d.L. Scienze dell'Informazione}\\[7cm]

{\Large Progetto di TPA - A.A. 1996-97}\\[1cm]
{\Huge Specifica Z} \\[2cm]

{\large Gruppo Zero} \\[0.5cm]

{\large Andrea Ghidini ({\em segretario}) \\
        Marco Guerra \\
        Luca Padovani ({\em portavoce}) \\
        Massimo Zaniboni}

\end{center}
\end{titlepage}

\renewcommand{\contentsname}{Indice}
\tableofcontents
\newpage

\section{Introduzione}

Il sistema da realizzare \`e formato da quattro moduli: il client, il server, 
il broker ed il sito borsistico.

Il sito borsistico \`e un sottosistema capace di fornire su richiesta le quotazione
e il rendimento nominale, nel caso quest'ultimo esista, di un certo insieme di
titoli quotati in borsa.

Il broker \`e un sottosistema capace di vendere e comprare titoli quotati in
borsa. Ogni volta che esegue le operazioni richieste invia un messaggio di
notifica al server.

Il client \`e un sottosistema che fornisce un'interfaccia integrata in un 
Web Browser attraverso la quale l'utente dialoga con il server. 

Il server \`e il sottosistema che riceve ed esegue i comandi del client, gestisce
le informazioni riservate dell'utente e coordina il lavoro degli altri 
sottosistemi.
Esso \`e l'unico sistema specificato formalmente. Dalla sua specifica 
si possono comunque ricavare i requisiti fondamentali degli altri sottosistemi.

Il sistema complessivo \`e pensato come un sistema ``server-centrico''. Il server
\`e associato ad un solo utente di cui gestisce: password, titoli posseduti,
titoli in movimentazione, soldi investiti nel portafoglio e regole automatiche
di compravendita. Inoltre il server gestisce un database storico contenente le
quotazioni e i rendimenti nominali giorno per giorno dei titoli a cui \`e 
interessato l'utente. Di questi titoli il server mantiene anche le quotazioni
``attuali''. Il server \`e descritto come un sistema che riceve messaggi
dall'esterno, li processa e invia gli opportuni messaggi di risposta. Questo
modo di specificare le funzionalit\`a del sever rende pi\`u naturale pensare
al sistema come operante in rete e interrogabile via Web, come richiesto nel
documento di specifica informale.

Per semplicit\`a non sono stati specificati i sistemi di sicurezza necessari
in una applicazione finanziaria reale, a parte uno scambio di password fra client 
e server al momento della connessione.

Nella figura \`e rappresentata schematicamente l'applicazione (server) ed
i componenti con i quali interagisce.

\begin{center}
\input{tpa97.pstex_t}
\end{center}

\subsection{Convenzioni sintattiche}

Per facilitare la lettura del documento sono state adottate le seguenti
convenzioni sintattiche: 
\begin{itemize}
\item Il nome degli schemi, dei messaggi, dei
report predefiniti cominciano con una lettera maiuscola. Inoltre i nomi 
dei messaggi hanno un suffisso ``{\it \_Msg}'' oppure ``{\it \_Rep}'' ({\em Reply}), mentre
i report hanno suffisso ``{\it \_Rpt}\,''.
\item I tipi base e i tipi derivati sono scritti in lettere maiuscole.
\item Il nome delle funzioni, delle variabili globali, delle variabili 
all'interno di schemi cominciano con una lettera minuscola.
\end{itemize}

%%%%%%%%%%%%%%%%
% DATI GLOBALI %
%%%%%%%%%%%%%%%%

\section{Tipi primitivi e dati globali}

VALUE \`e l'insieme dei numeri razionali con al pi\`u {\em k} cifre 
decimali ($k > 0$). VALUE verr\`a usato come tipo generico per tutti i valori
di borsa, quali la quotazione, il rendimento, il cambio, ecc.
\`E stato scelto di codificare VALUE con un intero e 
non con un tipo base in quanto nel documento sono frequenti operazioni di 
confronto e calcolo che coinvolgono valori di tipo VALUE. 

\index{VALUE}
\begin{zed}
        VALUE == \num 
\end{zed}

STRING \`e l'insieme di tutte le stringhe. Una stringa \`e una sequenza 
finita, eventualmente vuota, di caratteri.

\index{STRING}
\begin{zed}
        [STRING]
\end{zed}

BOOLEAN \`e usato per rappresentare valori booleani, pu\`o assumere i valori 
TRUE o FALSE.

\index{BOOLEAN}
\begin{syntax}
        BOOLEAN & ::= & TRUE | FALSE
\end{syntax}

ITEMID \`e l'insieme degli identificatori per {\em strumenti finanziari}. 

\index{ITEMID}
\begin{zed}
        [ITEMID]
\end{zed}

Ogni strumento finanziario appartiene ad un'unica classe.
L'applicazione prevede tre tipi di strumenti diversi: 
azioni (SHARE), titoli di stato (BOND) e valute estere (CURRENCY).

\index{ITEMCLASS}
\begin{syntax}
        ITEMCLASS & ::= & SHARE | BOND | CURRENCY
\end{syntax}

La seguente funzione individua la classe di uno strumento a partire dal suo
identificatore.

\index{is}
\begin{axdef}
        is: ITEMID \surj ITEMCLASS
\end{axdef}

Il {\em valore} di uno strumento finanziario dipende dalla sua classe. In 
particolare, per le azioni \`e significativa la quotazione, per i titoli di 
stato si considerano la quotazione ed il rendimento nominale, per le valute
estere si considera il cambio (inteso comunque come ``quotazione'' della
valuta estera).

\index{ITEMVALUE}
\begin{schema}{ITEMVALUE}
        quotation: VALUE \\
        nomYield: VALUE 
\end{schema}

Si definisce il tipo DATE che costituisce l'insieme di tutte le date. Anche
in questo caso si \`e scelta una codifica con numeri interi in quanto sar\`a
vitale poter operare confronti tra date. 
Si suppone che questa codifica preservi l'ordinamento usuale tra le date.

\begin{zed}
        DATE == \num
\end{zed}

Si definisce la funzione ausiliaria {\it prevDate} che permette di calcolare,
a partire da una data {\it d} e un numero {\it n}, la data corrispondente
a {\it n} giorni prima di {\it d}.

\index{prevDate}
\begin{axdef}
        prevDate: DATE \cross \nat \pfun DATE
\where
        \forall date: DATE; n_1, n_2: \nat @ \\
\t1		prevDate(date, 0) = date \land \\
\t1             prevDate(date, n_1) \leq date \land \\
\t1             n_1 \geq n_2 \implies prevDate(date, n_1) \leq prevDate(date, n_2)
\end{axdef}

``{\it today}'' \`e una variabile globale che contiene la data corrente e
viene aggiornata automaticamente dal sistema.

\index{today}
\begin{axdef}
        today: DATE
\end{axdef}

Il database storico registra giornalmente i valori di un insieme di strumenti
finanziari. Come si \`e visto ogni strumento finanziario \`e caratterizzato 
da diverse quanti\`a, tuttavia ogni database elementare ha la stessa struttura:

\index{DATABASE}
\begin{zed}
        DATABASE == ITEMID \cross DATE \ffun ITEMVALUE
\end{zed}

Un secondo database registra giornalmente il valore del portafoglio e 
l'investi\-mento speso nel portafoglio.

\index{PFDATABASE}
\begin{zed}
        PFDATABASE == DATE \ffun VALUE
\end{zed}

Il portafoglio memorizza la quantit\`a di ogni strumento posseduto,
l'entit\`a complessiva delle vendite pendenti su un certo strumento
ed il numero totale di transazioni pendenti su uno strumento.

\index{PORTFOLIO}
\index{PENDINGOP}
\index{TRANSACTIONS}
\begin{zed}
        PORTFOLIO == ITEMID \ffun \nat
\also
        PENDINGOP == ITEMID \ffun \nat
\also
	TRANSACTIONS == ITEMID \ffun \nat
\end{zed}

%%%%%%%%%%%%%%%%%
% COMUNICAZIONE %
%%%%%%%%%%%%%%%%%
  
\section{Comunicazione}

ADDRESS \`e l'insieme di tutti gli indirizzi di rete. Un indirizzo di rete
identifica univocamente un host ed un processo all'interno dell'host di tutta
la rete.

\index{ADDRESS}
\begin{zed}
        [ADDRESS]
\end{zed}

CONTENT \`e rappresenta un tipo generico per il contenuto dei messaggi.

\index{CONTENT}
\begin{zed}
        [CONTENT]
\end{zed}

A volte un messaggio ha un contenuto vuoto.

\begin{axdef}
        nullContent: CONTENT
\end{axdef}

Ogni messaggio gestito o generato dall'applicazione ha un tipo (MSGTYPE) che
ne specifica l'utilizzo e in particolare il tipo di contenuto. 

\index{MSGTYPE}
\begin{syntax}
        MSGTYPE & ::= & UpdateDataBase\_Msg | ViewReport\_Msg \\
                & | & OpenConnection\_Msg | OpenConnection\_Rep \\
                & | & CloseConnection\_Msg | CloseConnection\_Rep \\
                & | & Broker\_Rep | ManualTrading\_Msg | AutoTrading\_Msg \\
                & | & Trading\_Msg | PortfolioValueDateX\_Msg \\
                & | & PortfolioValueDateX\_Rep | ViewString\_Msg \\
                & | & ViewXAscendentQuotationOrder\_Msg \\
                & | & ViewRules\_Msg | ViewRules\_Rep | AddRule\_Msg \\
                & | & DeleteRule\_Msg | SetRuleOn\_Msg | SetRuleOff\_Msg \\
                & | & ViewXIncQuotationOrder\_Msg \\
                & | & ViewXDecQuotationOrder\_Msg \\
                & | & ViewXIncYieldOrder\_Msg | ViewXDecYieldOrder\_Msg \\
                & | & ViewSortedItems\_Msg | ViewPortfolioGraph\_Msg \\
                & | & ViewPortfolioGraph\_Rep | ViewDataBaseGraph\_Msg \\
                & | & UpdateDataBase\_Rep | ViewAllItems\_Msg \\
                & | & GetAllItems\_Msg | GetAllItems\_Rep  \\
		& | & ViewAllItems\_Rep | DeleteItem\_Msg | AddItem\_Msg \\
		& | & ViewDataBaseGraph\_Rep
\end{syntax}

Un messaggio \`e formato, nell'ordine, dagli indirizzi del mittente e del
destinatario, dal tipo di messaggio e dal suo contenuto.

\index{MESSAGE}
\begin{zed}
        MESSAGE == ADDRESS \cross ADDRESS \cross MSGTYPE \cross CONTENT
\end{zed}

Si definiscono alcune funzioni ausiliarie per la gestione dei messaggi. Sono
usate per estrarre i vari campi di un messaggio.

\index{getSender}
\index{getReceiver}
\index{getType}
\index{getContent}
\begin{axdef}
        getSender: MESSAGE \fun ADDRESS \\
        getReceiver: MESSAGE \fun ADDRESS \\
        getType: MESSAGE \fun MSGTYPE \\
        getContent: MESSAGE \fun CONTENT
\where
        \forall m: MESSAGE; s, d: ADDRESS; t: MSGTYPE; c: CONTENT | m = (s, d, t, c) @ \\
\t1             getSender(m) = s \land \\
\t1             getReceiver(m) = d \land \\
\t1             getType(m) = t \land \\
\t1             getContent(m) = c 
\end{axdef}

``{\it whoAmI}\,'' \`e una variabile globale che rappresenta l'indirizzo del 
programma in esecuzione. 

\index{whoAmI}
\begin{axdef}
        whoAmI: ADDRESS
\end{axdef}

Per la comunicazione client-server con il sito di borsa e con il broker 
si interpone uno schema ``{\it Net}\,'' dove si suppone non esistano messaggi
corrotti. Si suppone inoltre che la comunicazione dei messaggi avvenga 
tramite canali FIFO tra coppie di processi.

\index{Net}
\begin{schema}{Net}
        msg: \bag MESSAGE
\end{schema}

Le primitive SendTo e Receive sono usate per la comunicazione punto-a-punto.

\index{SendTo}
\begin{schema}{SendTo}
        \Delta Net \\
        addr?: ADDRESS \\
        type?: MSGTYPE \\
        c?: CONTENT 
\where
        \exists m: MESSAGE | m = (whoAmI, addr?, type?, c?) @ msg' = msg \uplus \lbag m \rbag
\end{schema}

\index{Receive}
\begin{schema}{Receive}
        \Delta Net \\
        sender!: ADDRESS \\
        type!: MSGTYPE \\
        c!: CONTENT
\where
        \exists m: MESSAGE | m \inbag msg \land getReceiver(m) = whoAmI @ \\
\t1             sender! = getSender(m) \land \\
\t1             type! = getType(m) \land \\
\t1             c! = getContent(m) \land \\
\t1             msg' = msg \bagdiff \lbag m \rbag
\end{schema}

\index{NoMessage}
\begin{schema}{NoMessage}
        \Xi Net\\
\where
        \forall m: MESSAGE | m \inbag msg @ getReceiver(m) \neq whoAmI
\end{schema}

%%%%%%%%%%
% SERVER %
%%%%%%%%%%

\section{Applicazione Server}

Il server mantiene le informazioni relative ai database, al portafoglio 
dell'utente, allo stato della connessione con l'utente e ai diritti di
accesso dell' utente. 
Questa versione dell'applicazione consente di lavorare
con un singolo utente che \`e l'unico abilitato a richiedere la connessione
con il server. 

\subsection{Il database storico}

Il database storico \`e concettualmente diviso in tre database, ognuno
predisposto a contentere i dati di borsa di una particolare classe di
strumenti finanziari. Nell'ordine si definiscono i database per le azioni,
i titoli di stato e le valute estere.

\index{ShareDataBase}
\begin{schema}{ShareDataBase}
        shareDataBase: DATABASE
\where
        \forall id: ITEMID; date: DATE; v: ITEMVALUE | \\
\t1             v = shareDataBase(id, date) @ is(id) = SHARE \land 
			date \leq today \land v.nomYield = 0
\end{schema}

\index{BondDataBase}
\begin{schema}{BondDataBase}
        bondDataBase: DATABASE 
\where
        \forall id: ITEMID; date: DATE; v: ITEMVALUE | \\
\t1             v = bondDataBase(id, date) @ 
			is(id) = BOND \land date \leq today
\end{schema}

\index{CurrencyDataBase}
\begin{schema}{CurrencyDataBase}
        currencyDataBase: DATABASE
\where
        \forall id: ITEMID; date: DATE; v: ITEMVALUE | \\
\t1             v = currencyDataBase(id, date) @ 
			is(id) = CURRENCY \land date \leq today \land 
			v.nomYield = 0
\end{schema}

Il database storico nella sua globalit\`a \`e rappresentato dal seguente 
schema, che definisce inoltre un campo ``{\it dataBase}'' attraverso 
il quale sono acceduti i dati di borsa di tutte le categorie di 
strumenti.

\index{DataBase}
\begin{schema}{DataBase}
        ShareDataBase \\
        BondDataBase \\
        CurrencyDataBase \\
        dataBase: DATABASE
\where
        dataBase = shareDataBase \cup bondDataBase \cup currencyDataBase
\end{schema}

Il database storico \`e vuoto al primo avvio dell'applicazione. Il seguente 
schema di inizializzazione \`e relativo al momento in cui l'applicazione
viene installata. \`E ragionevole pensare che, nel momento in cui 
l'applicazione viene riavviata per qualche motivo, il database storico 
ritorni nella condizione dell'ultimo aggiornamento.

\index{InitDataBase}
\begin{schema}{InitDataBase}
        DataBase'
\where      
        \dom dataBase' = \empty
\end{schema}

Il database storico viene aggiornato periodicamente attraverso il seguente
schema:

\index{UpdateDataBaseOk}
\begin{schema}{UpdateDataBaseOk}
        \Delta DataBase \\
        update?: DATABASE 
\where
        dataBase' = dataBase \oplus update?
\end{schema}

Definiamo le seguenti funzioni ausiliarie:

``{\it dataExact}\,'' determina se nel database sono presenti i dati di borsa
relativi a un certo strumento finanziario in una data specificata.

\index{dataExact}
\begin{axdef}
        dataExact: DATABASE \cross ITEMID \cross DATE \fun BOOLEAN
\where
        \forall db: DATABASE; id: ITEMID; date: DATE @ \\
\t1             dataExact(db, id, date) = \zif (id, date) \in \dom db \zthen TRUE \zelse FALSE
\end{axdef}

``{\it dataDay}'' determina se sono presenti i dati di borsa relativi a un 
certo strumento finanziario in una data specificata o una data antecedente.

\index{dataDay}
\begin{axdef}
        dataDay: DATABASE \cross ITEMID \cross DATE \fun BOOLEAN
\where
        \forall db: DATABASE; id: ITEMID; date: DATE @ 
		dataDay(db, id, date) = \\
\t2                     \zif \exists date_1: DATE | date_1 \leq date @ 
				(id, date_1) \in \dom db \zthen TRUE \zelse FALSE 
\end{axdef}

\index{getValue}
``{\it getValue}'' restituisce i dati di borsa pi\`u aggiornati, fino a una 
certa data, di uno strumento finanziario.

\begin{axdef}
        getValue: DATABASE \cross ITEMID \cross DATE \pfun ITEMVALUE
\where
        \forall db: DATABASE; id: ITEMID; date: DATE | 
                dataDay(db, id, date) = TRUE @ \\
\t2			getValue(db, id, date) = db(id, max \{ date_1: DATE | 
				date_1 \leq date \land (id, date_1) \in \dom db \}) 
\end{axdef}

``{\it getQuotation}'' restituisce la quotazione pi\`u aggiornata di uno 
strumento finanziario.

\index{getQuotation}
\begin{axdef}
        getQuotation: DATABASE \cross ITEMID \cross DATE \pfun VALUE
\where
        \forall db: DATABASE; id: ITEMID; date: DATE; v: ITEMVALUE | \\
\t1		v = getValue(db, id, date) @ getQuotation(db, id, date) = v.quotation
\end{axdef}

``{\it getNominalYield}\,'' restituisce il rendimento nominale pi\`u 
aggironato di un titolo di stato.

\index{getNominalYield}
\begin{axdef}
        getNominalYield: DATABASE \cross ITEMID \cross DATE \pfun VALUE
\where
        \forall db: DATABASE; id: ITEMID; date: DATE; v: ITEMVALUE | \\
\t1		v = getValue(db, id, date) \land is(id) = BOND @ 
                        getNominalYield(db, id, date) = v.nomYield
\end{axdef}

``{\it getYield}\,'' calcola il rendimento di uno strumento finanziario dalla
data specificata fino a oggi. Il calcolo del rendimento avviene
attraverso la seguente formula:

\begin{displaymath}
        yield(id, date) = ( \frac{quotation(id, today)}{quotation(id, date)}
                - 1 ) * 100
\end{displaymath}

Da notare che Z, non ammettendo il tipo reale, consente di operare solo
la divisione intera.

\index{getYield}
\begin{axdef}
        getYield: DATABASE \cross ITEMID \cross DATE \pfun VALUE
\where
        \forall db: DATABASE; id: ITEMID; date: DATE | \\
\t1             dataExact(db, id, today) = TRUE \land 
                dataDay(db, id, date) = TRUE @ \\
\t2             getYield(db, id, date) = \\
\t3			((getQuotation(db, id, today) * 100) \div 
			getQuotation(db, id, date) - 100)
\end{axdef}

\subsection{Il portafoglio}

Il portafoglio registra i titoli posseduti o tenuti sotto osservazione 
dall'utente. Inoltre, per ogni strumento, esiste una quantit\`a che 
indica l'entit\`a totale di transazioni di vendita per un certo
strumento.
Il monitor contiene quei titoli non posseduti e sui quali 
non \`e in corso alcuna transazione.

\index{Portfolio}
\begin{schema}{Portfolio}
        portfolio: PORTFOLIO \\
        pending: PENDINGOP \\
	transaction: TRANSACTIONS \\
        monitor: \power ITEMID
\where
        \dom pending = \dom portfolio
\also
	\dom transaction = \dom portfolio
\also
        monitor = \{ id: ITEMID | id \in \dom portfolio \land 
                portfolio(id) = 0 \land transaction(id) = 0 \}
\end{schema}

Per l'inizializzazione di questo database si pu\`o fare un discorso analogo
a quello per il database storico.

\index{InitPortfolio}
\begin{schema}{InitPortfolio}
        Portfolio'
\where
        \dom portfolio' = \empty
\end{schema}

Le operazioni di compravendita (transactions) hanno effetti sia sul 
portafoglio che sul database investimento/valore. 
La compravendita effettuata tramite un broker \`e gestita
attraverso un protocollo particolare che garantisce la consistenza del
portafoglio in situazioni critiche. 

\index{TransactionOn}
\begin{schema}{TransactionOn}
        \Delta Portfolio \\
        id?: ITEMID \\
        reqN?: \num
\where
        id? \in \dom portfolio
\also
        pending' = \zif reqN? < 0 \zthen pending \oplus 
			\{ id? \mapsto pending(id?) - reqN? \} \zelse pending
\also
	transaction' = transaction \oplus \{ id? \mapsto transaction(id?) + 1 \}
\also
        portfolio' = portfolio
\end{schema}

\index{TransactionOff}
\begin{schema}{TransactionOff}
        \Delta Portfolio \\
        id?: ITEMID \\
        reqN?: \num
\where
        pending' = \zif reqN? < 0 \zthen pending \oplus 
			\{ id? \mapsto pending(id?) + reqN? \} \zelse pending
\also
	transaction' = transaction \oplus \{ id? \mapsto transaction(id?) - 1 \}
\also
        portfolio' = portfolio
\end{schema}

\index{CreatePortfolioEntry}
\begin{schema}{CreatePortfolioEntry}
        \Delta Portfolio \\
        id?: ITEMID \\
        effN?: \num
\where
        id? \notin \dom portfolio
\also
        portfolio' = portfolio \oplus \{ id? \mapsto effN? \}
\also
	transaction' = transaction \oplus \{ id? \mapsto 0 \}
\also
        pending' = pending \oplus \{ id? \mapsto 0 \}
\end{schema}

\index{UpdatePortfolioEntry}
\begin{schema}{UpdatePortfolioEntry}
        \Delta Portfolio \\
        id?: ITEMID \\
        effN?: \num
\where
        id? \in \dom portfolio
\also
        portfolio' = portfolio \oplus \{ id? \mapsto portfolio(id?) + effN? \}
\also
        pending' = pending
\also
	transaction' = transaction
\end{schema}

\begin{zed}
	UpdatePortfolio \defs CreatePortfolioEntry \lor UpdatePortfolioEntry
\end{zed}

\subsection{Il database investimento/valore}

Il seguente database registra giornalmente il valore del portafoglio utente 
e l'investimento quando quest'ultimo cambia.

\index{PfDataBase}
\begin{schema}{PfDataBase}
        pfValueDB: PFDATABASE \\
        pfInvestmentDB: PFDATABASE
\where
        \forall date: DATE | date \in \dom pfValueDB \lor 
		date \in \dom pfInvestmentDB @ date \leq today
\end{schema}

Per l'inizializzazione di questo database si pu\`o fare un discorso analogo
a quello per il database storico.

\index{InitPfDataBase}
\begin{schema}{InitPfDataBase}
        PfDataBase'
\where
        \dom pfValueDB' = \empty
\also
	\dom pfInvestmentDB' = \empty
\end{schema}

Nel momento in cui sono disponibili dati di borsa aggiornati il valore
del portafoglio deve essere ricalcolato ed il database investimento/valore
aggiornato di conseguenza.
Nell'impossibilit\`a di specificare in modo semplice il calcolo del valore 
del portafoglio ci limitiamo alla seguente definizione assiomatica:

\index{calcValue}
\begin{axdef}
        calcValue: PORTFOLIO \cross DATABASE \pfun VALUE
\end{axdef}

Intuitivamente il valore del portafoglio \`e calcolato attraverso la seguente
formula:

\begin{displaymath}
\displaystyle
        calcValue(portfolio) = \sum_{id \in \dom portfolio} portfolio(id) * 
                quotation(id, today)
\end{displaymath}

In conclusione, l'aggiornamento del database investimento/valore avviene 
attraverso il seguente schema:

\index{UpdatePfDataBaseOk}
\begin{schema}{UpdatePfDataBaseOk}
        \Xi DataBase \\
        \Xi Portfolio \\
        \Delta PfDataBase
\where
        \forall id: ITEMID | id \in \dom portfolio \land portfolio(id) > 0 @ 
                dataDay(dataBase, id, today) = TRUE
\also
        pfValueDB' = pfValueDB \oplus \{ today \mapsto calcValue(portfolio, dataBase) \}
\also
        pfInvestmentDB' = pfInvestmentDB
\end{schema}

Non sempre \`e possibile calcolare il valore del portafoglio, ad esempio a
causa di alcuni strumenti non quotati.

\index{DataNotPresent}
\begin{schema}{DataNotPresent}
        \Xi DataBase \\
        \Xi Portfolio
\where
        \exists id: ITEMID | id \in \dom portfolio \land portfolio(id) > 0 @ 
                dataDay(dataBase, id, today) = FALSE
\end{schema}

\index{UpdatePfDataBase}
\begin{zed}
	UpdatePfDataBase \defs UpdatePfDataBaseOk \lor DataNotPresent
\end{zed}

Nel momento in cui arriva dal broker la notifica di un'operazione bisogna
``aggiustare'' (back-patch) retroattivamente il database investmento/valore. 
L'operazione di back-patch viene eseguita utilizzando i dati di borsa, 
se disponibili, oppure la quotazione dello strumento interessato 
ritornata dal broker stesso.

\index{BackPatchPfDataBaseValue}
\begin{schema}{BackPatchPfDataBaseValue}
	\Xi DataBase \\
        \Delta PfDataBase \\
        id?: ITEMID \\
        effN?: \num \\
        date?: DATE \\
        v?: ITEMVALUE
\where
	\dom pfValueDB = \dom pfValueDB'
\also
        \forall d: DATE | d \geq date? \land d \in \dom pfValueDB @ pfValueDB'(d) = \\
\t1		\zif dataDay(dataBase, id?, date?) = TRUE \zthen \\
\t2                     pfValueDB(d) + effN? * getQuotation(dataBase, id?, d) \\
\t1             \zelse pfValueDB(d) + effN? * v?.quotation
\also
        \forall d: DATE | d < date? \land d \in \dom pfValueDB @ 
                pfValueDB'(d) = pfValueDB(d)
\also
        pfInvestmentDB' = pfInvestmentDB
\end{schema}

\index{BackPatchPfDataBaseInvestment}
\begin{schema}{BackPatchPfDataBaseInvestment}
        \Delta PfDataBase \\
        effN?: \num \\
        date?: DATE \\
        v?: ITEMVALUE
\where
	date? \in \dom pfInvestmentDB
\also
	\dom pfInvestmentDB' = \dom pfInvestmentDB
\also
        \forall d: DATE | d \geq date? \land d \in \dom pfInvestmentDB @ \\
\t1             pfInvestmentDB'(d) = pfInvestmentDB(d) + effN? * v?.quotation
\also
        \forall d: DATE | d < date? \land d \in \dom pfInvestmentDB @ 
		pfInvestmentDB'(d) = pfInvestmentDB(d)
\also
        pfValueDB' = pfValueDB
\end{schema}

La funzione seguente reperisce dal database investimento il valore
pi\`u aggiornato fino a una certa data:

\index{getLastValue}
\begin{axdef}
        getLastValue: PFDATABASE \cross DATE \fun VALUE
\where
        \forall f: PFDATABASE; d: DATE @ \\
\t1             \zlet prev == \{ d_1: DATE | d_1 \leq d \land d_1 \in \dom f \} @ \\
\t2                     getLastValue(f, d) = 
				\zif prev \neq \empty \zthen f(max~prev) \zelse 0
\end{axdef}

\index{AddPfDataBaseInvestment}
\begin{schema}{AddPfDataBaseInvestment}
	\Delta PfDataBase \\
	effN?: \num \\
	date?: DATE \\
	v?: ITEMVALUE
\where
	date? \notin \dom pfInvestmentDB
\also
	pfInvestmentDB' = pfInvestmentDB \oplus \\
\t1		\{ date? \mapsto getLastValue(pfInvestmentDB, date?) + 
			effN? * v?.quotation \}
\end{schema}

\index{BackPatchPfdataBase}
\begin{zed}
        BackPatchPfDataBase \defs BackPatchPfDataBaseValue \land \\
\t1		(BackPatchPfDataBaseInvestment \lor AddPfDataBaseInvestment)
\end{zed}

\subsection{I dati utente ed il server}

I dati di un utente comprendono il portafoglio, il database 
investimento/valore, lo stato della connessione con il server, il suo 
login e la password, il suo indirizzo di rete.

\index{User}
\begin{schema}{User}
        Portfolio \\
        PfDataBase \\
        userConnected: BOOLEAN \\
        userLogin, userPassword: STRING \\      
        userAddress: ADDRESS
\end{schema}

La maggior parte dei messaggi inviati dal server sono destinati all'utente.
Si definiscono due schemi ausiliari che espandono quelli relativi alla
comunicazione in rete e semplificano la specifica.

\index{ToUser}
\begin{schema}{ToUser}
        \Xi User \\
        addr!: ADDRESS 
\where
        addr! = userAddress
\end{schema}

\index{Send}
\begin{zed}
        Send \defs ToUser \pipe SendTo
\end{zed}

Infine il server mantiene le informazioni dell'utente e del database storico,
nonch\'e l'indirizzo del sito di borsa ({\em stock exchange}) di riferimento.

\index{Server}
\begin{schema}{Server}
        DataBase \\
        User \\
        stockExchangeAddr: ADDRESS 
\end{schema}

Quando il server viene inizializzato registra login e password dell'utente
abilitato a dialogare con lui e l'indirizzo del sito di borsa.

\index{InitServer}
\begin{schema}{InitServer}
        Server' \\
        registeredUserLogin?, registeredUserPassword?: STRING \\
        registeredStockExchangeAddr?: ADDRESS 
\where
        userConnected' = FALSE
\also
        userLogin' = registeredUserLogin?
\also
        userPassword' = registeredUserPassword?
\also
        stockExchangeAddr' = registeredStockExchangeAddr?
\end{schema}

%%%%%%%%%%%%%%%%%%
% TIPI DI ERRORE %
%%%%%%%%%%%%%%%%%%

\subsection{Tipi di errore}

I messaggi di errore sono memorizzati sotto forma di report.

\index{REPORT}
\begin{syntax}
        REPORT & ::= & Ok\_Rpt | UserConnected\_Rpt \\
                & | & AccessDenied\_Rpt | NotConnected\_Rpt \\
                & | & BrokerReply\_Rpt | IllegalOperation\_Rpt \\
                & | & WrongDate\_Rpt | RulePresent\_Rpt \\
                & | & RuleNotPresent\_Rpt | WrongItems\_Rpt \\
                & | & WrongRange\_Rpt | DataBaseUpdated\_Rpt \\
                & | & ItemBusy\_Rpt | ItemNotPresent\_Rpt \\
		& | & ItemPresent\_Rpt
\end{syntax}

\begin{axdef}
        packReport: REPORT \inj CONTENT
\end{axdef}

Ulteriori funzioni di conversione pi\`u specifiche, come ``{\it packRules}'', 
saranno introdotte al momento opportuno.

Molti schemi indicano il completamento di un'operazione con successo
semplicemente attraverso un messaggio di ``Ok'', inviato dal seguente 
schema.

\index{Success}
\begin{schema}{Success}
        sender?: ADDRESS \\
        addr!: ADDRESS; type!: MSGTYPE; c!: CONTENT
\where
        addr! = sender?
\also
        type! = ViewReport\_Msg
\also
        c! = packReport(Ok\_Rpt)
\end{schema}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% COLLEGAMENTO CON IL CLIENT %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Collegamento con il Client}

Prima di poter operare sul portafoglio l'utente deve collegarsi al server,
ad esempio tramite un browser Web.

Nel messaggio di connessione si suppone siano presenti login e password 
dell'utente che richiede la connessione.

\begin{axdef}
        extractUserLogin: CONTENT \fun STRING
\also
        extractUserPassword: CONTENT \fun STRING
\end{axdef}

\index{OpenConnectionRequest}
\begin{schema}{OpenConnectionRequest}
        type?: MSGTYPE; c?: CONTENT \\
        userLogin!, userPassword!: STRING
\where
        type? = OpenConnection\_Msg
\also
        userLogin! = extractUserLogin(c?)
\also
        userPassword! = extractUserPassword(c?)
\end{schema}

Se la connessione ha successo l'indirizzo del client viene registrato nello
stato ``{\it User}''. 

\index{OpenConnectionOk}
\begin{schema}{OpenConnectionOk}
        \Delta User \\
        sender?: ADDRESS \\
        userLogin?, userPassword?: STRING
\where
        userConnected = FALSE
\also
        userLogin? = userLogin 
\also
        userPassword? = userPassword
\also
        userConnected' = TRUE
\also
        userAddress' = sender?
\end{schema}

\index{OpenConnectionReply}
\begin{schema}{OpenConnectionReply}
        \Xi User \\
        addr!: ADDRESS; type!: MSGTYPE; c!: CONTENT
\where
        addr! = userAddress
\also
        type! = OpenConnection\_Rep
\also
        c! = nullContent
\end{schema}

Un utente gi\`a connesso non pu\`o chiedere l'apertura di un'altra connessione.

\index{UserConnected}
\begin{schema}{UserConnected}
        \Xi User \\
        userLogin?, userPassword? : STRING
\where
        userConnected = TRUE
\also
        userLogin? = userLogin
\also
        userPassword? = userPassword
\end{schema}

\index{userConnectedReply}
\begin{schema}{UserConnectedReply}
        sender?: ADDRESS \\
        addr!: ADDRESS; type!: MSGTYPE; c!: CONTENT
\where
        addr! = sender?
\also
        type! = ViewReport\_Msg
\also
        c! = packReport(UserConnected\_Rpt)
\end{schema}

Infine il seguente schema controlla che l'utente che chiede la connessione sia
quello effettivamente abilitato ad usare l'applicazione:

\index{AccessDenied}
\begin{schema}{AccessDenied}
        \Xi User \\
        userLogin?, userPassword?: STRING
\where
        userLogin? \neq userLogin \lor userPassword? \neq userPassword
\end{schema}

\index{AccessDeniedReply}
\begin{schema}{AccessDeniedReply}
        sender?: ADDRESS \\
        addr!: ADDRESS; type!: MSGTYPE; c!: CONTENT
\where
        addr! = sender?
\also
        type! = ViewReport\_Msg
\also
        c! = packReport(AccessDenied\_Rpt)
\end{schema} 

Dualmente l'utente chiede la chiusura della connessione attraverso gli 
schemi seguenti.

\index{CloseConnectionRequest}
\begin{schema}{CloseConnectionRequest}
        type?: MSGTYPE
\where
        type? = CloseConnection\_Msg
\end{schema}

\index{CloseConnectionOk}
\begin{schema}{CloseConnectionOk}
        \Delta User \\
\where
        userConnected = TRUE
\also
        userConnected' = FALSE
\end{schema}

\index{CloseConnectionReply}
\begin{schema}{CloseConnectionReply}
        sender?: ADDRESS \\
        addr!: ADDRESS; type!: MSGTYPE; c!: CONTENT
\where
        addr! = sender?
\also
        type! = CloseConnection\_Rep
\also
        c! = nullContent
\end{schema}

\index{NotConnected}
\begin{schema}{NotConnected}
        \Xi User \\
\where
        userConnected = FALSE
\end{schema}

\index{NotConnectedReply}
\begin{schema}{NotConnectedReply}
        sender?: ADDRESS \\
        addr!: ADDRESS; type!: MSGTYPE; c!: CONTENT
\where
        addr! = sender?
\also
        type! = ViewReport\_Msg
\also
        c! = packReport(NotConnected\_Rpt)
\end{schema}

Riassumendo, gli schemi di gestione della connessione risultano:

\index{OpenConnection}
\index{CloseConnection}
\begin{zed}
        OpenConnection \defs OpenConnectionRequest \pipe \\ 
\t1             ((OpenConnectionOk \land OpenConnectionReply) \lor \\
\t1             (UserConnected \land UserConnectedReply) \lor \\
\t1             (AccessDenied \land AccessDeniedReply)) \pipe SendTo
\also
        CloseConnection \defs CloseConnectionRequest \pipe \\
\t1             ((CloseConnectionOk \land CloseConnectionReply) \lor \\
\t1             (NotConnected \land NotConnectedReply) \lor \\
\t1             (AccessDenied \land AccessDeniedReply)) \pipe SendTo
\end{zed}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% COMUNICAZIONE CON IL BROKER %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Comunicazione con il broker}

Il broker notifica ogni operazione al server inviando un messaggio per
ogni transazione. Questo messaggio di notifica contiene le seguenti
informazioni: identificatore dello strumento coinvolto nella transazione,
data in cui la transazione \`e effettivamente avvenuta, entit\`a richiesta
della transazione (positiva in caso di acquisto, negativa in caso di vendita),
entit\`a effettiva della transazione (che pu\`o differire dall'entit\`a 
richiesta), valore dello strumento al momento della transazione.

Le funzioni seguenti sono usate per estrarre dai messaggi di notifica e 
di richiesta di transazione i campi suddetti:

\begin{axdef}
        extractItemId: CONTENT \fun ITEMID
\also
        extractDate: CONTENT \fun DATE
\also
        extractReqN: CONTENT \fun \num
\also
        extractEffN: CONTENT \fun \num
\also
        extractItemValue: CONTENT \fun ITEMVALUE
\also
        extractN: CONTENT \fun \num
\end{axdef}

\subsubsection{Notifica di una transazione}

Il broker notifica una transazione attraverso i seguenti schemi:

\index{BrokerNotificationRequest}
\begin{schema}{BrokerNotificationRequest}
        type?: MSGTYPE; c?: CONTENT \\
        id!: ITEMID \\
        date!: DATE \\
        effN!, reqN!: \num \\
        v!: ITEMVALUE \\
\where
        type? = Broker\_Rep
\also
        id! = extractItemId(c?)
\also
        date! = extractDate(c?) 
\also
        reqN! = extractReqN(c?) 
\also
        effN! = extractEffN(c?) 
\also
        v! = extractItemValue(c?)       
\end{schema}

Se l'utente \`e collegato nel momento in cui arriva una notifica, viene
avvisato:

\index{BrokerNotificationOkReply}
\begin{schema}{BrokerNotificationOkReply}
        \Xi User \\
        type!: MSGTYPE; c!: CONTENT \\
        m!: MESSAGE
\where
        userConnected = TRUE
\also   
        type! = ViewReport\_Msg
\also
        c! = packReport(BrokerReply\_Rpt)
\end{schema}

\index{BrokerNotification}
\begin{zed}
        BrokerNotification \defs BrokerNotificationRequest \pipe \\
\t1             ((TransactionOff \land UpdatePortfolio \land BackPatchPfDataBase) \land \\
\t1             ((BrokerNotificationOkReply \pipe Send) \lor NotConnected))
\end{zed}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% COMUNICAZIONE CON IL SITO BORSISTICO %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Comunicazione con il sito borsistico}

Periodicamente l'applicazione richiede i dati di borsa dal sito borsistico
(si veda a proposito lo schema ``{\it TimeOut}\,''). Il sito di borsa risponde
con un messaggio che contiene i dati di borsa degli strumenti richiesti.
\`E anche possibile che il sito non sia in grado di fornire alcuni dati di
borsa ed in effetti il database storico pu\`o contenere dei ``buchi'' relativi
ad esempio a strumenti sospesi in borsa per certi periodi.
Quando arriva un messaggio di aggiornamento dei dati di borsa prima di tutto
si aggiorna il database storico, successivamente viene aggiornato il
database investimento/valore.

\begin{axdef}
        extractDataBase: CONTENT \fun DATABASE
\end{axdef}

\index{UpdateDataBaseRequest}
\begin{schema}{UpdateDataBaseRequest}
        type?: MSGTYPE; c?: CONTENT \\
        update!: DATABASE
\where
        type? = UpdateDataBase\_Rep
\also
        update! = extractDataBase(c?)
\end{schema}

\index{UpdateDataBaseReply}
\begin{schema}{UpdateDataBaseReply}
	\Xi User \\
        type!: MSGTYPE; c!: CONTENT 
\where
	userConnected = TRUE
\also
        type! = ViewReport\_Msg
\also
        c! = packReport(DataBaseUpdated\_Rpt)
\end{schema}

\index{UpdateDataBase}
\begin{zed}
        UpdateDataBase \defs UpdateDataBaseRequest \pipe \\
\t1		(UpdateDataBaseOk \land UpdatePfDataBase) \land 
                ((UpdateDataBaseReply \pipe Send) \lor NotConnected)
\end{zed}

%%%%%%%%%%%
% COMANDI %
%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% COMANDI DI COMPRAVENDITA %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Comandi di compravendita}

L'utente pu\`o eseguire direttamente operazioni di compravendita in due
modi. Il primo, detto modo ``manuale'', consente all'utente di variare 
a piacimento la composizione del portafoglio fornendo all'applicazione
i dati delle transazioni effettuate attraverso modalit\`a esterne 
all'applicazione stessa.
Queste operazioni possono anche essere usate nel momento in cui l'applicazione
\`e installata per portare il portafoglio al suo stato reale.

Un secondo modo, detto modo ``automatico'', prevede che le transazioni siano
effettuate attraverso un broker. L'utente si limita a specificare lo strumento
interessato e l'entit\`a della transazione, dopodich\'e la richiesta viene
inoltrata al broker e l'applicazione provvede ad aggiornare automaticamente
il portafoglio attraverso i messaggi di notifica.

\subsubsection{Compravendita manuale}

\index{ManualTradingRequest}
\begin{schema}{ManualTradingRequest}
        type?: MSGTYPE; c?: CONTENT \\
        id!: ITEMID \\
        date!: DATE \\
        effN!, reqN!: \num \\
        v!: ITEMVALUE
\where
        type? = ManualTrading\_Msg
\also
        id! = extractItemId(c?)
\also
        date! = extractDate(c?)
\also
        effN! = extractN(c?)
\also
	reqN! = effN!
\also
        v! = extractItemValue(c?)       
\end{schema}

Il seguente schema determina la legalit\`a di un'operazione di compravendita
nel caso pi\`u generale in cui l'utente \`e abilitato ad acquistare 
strumenti che ancora non possiede. 

\index{LegalOperation}
\begin{schema}{LegalOperation}
        \Xi Portfolio \\
        id?: ITEMID \\
        reqN?: \num \\
        v?: ITEMVALUE \\
\where
        reqN? \neq 0
\also
        id? \notin \dom portfolio \implies reqN? \geq 0
\also
	id? \in \dom portfolio \implies 
		portfolio(id?) - pending(id?) + reqN? \geq 0
\end{schema}

Un operazione \`e definita illegale se l'entit\`a della transazione \`e nulla,
se \`e una vendita di uno strumento non posseduto o comunque una vendita 
superiore alla quantit\`a posseduta.

\index{IllegalOperation}
\begin{schema}{IllegalOperation}
        \Xi Portfolio \\
        id?: ITEMID \\
        reqN?: \num 
\where
        reqN? = 0 \lor \\
\t1     (reqN? < 0 \land id? \notin \dom portfolio) \lor \\
\t1     (reqN? < 0 \land id? \in \dom portfolio \land 
		portfolio(id?) - pending(id?) + reqN? < 0)
\end{schema}

\index{IllegalOperationReply}
\begin{schema}{IllegalOperationReply}
        type!: MSGTYPE; c!: CONTENT
\where
        type! = ViewReport\_Msg
\also
        c! = packReport(IllegalOperation\_Rpt)
\end{schema}

\index{ManualTrading}
\begin{zed}
        ManualTrading \defs ManualTradingRequest \pipe \\
\t1             ((LegalOperation \land UpdatePortfolio \land BackPatchPfDataBase \land Success) \lor \\
\t1             (IllegalOperation \land IllegalOperationReply)) \pipe Send
\end{zed}

\subsubsection{Compravendita automatica tramite il broker}

\begin{axdef}
        extractBrokerAddress: CONTENT \fun ADDRESS
\end{axdef}

\index{AutoTradingRequest}
\begin{schema}{AutoTradingRequest}
        type?: MSGTYPE; c?: CONTENT \\
        id!: ITEMID \\
        reqN!: \num \\
        brokerAddress!: ADDRESS 
\where
        type? = AutoTrading\_Msg
\also
        id! = extractItemId(c?)
\also
        reqN! = extractN(c?)
\also
        brokerAddress! = extractBrokerAddress(c?) 
\end{schema}

\begin{axdef}
        packRequest: ITEMID \cross \num \inj CONTENT
\end{axdef}

\index{CreateRequestForBroker}
\begin{schema}{CreateRequestForBroker}
        id?: ITEMID \\
        reqN?: \num \\
        brokerType!: MSGTYPE \\
        brokerC!: CONTENT
\where
        brokerType! = Trading\_Msg
\also
        brokerC! = packRequest(id?, reqN?)
\end{schema}

Da notare che in caso di compravendita automatica l'utente non \`e abilitato
ad acquistare strumenti che non siano gi\`a nel portafoglio.

\index{IllegalOperationAuto}
\begin{schema}{IllegalOperationAuto}
        \Xi Portfolio \\
        id?: ITEMID \\
        reqN?: \num 
\where
        reqN? = 0 \lor \\
\t1     (id? \notin \dom portfolio) \lor \\
\t1     (reqN? < 0 \land id? \in \dom portfolio \land 
		portfolio(id?) - pending(id?) + reqN? < 0)	
\end{schema}

\index{RequestForBroker}
\index{DoAutoTrading}
\index{AutoTrading}
\begin{zed}
	RequestForBroker \defs CreateRequestForBroker \pipe \\
\t1     	SendTo[brokerC? / c?, brokerType? / type?, brokerAddress? / addr?]
\also
	DoAutoTrading \defs \\
\t1             ((LegalOperation \land TransactionOn \land 
			RequestForBroker \land Success) \lor \\
\t1		(IllegalOperationAuto \land IllegalOperationReply)) \pipe Send
\also
        AutoTrading \defs AutoTradingRequest \pipe DoAutoTrading
\end{zed}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% INTERROGAZIONE DEI DATABASE %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Interrogazioni}

In questa sezione sono raccolte tutte le interrogazioni che l'utente pu\`o 
eseguire sul database storico e sul database investimento/valore.

\subsubsection{Valore del portafoglio in una certa data}

\index{PortfolioValueDateXRequest}
\begin{schema}{PortfolioValueDateXRequest}
        type?: MSGTYPE; c?: CONTENT \\
        date!: DATE
\where
        type? = PortfolioValueDateX\_Msg
\also
        date! = extractDate(c?)
\end{schema}

\index{PortfolioValueDateXOk}
\begin{schema}{PortfolioValueDateXOk}
        \Xi PfDataBase \\
        date?: DATE \\
        value!, investment!: VALUE
\where
        date? \in \dom pfValueDB
\also
        value! = pfValueDB(date?) 
\also
        investment! = getLastValue(pfInvestmentDB, date?)
\end{schema}

\begin{axdef}
        packValueValue: VALUE \cross VALUE \inj CONTENT
\end{axdef}

\index{PortfolioValueDateXReply}
\begin{schema}{PortfolioValueDateXReply}
        value?, investment?: VALUE \\
        type!: MSGTYPE; c!: CONTENT
\where
        type! = PortfolioValueDateX\_Rep
\also
        c! = packValueValue(value?, investment?)
\end{schema}

\index{WrongDate}
\begin{schema}{WrongDate}
        \Xi PfDataBase \\
        date?: DATE
\where
        date? \notin \dom pfValueDB
\end{schema}

\index{WrongDateReply}
\begin{schema}{WrongDateReply}
        type!: MSGTYPE; c!: CONTENT
\where
        type! = ViewReport\_Msg
\also
        c! = packReport(WrongDate\_Rpt)
\end{schema}

\index{PortfolioValueDateX}
\begin{zed}
        PortfolioValueDateX \defs PortfolioValueDateXRequest \pipe \\
\t1             ((PortfolioValueDateXOk \land PortfolioValueDateXReply) \lor \\
\t1		(WrongDate \land WrongDateReply)) \pipe Send
\end{zed}

\subsubsection{Visualizzazione di strumenti ordinati per quotazione o rendimento}

Con queste richieste l'utente pu\`o visualizzare un insieme di strumenti 
ordinati in base alla loro quotazione o al loro rendimento.
L'ordine degli elementi pu\`o essere crescente o decrescente:

\index{SORTTYPE}
\begin{zed}
	SORTTYPE ::=  INC | DEC
\end{zed}

Un ordinamento di strumenti \`e definito come una particolare sequenza 
degli stessi che gode di certe propriet\`a. 

\index{SORTEDITEMS}
\begin{schema}{SORTEDITEMS}
	itval: \seq (ITEMID \cross VALUE) \\
	sort: SORTTYPE
\where
	\forall i, j: 1 \upto \# itval | i \leq j @ \\
\t1		sort = INC \implies second(itval(i)) \leq second(itval(j)) \land \\
\t1		sort = DEC \implies second(itval(i)) \geq second(itval(j))
\end{schema}

\begin{axdef}
        extractItemSet: CONTENT \fun \power ITEMID
\end{axdef}

\index{ViewXIncQuotationOrderRequest}
\begin{schema}{ViewXIncQuotationOrderRequest}
        type?: MSGTYPE; c?: CONTENT \\
        x!: \power ITEMID
\where
        type? = ViewXIncQuotationOrder\_Msg
\also
        x! = extractItemSet(c?)
\end{schema}

\index{ViewXIncQuotationOrderOk}
\begin{schema}{ViewXIncQuotationOrderOk}
        \Xi DataBase \\
        x?: \power ITEMID \\
        order!: SORTEDITEMS
\where
        x? \neq \empty
\also
	\forall id: ITEMID | id \in x? @ dataDay(dataBase, id, today) = TRUE
\also
	\exists o: SORTEDITEMS @ \forall id: ITEMID | id \in x? @ \\
\t1		\langle (id, getQuotation(dataBase, id, today)) \rangle \subseq o.itval \land 
		o.sort = INC \land order! = o					
\end{schema}

\begin{axdef}
        packSortedItems: SORTEDITEMS \inj CONTENT
\end{axdef}

\index{ViewSortedItemsReply}
\begin{schema}{ViewSortedItemsReply}
        order?: SORTEDITEMS \\
        type!: MSGTYPE; c!: CONTENT
\where
        type! = ViewSortedItems\_Msg
\also
        c! = packSortedItems(order?)
\end{schema}

I casi di errore si hanno quando l'utente specifica un insieme vuoto di
strumenti, oppure quando il database storico non contiene i dati di borsa
relativi alla richiesta.

\index{NoItem}
\begin{schema}{NoItem}
        x?: \power ITEMID 
\where
        x? = \empty
\end{schema}

\index{NoData}
\begin{schema}{NoData}
        \Xi DataBase \\
        x?: \power ITEMID \\
\where
        x? \neq \empty
\also
        \exists id: ITEMID | id \in x? @ 
		dataDay(dataBase, id, today) = FALSE
\end{schema}

\index{WrongItems}
\begin{zed}
        WrongItems \defs NoItem \lor NoData     
\end{zed}

\index{WrongItemsReply}
\begin{schema}{WrongItemsReply}
        type!: MSGTYPE; c!: CONTENT
\where
        type! = ViewReport\_Msg
\also
        c! = packReport(WrongItems\_Rpt)
\end{schema}
 
\index{ViewXIncQuotationOrder}
\begin{zed}
        ViewXIncQuotationOrder \defs ViewXIncQuotationOrderRequest \pipe \\
\t1             ((ViewXIncQuotationOrderOk \pipe ViewSortedItemsReply) \lor \\
\t1             (WrongItems \land WrongItemsReply)) \pipe Send
\end{zed}

\index{ViewXDecQuotationOrderRequest}
\begin{schema}{ViewXDecQuotationOrderRequest}
        type?: MSGTYPE; c?: CONTENT \\
        x!: \power ITEMID 
\where
        type? = ViewXDecQuotationOrder\_Msg
\also
        x! = extractItemSet(c?)
\end{schema}

\index{ViewXDecQuotationOrderOk}
\begin{schema}{ViewXDecQuotationOrderOk}
        \Xi DataBase \\
        x?: \power ITEMID \\
        order!: SORTEDITEMS
\where
        x? \neq \empty
\also
        \forall id: ITEMID | id \in x? @ dataDay(dataBase, id, today) = TRUE 
\also
	\exists o: SORTEDITEMS @ \forall id: ITEMID | id \in x? @ \\
\t1		\langle (id, getQuotation(dataBase, id, today)) \rangle \subseq o.itval \land 
		o.sort = DEC \land order! = o					
\end{schema}

\index{ViewXDecQuotationOrder}
\begin{zed}
        ViewXDecQuotationOrder \defs ViewXDecQuotationOrderRequest \pipe \\
\t1             ((ViewXDecQuotationOrderOk \pipe ViewSortedItemsReply) \lor \\
\t1             (WrongItems \land WrongItemsReply)) \pipe Send
\end{zed}

\begin{axdef}
        extractDays: CONTENT \fun \nat
\end{axdef}

\index{ViewXIncYieldOrderRequest}
\begin{schema}{ViewXIncYieldOrderRequest}
        type?: MSGTYPE; c?: CONTENT \\
        x!: \power ITEMID \\
        days!: \nat
\where
        type? = ViewXIncYieldOrder\_Msg
\also
        x! = extractItemSet(c?)
\also 
        days! = extractDays(c?)
\end{schema}

\index{ViewXIncYieldOrderOk}
\begin{schema}{ViewXIncYieldOrderOk}
        \Xi DataBase \\
        x?: \power ITEMID \\
        days?: \nat \\
        order!: SORTEDITEMS
\where
        x? \neq \empty
\also
        \forall id: ITEMID | id \in x? @ \\
\t1             dataDay(dataBase, id, prevDate(today, days?)) = TRUE \land \\
\t1             dataExact(dataBase, id, today) = TRUE 
\also
	\exists o: SORTEDITEMS @ \forall id: ITEMID | id \in x? @ \\
\t1		\langle (id, getYield(dataBase, id, days?)) \rangle \subseq o.itval \land 
		o.sort = INC \land order! = o					
\end{schema}

\index{NoUpdatedData}
\begin{schema}{NoUpdatedData}
        \Xi DataBase \\
        x?: \power ITEMID \\
        days?: \nat
\where
        x? \neq \empty
\also
        \exists id: ITEMID | id \in x? @ \\
\t1             dataDay(dataBase, id, prevDate(today, days?)) = FALSE \lor \\
\t1             dataExact(dataBase, id, today) = FALSE
\end{schema}

\index{ViewXIncYieldOrder}
\begin{zed}
        ViewXIncYieldOrder \defs ViewXIncYieldOrderRequest \pipe \\
\t1             ((ViewXIncYieldOrderOk \pipe ViewSortedItemsReply) \lor \\
\t1             ((NoItem \lor NoUpdatedData) \land WrongItemsReply)) \pipe Send
\end{zed}

\index{ViewXDecYieldOrderRequest}
\begin{schema}{ViewXDecYieldOrderRequest}
        type?: MSGTYPE; c?: CONTENT \\
        x!: \power ITEMID \\
        days!: \nat 
\where
        type? = ViewXDecYieldOrder\_Msg
\also
        x! = extractItemSet(c?) 
\also
        days! = extractDays(c?)
\end{schema}

\index{ViewXDecYieldOrderOk}
\begin{schema}{ViewXDecYieldOrderOk}
        \Xi DataBase \\
        x?: \power ITEMID \\
        days?: \nat \\
        order!: SORTEDITEMS
\where
        x? \neq \empty
\also
        \forall id: ITEMID | id \in x? @ \\
\t1             dataDay(dataBase, id, prevDate(today, days?)) = TRUE \land \\
\t1             dataExact(dataBase, id, today) = TRUE 
\also
	\exists o: SORTEDITEMS @ \forall id: ITEMID | id \in x? @ \\
\t1		\langle (id, getYield(dataBase, id, days?)) \rangle \subseq o.itval \land 
		o.sort = DEC \land order! = o					
\end{schema}

\index{ViewXDecYieldOrder}
\begin{zed}
        ViewXDecYieldOrder \defs ViewXDecYieldOrderRequest \pipe \\
\t1             ((ViewXDecYieldOrderOk \pipe ViewSortedItemsReply) \lor \\
\t1             ((NoItem \lor NoUpdatedData) \land WrongItemsReply)) \pipe Send
\end{zed}

\subsubsection{Visualizzazione del grafico relativo all'andamento del portafoglio}

\begin{axdef}
        extractStartDate, extractEndDate: CONTENT \fun DATE
\end{axdef}

\index{ViewPortfolioGraphRequest}
\begin{schema}{ViewPortfolioGraphRequest}
        type?: MSGTYPE \\
        c?: CONTENT \\
        start!, end!: DATE 
\where
        type? = ViewPortfolioGraph\_Msg
\also
        start! = extractStartDate(c?)
\also
        end! = extractEndDate(c?)
\end{schema}

Un grafico relativo al portafoglio pu\`o essere rappresentato come un
sottoinsieme del database del portafoglio stesso:

\index{PFGRAPH}
\begin{schema}{PFGRAPH}
	vGraph, iGraph: PFDATABASE \\
	start, end: DATE
\where
	start \leq end
\end{schema}

Da notare che, nel caso in cui nella data iniziale il database non \`e definito,
verr\`a usata la data antecedente pi\`u vicina a quella specificata per cui
sono disponibili i dati investimento e valore.

\index{ViewPortfolioGraphOk}
\begin{schema}{ViewPortfolioGraphOk}
        \Xi PfDataBase \\
        start?, end?: DATE \\
        graph!: PFGRAPH
\where
        start? \leq today \land end? \leq today
\also
        start? \leq end?
\also
	\zlet domain == \{ d: DATE | start? \leq d \land d \leq end? \}; \\
\t1		uptoV == \{ d: DATE | d \leq start? \land d \in \dom pfValueDB \}; \\
\t1		uptoI == \{ d: DATE | d \leq start? \land d \in \dom pfInvestmentDB \} @ \\
\t1		\zlet lastV == \zif uptoV = \empty \zthen 
				\empty \zelse \{ max~uptoV \}; \\
\t2			lastI == \zif uptoI = \empty \zthen 
					\empty \zelse \{ max~uptoI \} @ \\
\t3				graph!.start = start? \land graph!.end = end? \land \\
\t3				graph!.vGraph = (domain \cup lastV) \dres pfValueDB \land \\
\t3				graph!.iGraph = (domain \cup lastI) \dres pfInvestmentDB
\end{schema}

\index{WrongRange}
\begin{schema}{WrongRange}
        \Xi PfDataBase \\
        start?, end?: DATE
\where
        start? > today \lor end? > today \lor start? > end?
\end{schema}

\index{WrongRangeReply}
\begin{schema}{WrongRangeReply}
        type!: MSGTYPE; c!: CONTENT
\where
        type! = ViewReport\_Msg
\also
        c! = packReport(WrongRange\_Rpt)
\end{schema}

\begin{axdef}
        packPfGraph: PFGRAPH \fun CONTENT
\end{axdef}

\index{ViewPortfolioGraphReply}
\begin{schema}{ViewPortfolioGraphReply}
        graph?: PFGRAPH \\
        type!: MSGTYPE; c!: CONTENT 
\where
        type! = ViewPortfolioGraph\_Rep
\also
        c! = packPfGraph(graph?)
\end{schema}

\index{ViewPortfolioGraph}
\begin{zed}
        ViewPortfolioGraph \defs ViewPortfolioGraphRequest \pipe \\
\t1             ((ViewPortfolioGraphOk \pipe ViewPortfolioGraphReply) \lor \\
\t1             (WrongRange \land WrongRangeReply)) \pipe Send
\end{zed}

\subsubsection{Visualizzazione dell'andamento di un insieme di strumenti}

Con questa interrogazione l'utente specifica un insieme X di strumenti
finanziari ed un intervallo Y di giorni e l'applicazione visualizza
su un grafico cartesiano l'andamento della quotazione degli strumenti
nell'intervallo. 
Come prima, anche qui il grafico pu\`o essere inteso come un particolare
sottoinsieme del database dei dati di borsa. L'unico accorgimento riguarda
la possibilit\`a di questo database di contenere ``buchi'' in 
corrispondenza di strumenti non quotati. 

\index{DBGRAPH}
\begin{schema}{DBGRAPH}
	dbGraph: DATABASE \\
	start, end: DATE
\where
	start \leq end
\end{schema}

\index{ViewDataBaseGraphRequest}
\begin{schema}{ViewDataBaseGraphRequest}
        type?: MSGTYPE; c?: CONTENT \\
        x!: \power ITEMID \\
        start!, end!: DATE
\where
        type? = ViewDataBaseGraph\_Msg
\also
        x! = extractItemSet(c?)
\also
        start! = extractStartDate(c?)
\also
        end! = extractEndDate(c?)
\end{schema}

\index{ViewDataBaseGraphOk}
\begin{schema}{ViewDataBaseGraphOk}
        \Xi DataBase \\
        start?, end?: DATE \\
        x?: \power ITEMID \\
        graph!: DBGRAPH
\where
        start? \leq today \land end? \leq today
\also
        start? \leq end?
\also
	x? \neq \empty
\also
	\zlet domain == \{ id: ITEMID; d: DATE | id \in x? \land 
		start? \leq d \land d \leq end? \}; \\
\t1		last == \{ id: ITEMID; d: DATE | \\
\t2			dataExact(dataBase, id, start?) = FALSE \land \\
\t2			dataDay(dataBase, id, start?) = TRUE \land \\
\t2			d = max~\{ d: DATE | d < start? \land 
				dataDay(dataBase, id, start?) = TRUE \} \} @ \\
\t1		graph!.start = start? \land \\
\t1		graph!.end = end? \land \\
\t1		graph!.dbGraph = (domain \cup last) \dres dataBase
\end{schema}

\begin{axdef}
	packDataBaseGraph: DBGRAPH \inj CONTENT
\end{axdef}

\index{ViewdataBaseGraphReply}
\begin{schema}{ViewDataBaseGraphReply}
	graph?: DBGRAPH \\
	type!: MSGTYPE; c!: CONTENT
\where
	type! = ViewDataBaseGraph\_Rep
\also
	c! = packDataBaseGraph(graph?)
\end{schema}

\index{ViewDataBaseGraph}
\begin{zed}
        ViewDataBaseGraph \defs ViewDataBaseGraphRequest \pipe \\
\t1             ((ViewDataBaseGraphOk \pipe ViewDataBaseGraphReply) \lor \\
\t1		(NoItem \land WrongItemsReply) \lor \\
\t1             (WrongRange \land WrongRangeReply)) \pipe Send
\end{zed}

%%%%%%%%%%%%%%%%%%%%%%%%%
% GESTIONE DELLE REGOLE %
%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Gestione delle regole}

L'applicazione gestisce le regole attraverso due entit\`a: eventi e azioni. 
Gli eventi sono predicati costruiti a partire da eventi atomici e dai 
connettivi logici {\em and} e {\em or}. Un evento atomico riguarda 
l'attributo di un singolo strumento finanziario, ovvero la quotazione, 
il rendimento o il rendimento nominale (solo nel caso di titoli di stato).
Le azioni possono consistere nella visualizzazione di un messaggio o nell'
invio di un messaggio ad un broker per acquistare o vendere strumenti.

\index{ATOMIC}
\index{EVENT}
\index{ACTION}
\begin{syntax}
        ATOMIC & ::= & quotation \ldata ITEMID \cross 
                (VALUE \rel VALUE) \cross VALUE \rdata \\
                      & | & yield \ldata ITEMID \cross \nat \cross 
                (VALUE \rel VALUE) \cross VALUE \rdata \\
                      & | & nominal\_yield \ldata ITEMID \cross
                (VALUE \rel VALUE) \cross VALUE \rdata
\also
        EVENT & ::= & atomic \ldata ATOMIC \rdata \\
              & | & and \ldata EVENT \cross EVENT \rdata \\
              & | & or \ldata EVENT \cross EVENT \rdata 
\also
        ACTION & ::= & print \ldata STRING \rdata \\
                & | & email \ldata ITEMID \cross \num \cross ADDRESS \rdata
\end{syntax}

La funzione seguente determina il valore booleano di un evento atomico:

\index{evalAtomicEvent}
\begin{axdef}
        evalAtomicEvent: DATABASE \cross ATOMIC \fun BOOLEAN
\where
        \forall db: DATABASE; ae: ATOMIC; \\
\t1             id: ITEMID; rel: VALUE \rel VALUE; val: VALUE | \\
\t2             ae = quotation(id, rel, val) @ evalAtomicEvent(db, ae) = \\
\t2             \zif dataExact(db, id, today) = TRUE \zthen \\ 
\t3                     \zif (getQuotation(db, id, today), val) \in rel \zthen TRUE 
                        \zelse FALSE \\
\t2             \zelse FALSE
\also
        \forall db: DATABASE; ae: ATOMIC; \\
\t1             id: ITEMID; rel: VALUE \rel VALUE; val: VALUE | \\
\t2             ae = nominal\_yield(id,rel,val) @ evalAtomicEvent(db, ae) = \\
\t2             \zif dataExact(db, id, today) = TRUE \land is(id) = BOND \zthen \\
\t3                     \zif (getNominalYield(db, id, today), val) \in rel \zthen TRUE 
                        \zelse FALSE \\
\t2             \zelse FALSE
\also
        \forall db: DATABASE; ae: ATOMIC; date: DATE; \\
\t1             id: ITEMID; days: \nat; rel: VALUE \rel VALUE; val: VALUE | \\
\t2             ae = yield(id, date, rel, val) @ evalAtomicEvent(db, ae) = \\ 
\t2             \zif dataExact(db, id, today) = TRUE \land \\
\t3                     dataDay(db, id, prevDate(today, days)) = TRUE \zthen \\
\t4                     	\zif (getYield(db, id, prevDate(today, days)), val) 
                                	\in rel \zthen TRUE \\
\t4				\zelse FALSE \\
\t2             \zelse FALSE
\end{axdef}

La funzione seguente valuta ricorsivamente il valore booleano di un evento:

\index{evalEvent}
\begin{axdef}
        evalEvent: DATABASE \cross EVENT \fun BOOLEAN
\where
        \forall db: DATABASE; e: EVENT; ae: ATOMIC | e = atomic(ae) @ \\
\t1             evalEvent(db, e) = evalAtomicEvent(db, ae)
\also
        \forall db: DATABASE; e, e_1, e_2: EVENT | e = and(e_1, e_2) @ 
                evalEvent(db, e) = \\
\t1			\zif evalEvent(db, e_1) = TRUE \land 
                        evalEvent(db, e_2) = TRUE \zthen TRUE \zelse FALSE
\also
        \forall db: DATABASE; e, e_1, e_2: EVENT | e = or(e_1, e_2) @ 
                evalEvent(db, e) = \\
\t1			\zif evalEvent(db, e_1) = TRUE \lor 
                        evalEvent(db, e_2) = TRUE \zthen TRUE \zelse FALSE
\end{axdef}

Ogni regola \`e dunque composta da un evento ed un'azione ed \`e univocamente
determinata da un identificatore (RULEID). 

\index{RULE}
\index{RULEID}
\index{RULEDB}
\begin{zed}
        RULE == EVENT \cross ACTION 
\also
        [RULEID]
\also
        RULEDB == RULEID \pinj RULE
\end{zed}

Ogni regola ha un flag di stato che indica se la regola \`e attiva oppure no.
Solo gli eventi di regole attive vengono controllati periodicamente.

\index{RULEFLAGDB}
\begin{zed}
        RULEFLAGDB == RULEID \pfun BOOLEAN
\end{zed}

\index{Rules}
\begin{schema}{Rules}
        rule: RULEDB \\
        ruleFlag: RULEFLAGDB
\where
        \dom rule = \dom ruleFlag
\end{schema}

\index{InitRules}
\begin{schema}{InitRules}
        Rules'
\where
        \dom rule' = \empty
\end{schema}

\subsubsection{Visualizzazione delle regole}

La seguente funzione \`e usata per inviare il database delle regole all'
applicazione client:

\begin{axdef}
        packRules: RULEDB \cross RULEFLAGDB \inj CONTENT
\end{axdef}

\index{ViewRulesRequest}
\begin{schema}{ViewRulesRequest}
        type?: MSGTYPE
\where
        type? = ViewRules\_Msg
\end{schema}

\index{CreateRulesTable}
\begin{schema}{CreateRulesTable}
        \Xi Rules \\
        ruleDB!: RULEDB \\
        ruleFlagDB!: RULEFLAGDB
\where
        ruleDB! = rule
\also
        ruleFlagDB! = ruleFlag
\end{schema}

\index{ViewRulesReply}
\begin{schema}{ViewRulesReply}
        \Xi User \\
        ruleDB?: RULEDB \\
        ruleFlagDB?: RULEFLAGDB \\
        type!: MSGTYPE; c!: CONTENT
\where
        type! = ViewRules\_Rep
\also
        c! = packRules(ruleDB?, ruleFlagDB?)
\end{schema}

\index{ViewRules}
\begin{zed}
        ViewRules \defs ViewRulesRequest \pipe 
		CreateRulesTable \pipe ViewRulesReply \pipe Send
\end{zed}

\subsubsection{Aggiunta di una nuova regola}

L'utente pu\`o aggiungere una nuova regola nel sistema fornendo l'evento e
l'azione ad essa associati. Il controllo sintattico di correttezza dell'evento
e dell'azione sono svolti da parte del client.

\begin{axdef}
        extractRuleId: CONTENT \fun RULEID  
\also
        extractEvent: CONTENT \fun EVENT
\also
        extractAction: CONTENT \fun ACTION
\end{axdef}

\index{AddRuleRequest}
\begin{schema}{AddRuleRequest}
        type?: MSGTYPE; c?: CONTENT \\
        event!: EVENT \\
        action!: ACTION 
\where
        type? = AddRule\_Msg
\also
        event! = extractEvent(c?)
\also
        action! = extractAction(c?)
\end{schema}

L'identificatore della regola aggiunta viene scelto dall'applicazione
stessa:

\index{AddRuleOk}
\begin{schema}{AddRuleOk}
        \Delta Rules \\
        event?: EVENT \\
        action?: ACTION
\where
        \forall rid: RULEID | rid \in \dom rule @ rule(rid) \neq (event?, action?)
\also
        \exists rid: RULEID | rid \notin \dom rule @ \\
\t1             rule' = rule \oplus \{ rid \mapsto (event?, action?) \} \land 
                ruleFlag' = ruleFlag \oplus \{ rid \mapsto FALSE \}
\end{schema}

Non \`e possibile specificare pi\`u volte la stessa regola:

\index{RulePresent}
\begin{schema}{RulePresent}
        \Xi Rules \\
        event?: EVENT \\
        action?: ACTION
\where
        \exists rid: RULEID | rid \in \dom rule @ rule(rid) = (event?, action?)
\end{schema}

\index{RulePresentReply}
\begin{schema}{RulePresentReply}
        \Xi User \\
        type!: MSGTYPE; c!: CONTENT
\where
        type! = ViewReport\_Msg
\also
        c! = packReport(RulePresent\_Rpt)
\end{schema}

\index{AddRule}
\begin{zed}
        AddRule \defs AddRuleRequest \pipe \\
\t1             ((AddRuleOk \land Success) \lor \\
\t1             (RulePresent \land RulePresentReply)) \pipe Send
\end{zed}

\subsubsection{Cancellazione di una regola}

L'utente specifica l'identificatore di una regola da cancellare:

\index{DeleteRuleRequest}
\begin{schema}{DeleteRuleRequest}
        type?: MSGTYPE; c?: CONTENT \\
        rid!: RULEID
\where
        type? = DeleteRule\_Msg
\also
        rid! = extractRuleId(c?)
\end{schema}

\index{DeleteRuleOk}
\begin{schema}{DeleteRuleOk}
        \Delta Rules \\
        rid?: RULEID
\where
        rid? \in \dom rule
\also
        rule' = \{ rid? \} \ndres rule
\also
	ruleFlag' = \{ rid? \} \ndres ruleFlag
\end{schema}

\index{RuleNotPresent}
\begin{schema}{RuleNotPresent}
        \Xi Rules \\
        rid?: RULEID
\where
        rid? \notin \dom rule
\end{schema}

\index{RuleNotPresentReply}
\begin{schema}{RuleNotPresentReply}
        \Xi User \\
        type!: MSGTYPE; c!: CONTENT
\where
        type! = ViewReport\_Msg
\also
        c! = packReport(RuleNotPresent\_Rpt)
\end{schema}

\index{DeleteRule}
\begin{zed}
        DeleteRule \defs DeleteRuleRequest \pipe \\ 
\t1             ((DeleteRuleOk \land Success) \lor \\
\t1             (RuleNotPresent \land RuleNotPresentReply)) \pipe Send
\end{zed}

\subsubsection{Attivazione di una regola}

Ogni nuova regola inserita \`e marcata esplicitamente {\em non} attiva
dall'applicazione, inoltre una regola il cui evento si verifica viene
disabilitata automaticamente. 
L'utente pu\`o attivare una regola attraverso questo comando.

\index{SetRuleOnRequest}
\begin{schema}{SetRuleOnRequest}
        type?: MSGTYPE; c?: CONTENT \\
        rid!: RULEID
\where
        type? = SetRuleOn\_Msg
\also
        rid! = extractRuleId(c?)
\end{schema}

\index{SetRuleOnOk}
\begin{schema}{SetRuleOnOk}
        \Delta Rules \\
        rid?: RULEID
\where
        rid? \in \dom ruleFlag
\also
        ruleFlag' = ruleFlag \oplus \{ rid? \mapsto TRUE \}
\also
        rule' = rule
\end{schema}

\index{SetRuleOn}
\begin{zed}
        SetRuleOn \defs SetRuleOnRequest \pipe \\
\t1             ((SetRuleOnOk \land Success) \lor \\
\t1             (RuleNotPresent \land RuleNotPresentReply)) \pipe Send
\end{zed}

\subsubsection{Disattivazione di una regola}

L'utente pu\`o decidere di disattivare una regola attraverso il seguente
comando:

\index{SetRuleOffRequest}
\begin{schema}{SetRuleOffRequest}
        type?: MSGTYPE; c?: CONTENT \\
        rid!: RULEID
\where
        type? = SetRuleOff\_Msg
\also
        rid! = extractRuleId(c?)
\end{schema}

\index{SetRuleOffOk}
\begin{schema}{SetRuleOffOk}
        \Delta Rules \\
        rid?: RULEID
\where
        rid? \in \dom ruleFlag
\also
        ruleFlag' = ruleFlag \oplus \{ rid? \mapsto FALSE \}
\also
        rule' = rule
\end{schema}

\index{SetRuleOff}
\begin{zed}
        SetRuleOff \defs SetRuleOffRequest \pipe \\
\t1             ((SetRuleOffOk \land Success) \lor \\
\t1             (RuleNotPresent \land RuleNotPresentReply)) \pipe Send
\end{zed}

\subsubsection{Verifica delle regole}

Lo schema seguente determina se l'evento associato ad una regola \`e 
verificato:

\index{TestRuleOk}
\begin{schema}{TestRuleOk}
        \Delta Rules \\
        \Xi DataBase \\
        rid?: RULEID 
\where
        rid? \in \dom rule
\also
        ruleFlag(rid?) = TRUE
\also
        evalEvent(dataBase, first(rule(rid?))) = TRUE
\also
        ruleFlag' = ruleFlag \oplus \{ rid? \mapsto FALSE \}
\end{schema}

Le regole non attive non sono prese in considerazione:

\index{TestRuleOff}
\begin{schema}{TestRuleOff}
        \Xi Rules \\
        rid?: RULEID
\where
        rid? \in \dom rule
\also
        ruleFlag(rid?) = FALSE
\end{schema}

\index{TestRuleFalse}
\begin{schema}{TestRuleFalse}
        \Xi Rules \\
        \Xi DataBase \\
        rid?: RULEID
\where
        rid? \in \dom rule
\also
        ruleFlag(rid?) = TRUE
\also
        evalEvent(dataBase, first (rule(rid?))) = FALSE
\end{schema}

Seguono gli schemi che ``eseguono'' l'azione, una volta che l'evento \`e 
verificato:

\index{ExecActionEmailOk}
\begin{schema}{ExecActionEmailOk}
        action?: ACTION \\
        rid?: RULEID \\
        id!: ITEMID \\
        n!: \num \\
        brokerAddress!: ADDRESS 
\where
        \exists id: ITEMID; n: \num; addr: ADDRESS | \\
\t1             action? = email(id, n, addr) @ 
                        id! = id \land n! = n \land brokerAddress! = addr
\end{schema}

\index{ExecRuleEmail}
\begin{zed}
        ExecRuleEmail \defs ExecActionEmailOk \pipe DoAutoTrading
\end{zed}

\begin{axdef}
	packString: STRING \inj CONTENT
\end{axdef}

\index{ExecActionPrint}
\begin{schema}{ExecActionPrint}
        action?: ACTION \\
        type!: MSGTYPE; c!: CONTENT
\where
        \exists s: STRING | action? = print(s) @ 
                type! = ViewString\_Msg \land c! = packString(s)
\end{schema}

\index{ExecRulePrint}
\begin{zed}
        ExecRulePrint \defs ExecActionPrint \pipe Send
\end{zed}

\index{ExecRule}
\begin{zed}
        ExecRule \defs ExecRulePrint \lor ExecRuleEmail 
\end{zed}

La verifica delle regole avviene dopo ogni aggiornamento del database 
storico attraverso lo schema {\it UpdateDataBase}. L'identificatore di ogni 
regola viene passato allo schema seguente:

\index{TestRule}
\begin{zed}
        TestRule \defs (TestRuleOk \land ExecRule) \lor 
                TestRuleOff \lor TestRuleFalse \lor RuleNotPresent
\end{zed}

%%%%%%%%%
% VARIE %
%%%%%%%%%

\subsection{Varie}

\subsubsection{Timeout}

Allo scadere del timeout l'applicazione prepara un messaggio con cui richiede
dal sito di borsa i dati aggiornati degli strumenti nel portafoglio e
nel monitor. Il timeout non \`e gestito esplicitamente in questa specifica per
semplicit\`a, ma si pu\`o pensare ad un parametro configurabile dall'utente
che determina la frequenza del timeout.
Per garantire che non vi siano ``buchi'' nel database investimento/valore
\`e necessario che {\it TimeOut} sia richiamato almeno una volta al giorno.

\begin{axdef}
        packNeededData: DATE \cross \power ITEMID \inj CONTENT
\end{axdef}

\index{RequestData}
\begin{schema}{RequestData}
        \Xi Server \\
        \Xi Portfolio \\
        addr!: ADDRESS; type!: MSGTYPE; c!: CONTENT
\where
        addr! = stockExchangeAddr
\also
        type! = UpdateDataBase\_Msg
\also
        c! = packNeededData(today, \dom portfolio)
\end{schema}

\index{TimeOut}
\begin{zed}
        TimeOut \defs RequestData \pipe SendTo
\end{zed}

\subsubsection{Visualizzazione di tutti gli strumenti}

L'applicazione consente di reperire dal sito di borsa il nome di tutti gli
strumenti finanziari conosciuti associati con il relativo identificatore.
I tre schemi che seguono gestiscono la richiesta dell'utente e la 
inoltrano al sito di borsa:

\index{ViewAllItemsRequest}
\begin{schema}{ViewAllItemsRequest}
        type?: MSGTYPE
\where
        type? = ViewAllItems\_Msg
\end{schema}

\index{ViewAllItemsReply}
\begin{schema}{ViewAllItemsReply}
        \Xi Server \\
        seAddr!: ADDRESS; seType!: MSGTYPE; seC!: CONTENT
\where
        seAddr! = stockExchangeAddr 
\also
        seType! = GetAllItems\_Msg
\also
        seC! = nullContent
\end{schema}

\index{ViewAllItemsReply}
\begin{zed}
        ViewAllItems \defs ViewAllItemsRequest \land \\
\t1		(ViewAllItemsReply \pipe SendTo[seAddr? / addr?, seType? / type?, seC? / c?]) \land \\
\t1		(Success \pipe Send)
\end{zed}

Quando il sito di borsa risponde con l'elenco dei nomi, il server instrada
il pacchetto verso il client:

\index{GetAllItemsRequest}
\begin{schema}{GetAllItemsRequest}
        type?: MSGTYPE
\where
        type? = GetAllItems\_Rep
\end{schema}

\index{GetAllItemsReply}
\begin{schema}{GetAllItemsReply}
	\Xi User \\
        type!: MSGTYPE
\where
        type! = ViewAllItems\_Rep
\also
	userConnected = TRUE
\end{schema}

\index{GetAllItems}
\begin{zed}
        GetAllItems \defs GetAllItemsRequest \pipe 
		((GetAllItemsReply \pipe Send) \lor NotConnected)
\end{zed}

\subsubsection{Aggiunta e cancellazione di strumenti dal monitor}

\index{AddItemRequest}
\begin{schema}{AddItemRequest}
	type?: MSGTYPE; c?: CONTENT \\
	id!: ITEMID
\where
	type? = AddItem\_Msg
\also
	id! = extractItemId(c?)
\end{schema}

\index{AddItemOk}
\begin{schema}{AddItemOk}
	\Delta Portfolio \\
	id?: ITEMID
\where
	id? \notin \dom portfolio
\also
	portfolio' = portfolio \oplus \{ id? \mapsto 0 \}
\also
	pending' = pending \oplus \{ id? \mapsto 0 \}
\also 
	transaction' = transaction \oplus \{ id? \mapsto 0 \}
\end{schema}

\index{ItemPresent}
\begin{schema}{ItemPresent}
	\Xi Portfolio \\
	id?: ITEMID
\where
	id? \in \dom portfolio
\end{schema}

\index{ItemPresentReply}
\begin{schema}{ItemPresentReply}
	type!: MSGTYPE; c!: CONTENT
\where
	type! = ViewReport\_Msg
\also
        c! = packReport(ItemPresent\_Rpt)
\end{schema}
	
\index{AddItem}
\begin{zed}
	AddItem \defs AddItemRequest \pipe \\
\t1		((AddItemOk \land Success) \lor \\
\t1		(ItemPresent \land ItemPresentReply)) \pipe Send
\end{zed}

L'utente pu\`o decidere di eliminare dal portafoglio strumenti a cui non
\`e pi\`u interessato. Tali strumenti devono far parte del {\em monitor}.

\index{DeleteItemRequest}
\begin{schema}{DeleteItemRequest}
	type?: MSGTYPE; c?: CONTENT \\
	id!: ITEMID 
\where
	type? = DeleteItem\_Msg
\also
	id! = extractItemId(c?)
\end{schema}

\index{DeleteItemOk}
\begin{schema}{DeleteItemOk}
	\Delta Portfolio \\
	id?: ITEMID
\where
	id? \in monitor
\also
	portfolio' = \{ id? \} \ndres portfolio
\also
	pending' = \{ id? \} \ndres pending
\also
	transaction' = \{ id? \} \ndres transaction
\end{schema}

Uno strumento \`e definito ``occupato'' ({\em busy}) se \`e posseduto 
dall'utente o comunque \`e in corso una transazione che lo conivolge:
in questo caso non \`e possibile cancellarlo dal portafoglio.

\index{ItemBusy}
\begin{schema}{ItemBusy}
	\Xi Portfolio \\
	id?: ITEMID
\where
	id? \notin monitor
\also
	id? \in \dom portfolio
\end{schema}

\index{ItemBusyReply}
\begin{schema}{ItemBusyReply}
	type!: MSGTYPE; c!: CONTENT
\where
	type! = ViewReport\_Msg
\also
        c! = packReport(ItemBusy\_Rpt)
\end{schema}

\index{ItemNotPresent}
\begin{schema}{ItemNotPresent}
	\Xi Portfolio \\
	id?: ITEMID
\where
	id? \notin \dom portfolio
\end{schema}

\index{ItemNotPresentReply}
\begin{schema}{ItemNotPresentReply}
	type!: MSGTYPE; c!: CONTENT
\where
	type! = ViewReport\_Msg
\also
        c! = packReport(ItemNotPresent\_Rpt)
\end{schema}

\index{DeleteItem}
\begin{zed}
	DeleteItem \defs DeleteItemRequest \pipe \\
\t1		((DeleteItemOk \land Success) \lor \\
\t1		(ItemBusy \land ItemBusyReply) \lor \\
\t1		(ItemNotPresent \land ItemNotPresentReply)) \pipe Send
\end{zed}

\subsection{Gestione finale dei comandi}

\index{UserCommand}
\index{DoCommand}
\begin{zed}
        UserCommand \defs UserConnected \land \\
\t1             (ManualTrading \lor AutoTrading \lor \\
\t1             PortfolioValueDateX \lor ViewXIncQuotationOrder \lor \\
\t1             ViewXDecQuotationOrder \lor ViewXIncYieldOrder \lor \\
\t1             ViewXDecYieldOrder \lor ViewPortfolioGraph \lor \\
\t1             ViewDataBaseGraph \lor ViewRules \lor AddRule \lor \\
\t1             DeleteRule \lor SetRuleOn \lor SetRuleOff \lor \\
\t1		AddItem \lor DeleteItem)
\also
        DoCommand \defs (Receive \pipe \\
\t1		(UserCommand \lor OpenConnection \lor \\
\t1             CloseConnection \lor BrokerNotification \lor \\
\t1             UpdateDataBase \lor GetAllItems \lor \\
\t1		ViewAllItems)) \lor NoMessage  
\end{zed}

%%%%%%%%%%%%%%%%%%%%%%%
% APPLICAZIONE CLIENT %
%%%%%%%%%%%%%%%%%%%%%%%

\section{Applicazione Client}

L'applicazione client, che in un caso specifico si pu\`o ridurre ad un Web
browser, non fa altro che convertire le richieste dell'utente in messaggi
da inviare al server e visualizzare tramite un'opportuna interfaccia 
i dati o i messaggi che il server invia in risposta alle richieste.
Si suppone che il client verifichi la correttezza sintattica delle
richieste o, equivalentemente, vincoli l'utente a generare solo richieste 
corrette tramite un'opportuna organizzazione dell'interfaccia.

\addtocontents{toc}{\protect\vspace{0.5cm}}
\addtocontents{toc}{{\bf Indice analitico}}
\printindex

\end{document}

