Derivación deductiva de programas funcionales con patrones

Una de las dificultades principales en el desarrollo de software es la ausencia de un marco conceptual adecuado para su estudio. Una propuesta la constituye el modelo transformativo, que entiende el desarrollo de software como un proceso iterativo de transformación de especificaciones: se parte de una especificación inicial que va transformándose sucesivamente hasta obtener una especificación final que se toma como programa. Este modelo básico puede llevarse a la práctica de varias maneras. En concreto, la aproximación deductiva toma una sentencia lógica como especificación inicial y su proceso transformador consiste en la demostración de la sentencia; como producto secundario de la demostración se deriva un programa que satisface la especificación inicial. La tesis desarrolla un método deductivo para la derivación de programas funcionales con patrones, escritos en un lenguaje similar a Hope. El método utiliza una lógica multigénero, cuya relación con el lenguaje de programación es estudiada. También se identifican los esquemas de demostración necesarios para la derivación de funciones con patrones, basados en la demostración independiente de varias subsentencias. Cada subsentencia proporciona una subespecificación de una ecuación del futuro programa a derivar. Nuestro método deductivo está inspirado en uno previo de Zohar Manna y Richard Waldinger, conocido como el cuadro deductivo, que deriva programas en un lenguaje similar a Lisp. El nuevo método es una modificación del cuadro de estos autores, que incorpora géneros y permite demostrar una especificación mediante varios cuadros. Cada cuadro demuestra una subespecificación y por tanto deriva una ecuación del programa. Se prevén mecanismos para que los programas derivados puedan contener definiciones locales con patrones y variables anónimas y sinónimas y para que las funciones auxiliares derivadas no usen variables de las funciones principales. La tesis se completa con varios ejemplos de aplicación, un mecanismo que independentiza el método del lenguaje de programación y un prototipo de entorno interactivo de derivación deductiva. Categorías y descriptores de materia CR D.l.l [Técnicas de programación]: Programación funcional; D.2.10 [Ingeniería de software]: Diseño - métodos; F.3.1 [Lógica y significado de los programas]: Especificación, verificación y razonamiento sobre programas - lógica de programas; F.3.3 [Lógica y significado de los programas]: Estudios de construcciones de programas - construcciones funcionales; esquemas de programa y de recursion; 1.2.2 [Inteligencia artificial]: Programación automática - síntesis de programas; 1.2.3 [Inteligencia artificial]: Deducción y demostración de teoremas]: extracción de respuesta/razón; inducción matemática. Términos generales Programación funcional, síntesis de programas, demostración de teoremas. Otras palabras claves y expresiones Funciones con patrones, cuadro deductivo, especificación parcial, inducción estructural, teorema de descomposición.---ABSTRACT---One of the main difficulties in software development is the lack of an adequate conceptual framework of study. The transformational model is one such proposal that conceives software development as an iterative process of specifications transformation: an initial specification is developed and successively transformed until a final specification is obtained and taken as a program. This basic model can be implemented in several ways. The deductive approach takes a logical sentence as the initial specification and its proof constitutes the transformational process; as a byproduct of the proof, a program which satisfies the initial specification is derived. In the thesis, a deductive method for the derivation of Hope-like functional programs with patterns is developed. The method uses a many-sorted logic, whose relation to the programming language is studied. Also the proof schemes necessary for the derivation of functional programs with patterns, based on the independent proof of several subsentences, are identified. Each subsentence provides a subspecification of one equation of the future program to be derived. Our deductive method is inspired on a previous one by Zohar Manna and Richard Waldinger, known as the deductive tableau, which derives Lisp-like programs. The new method incorporates sorts in the tableau and allows to prove a sentence with several tableaux. Each tableau proves a subspecification and therefore derives an equation of the program. Mechanisms are included to allow the derived programs to contain local definitions with patterns and anonymous and synonymous variables; also, the derived auxiliary functions cannot reference parameters of their main functions. The thesis is completed with several application examples, i mechanism to make the method independent from the programming language and an interactive environment prototype for deductive derivation. CR categories and subject descriptors D.l.l [Programming techniques]: Functional programming; D.2.10 [Software engineering]: Design - methodologies; F.3.1 [Logics and meanings of programa]: Specifying and verifying and reasoning about programs - logics of programs; F.3.3 [Logics and meanings of programs]: Studies of program constructs - functional constructs; program and recursion schemes; 1.2.2 [Artificial intelligence]: Automatic programming - program synthesis; 1.2.3 [Artificial intelligence]: Deduction and theorem proving - answer/reason extraction; mathematical induction. General tenas Functional programming, program synthesis, theorem proving. Additional key words and phrases Functions with patterns, deductive tableau, structural induction, partial specification, descomposition theorem.

Un contributo alla sostenibilità ambientale: metano e territorio in Campania

IX Giornata Studio INU Infrastrutture blu e verdi, reti virtuali, culturali e sociali

Zeylü's-Siyer : manuscript, 1698

Continuation of Veysî's Dürretü't-tâc fi sîreti sâhibi'l-mi'râc: first biography of the Prophet Muḥammad divided into sections on Mecca and Medina.

Análise fenomenológica de fenómenos corporais anómalos na esquizofrenia

Trabalho Final do Curso de Mestrado Integrado em Medicina, Faculdade de Medicina, Universidade de Lisboa, 2014

QUIC tramite udp: un’indagine sul protocollo che intende velocizzare il web

In questo documento ho analizzato lo scenario della passata e dell’odierna Internet, dal classico protocollo HTTP, al protocollo sperimentale QUIC, argomento di questa tesi. In primis ho analizzato gli attuali protocolli utilizzati nella rete e ricercato i motivi che hanno portato a crearne di nuovi, successivamente ho effettuato un analisi teorica del protocollo affidandomi ai documenti forniti dall'IETF, poi in un capitolo a sé ho descritto l'handshake crittografato tipico di questo protocollo ed infine nell'ultimo capitolo ho mostrato graficamente e praticamente come lavora il protocollo in una reale implementazione. Dopo aver completato questa tesi, mi sono potuto rendere conto di quanto sia necessario un cambio di rotta verso protocolli di rete più veloci, sicuri ed affidabili. I classici protocolli oramai non sono più sufficienti a soddisfare le migliaia di richieste di connessione e presentano, come si vedrà, delle lacune a cui bisogna porre rimedio. Gran parte della popolazione mondiale ha accesso al web,ed è uno strumento ormai alla portata di tutti e non più privilegio di pochi e ci si augura per il bene della rete Internet che tale protocollo o protocolli simili possano prendere presto piede per una migliore esperienza di navigazione a livello globale. Probabilmente saranno necessari molti anni, ma l’idea che già si pensi ad un futuro non tanto prossimo fa ben sperare su quello che ci aspetta. Nella lettura di questa tesi si vedrà come queste ultime affermazioni possano diventare realtà.

Impiego del GNSS per il monitoraggio in aree sismiche

In questo elaborato si tratterà il metodo di analisi e modellazione post-sismica del terreno attraverso l’utilizzo dei dati GPS e dati SAR. Si prenderanno in esame due eventi sismici: il grande terremoto di Tohoku in Giappone del marzo 2011, con particolare attenzione alla conseguente formazione di un grande tsunami, e la sequenza sismica umbro-marchigiana del settembre/ottobre 1997. In tale contesto verranno descritti i diversi strumenti di monitoraggio e i modelli delle sorgenti sismiche, i quali hanno il compito di determinare importanti informazioni per la più rapida valutazione possibile del rischio sismico e per la corretta pianificazione delle attività umane e del territorio. Obiettivo della tesi è descrivere l’efficacia dell’utilizzo congiunto della tecnica di monitoraggio GPS e l’Interferometria Differenziale SAR. Grazie all’analisi ed alla conseguente modellazione dei dati raccolti nei due eventi sismici descritti in questo lavoro si dimostra l’importanza di tali tecniche per comprendere al meglio i fenomeni sismici. Nel primo capitolo verranno descritte le tecniche di monitoraggio GPS e SAR e le successive tecniche di analisi e modellazione dei dati al fine di avere una previsione dell’evento preso in considerazione. Nel secondo capitolo si esamineranno le peculiarità dell’evento sismico giapponese (2011) e delle elaborazioni condotte per caratterizzare lo tsunami provocato dalla rottura del fondale oceanico. Nel terzo capitolo si analizzerà la sequenza sismica umbro-marchigiana del 1997 prestando attenzione allo sviluppo della rete geodetica del territorio nazionale italiano con riferimenti allo sviluppo della Rete Integrata Nazionale GPS (RING). Nel quarto capitolo verrà descritto in modo introduttivo la struttura del software Bernese GNSS v. 5.2; un software di elaborazione dati usato in ambito scientifico per l’analisi di reti GNSS per il controllo delle deformazioni.

Sviluppo di metodologie per la generazione automatica di calibrazioni di guidabilità motore e cambio

Il presente progetto ha riguardato lo studio e lo sviluppo di metodologie per la generazione automatica di calibrazioni di guidabilità motore cambio, dove con guidabilità si intende il legame intercorrente tra le richieste del conducente ed il reale comportamento del veicolo. La prima parte della tesi si è concentrata sullo studio delle calibrazioni motore e delle calibrazioni del cambio automatico attualmente sfruttate dai software di produzione, sviluppando un modello di simulazione in grado di verificare come queste calibrazioni influenzino il comportamento del veicolo, concentrandosi sugli andamenti delle accelerazioni e dei regimi motore risultanti. Dopo la validazione del modello, è stato creato uno strumento, in ambiente Matlab, che restituisce la calibrazione di guidabilità del cambio automatico, ovvero la mappa sfruttata dalla relativa centralina per gestire il cambio della marcia, ricevendo in ingresso le seguenti informazioni: le grandezze fisiche del veicolo nel suo complesso, quali la massa, i rapporti di trasmissione, il rapporto del differenziale, il raggio di rotolamento dinamico e tutte le inerzie dei componenti della driveline; le calibrazioni di guidabilità motore, costituite da otto mappe, una per ogni marcia, che definiscono la coppia motrice che si richiede al motore di erogare, in funzione della posizione del pedale acceleratore e del regime motore; il piano quotato del motore. Il codice, note queste informazioni, genera automaticamente la mappa di cambio marcia con le linee di Upshift (marcia innestata crescente) e Downshift (marcia innestata decrescente), in funzione della posizione del pedale e dei giri in uscita dal cambio. Infine, si è valutata una possibile strategia per la calibrazione delle otto mappe pedale con cui viene gestito il controllo motore. Si sono generate mappe a potenza costante in cui il pedale assume la funzione di regolatore di velocità.

La Strategia Competitiva basata sulla Leadership di costo nei mercati dei beni durevoli

L'elaborato tratterà, in linea teorica e successivamente con un esempio pratico, il tema della strategia di costo basata sulla leadership di costo. La prima parte vedrà partirà da una linea ampia, al fine di chiarire al meglio cosa sia una strategia aziendale e come essa vada implementata,si restringerà poi andandosi a focalizzare con particolare attenzione su come applicare tale strategia nei mercati di beni durevoli, beni il cui consumo viene ripetuto nel tempo. L'analisi vedrà in particolare, li strumenti, i metodi aziendali e la filosofia per far si che tale strategia diventi più che competitiva nei mercati individuati. Si analizzerà inoltre brevemente il caso di Ikea, leader mondiale della produzione e distribuzione di mobili, la quale ha posto il suo modello di business proprio sulla Leadership di costo. La seconda parte vedrà un caso pratico: come tale strategia è stata implementata e utilizzata nel contesto del business game, una simulazione di un mercato proprio di beni durevoli, lavatrici e asciugabiancherie. L'analisi verterà sulla squadra Freedinelli che ha conseguito buoni risultati attraverso tale strategia. Infine verranno tratte delle conclusioni sulla convenienza ad utilizzare tale strategia, in quali casi sia più conveniente farlo e come farlo al meglio.

Modelli e metodi per il dimensionamento di buffer floor-storage in magazzini scaffalati.

In questa tesi sono stati studiati i fattori che influenzano l'utilizzo del buffer in un magazzino manuale. Per poter realizzare le analisi è stato realizzato un programma C# che simula la gestione del magazzino. Per ottimizzare l'assegnamento dei pallet alle location si è inoltre costruito un modello AMPL. L'obiettivo del modello è minimizzare la differenza tra le classi ottime dei codici in ingresso e i posti pallet ai quali questi vengono assegnati. Il programma C# oltre all'interfaccia con il risolutore AMPL Gurobi, deve interfacciarsi anche con il data base Access nel quale sono stati organizzati i dati necessari per l'analisi. Questi dati sono reali e relativi agli ingressi e alle uscite di un magazzino contenente materiale farmaceutico di due settimane di lavoro. Per facilitare e velocizzare lo studio le informazioni considerate sono quelle di due soli corridoi e non dell'intero magazzino. I risultati hanno evidenziato quattro fattori principali che influenzano la differenza tra un l'allocazione dei pallet in ingresso ad un magazzino. Questi elementi sono: costo di utilizzo del buffer, numero di location libere ad inizio simulazione, momento d'esecuzione del picking a magazzino e tipologia di location vute ad inizio della simulazione. Per ognuno di questi si è cercato, per quanto possibile, di individuare le implicazioni che quanto studiato può avere nella progettazione di un sistema di stoccaggio reale sia dal punto di vista logistico sia dal punto di vista economico. Non sempre le osservazioni reali alle quali si è arrivati hanno un risvolto pratico immediato, ma senza dubbio possono essere utili nello studio preliminare per la realizzazione di un sistema di stoccaggio. All'interno delle conclusioni sono state inserite anche possibili studi e approfondimenti futuri che possono essere eseguiti partendo dal progetto di tesi qui presentato.

la fabbrica automatica e i sistemi di controllo integrati

Lo scopo della presente tesi è quello di illustrare alcuni dei principali strumenti messi a disposizione dai controlli automatici a servizio dell’ingegneria, in particolare analizzando la struttura generale di una fabbrica automatica e descrivendone i principali sistemi di controllo. L’elaborato è suddiviso in tre macro parti: la prima ha l’obiettivo di inquadrare quella che è la fabbrica automatica, partendo dal precedente concetto di fabbrica tradizionale fino ad arrivare alla fabbrica moderna, caratterizzata da una spinta flessibilità produttiva determinata da una politica di produzione per lotti con elevati livelli di caratterizzazione. Della fabbrica automatica viene poi approfondita l’integrazione con i calcolatori attraverso il sistema concettuale del CIM, Computer Integrated Manufacturing, e l’impiego di celle di fabbricazione flessibili, ovvero le FMS, Flexible Manufacturing System. La seconda parte è incentrata sull’analisi delle logiche di controllo impiegate all’interno di tutto il processo di progettazione e di produzione, suddivise in tre gruppi: il primo focalizzato sui sistemi per la produzione automatica, NC e DNC; il secondo sui sistemi di simulazione e testing del prodotto, CAD, CAM e CAT; il terzo sui sistemi di controllo e sviluppo dati, SCADA, MES e DCS. La terza ed ultima parte è circoscritta all’approfondimento di un particolare sistema di controllo per la gestione dei processi, ovvero sull’uso del PLC, il Controllore Logico Programmabile. Vengono analizzate le componenti fisiche che lo costituiscono, il funzionamento base, i tempi di esecuzione delle istruzioni, i criteri di scelta e di dimensionamento ed altri aspetti rilevanti. Infine è presente un esempio applicativo di alcuni aspetti sovra citati con il caso dell’azienda bolognese G.D, leader del settore delle macchine automatiche a controllo numerico per la fabbricazione e l’impacchettamento delle sigarette.

L'innovazione come fattore competitivo: il caso degli elettrodomestici bianchi

La maggior parte dei mercati sono ormai caratterizzati da una elevata incertezza e da una bassa stabilità per quanto riguarda sia il progresso tecnologico che i bisogni e le richieste dei clienti; l’unica arma che le aziende possiedono per fare fronte alla mutabilità intrinseca dei contesti in cui operano è il continuo rinnovo dei prodotti e dei processi. Possiamo vedere l’innovazione, all’interno di un contesto aziendale, come il risultato di diversi fattori: l’evoluzione delle opportunità tecnologiche di prodotto e di processo, i nuovi modelli di impresa, i nuovi valori che si affermano nella società, i nuovi bisogni dei mercati. La prima parte di questa tesi è incentrata sulla descrizione della natura dell’innovazione, delle sue diverse applicazioni all’interno di un contesto aziendale e delle logiche di funzionamento delle aree aziendali preposte alla gestione dei progetti innovativi. Nella seconda parte si entra più nel dettaglio trattando alcuni aspetti distintivi dell’attività innovativa all’interno del mercato degli elettrodomestici ed analizzando uno specifico caso reale. La scelta della focalizzazione sul mercato degli elettrodomestici non è casuale, infatti la terza e ultima parte di questa trattazione è costituita dalla descrizione dell’attività svolta all’interno del Laboratorio di Gestione Aziendale (Business Game) seguito durante il primo semestre di quest’anno e che ha riguardato la simulazione della gestione di un’azienda produttrice di lavatrici e asciugabiancheria.

Studio con HEC-RAS di alcuni interventi per miglioramenti della funzionalità idraulica nel territorio del Consorzio di Bonifica della Romagna

Nel lavoro di tesi vengono esposti gli studi svolti su due aree situate nella giurisdizione riminese del Consorzio di Bonifica, riportanti forti problematiche idrauliche nelle reti di scolo: il territorio dei canali Tamagnino e Zonara Masere ed il Rio Gessi. La modellazione dei tratti è avvenuta attraverso i software Hec-Ras ed Hec-Hms, realizzati rispettivamente per l’analisi dei corsi d’acqua nelle pianure alluvionali attraverso la modellazione dell’evoluzione dei livelli e della corrente e per l’analisi dell’idrologia delle superfici di bacino. Il primo studio è dovuto a problematiche verificatesi fin dal 2014 causate da una variazione d’uso del suolo, il secondo studio è dovuto a dissesti idraulici iniziati nel 2013 causati alla presenza di un tombinamento che provoca l’ostruzione del tratto verso valle. Si esegue la modellazione dello stato di fatto per identificare le sezioni ed i manufatti problematici, in secondo luogo si realizzano le modellazioni delle ipotesi di progetto. Si definiscono infine le soluzioni praticabili e la spesa ipotizzata a seguito della realizzazione di un computo metrico estimativo.

Analisi di un impianto solare termico a circolazione forzata per la produzione di acqua calda sanitaria in un condominio

Il presente elaborato propone un’analisi in regime dinamico mediante il software di simulazione TRNSYS di un impianto solare termico per la produzione di acqua calda sanitaria istallato in un condominio a Bologna. Le simulazioni rappresentano una particolare tipologia di esperimento numerico e possono fornire lo stesso tipo di informazioni sulle performance termiche dei comuni esperimenti fisici. Esse possono valutare gli effetti delle variabili di progetto sulle performance del sistema attraverso una serie di esperimenti, eseguiti tutti in identiche condizioni metereologiche e di carico. Le variabili di progetto esaminate in questo documento mediante simulazione sono l’inclinazione e orientamento del collettore, la superficie captante totale istallata, il volume di accumulo e la portata massima del circuito solare. Le analisi esposte sono un esempio dei risultati che un approccio simulativo può garantire; nel nostro caso, in particolare, le simulazioni hanno confermato la bontà dei criteri di dimensionamento degli impianti solari termici che è possibile incontrare in letteratura. Il presente elaborato si propone inoltre di discutere i benefici, ambientali ed economici, legati all’investimento proposto. L’analisi economica, in particolare, è stata eseguita a seconda dell’impianto tradizionale da affiancare, del diverso costo dell’impianto, di differenti valori di superficie captante e considerando o meno gli incentivi fiscali offerti: per questa valutazione è stato nuovamente necessario l’ausilio del software di simulazione.

Analisi in regime dinamico dei consumi energetici per la produzione di acqua calda sanitaria in una palestra con integrazione di pannelli solari

L'elaborato è focalizzato sul dimensionamento di un sistema solare termico da integrare ad una caldaia a metano in una palestra di riferimento. Sono state condotte simulazioni dinamiche in ambiente Trnsys per analizzare il consumo energetico dell'utenza termica, eseguite anche al variare dei valori di differenti variabili. Infine sono state condotte valutazioni economiche, tramite parametri finanziari, per decretare la fattibilità e la convenienza dell'investimento.

Modellazione del ciclo termico di un impianto di termovalorizzazione dei rifiuti

Breve analisi sulla gestione dei rifiuti e simulazione del ciclo termico del termovalorizzatore del Frullo (gruppo Hera, Bologna), con modellazione di due possibili variazioni operative (dettate dal gestore dell'impianto), per valutare la loro fattibilità in termini di miglioramento dell'efficienza elettrica e termica. Conferma dei risultati ottenuti mediante un'analisi economica basata sulla vendita stagionale dell'energia elettrica e termica.