INF/01

Curriculum: PERCORSO COMUNE

A.A.
CFU Durata (ore)
Periodo Sede
2017/2018 12 96 Ciclo Annuale Unico URBINO

Didattica in lingua straniera
Insegnamento con materiali opzionali in lingua straniera: Inglese

* La didattica è svolta interamente in lingua italiana. I materiali di studio e l'esame possono essere in lingua straniera.

Assegnato ai Corsi di Studio

Docente


Alessandro Aldini

alessandro.aldini@uniurb.it

Obiettivi Formativi
Questo insegnamento ha lo scopo di introdurre la teoria dei linguaggi formali e di illustrare tecniche per modellare l'architettura di sistemi software complessi e verificarne le relative proprietà attraverso l'uso di metodi formali basati su automi, algebre, e logiche. In secondo luogo, ha l'obiettivo di presentare il paradigma di programmazione funzionale attraverso lo studio del linguaggio Haskell.

Programma
01. Introduzione alla modellazione e verifica:
      01.01 L'esigenza di metodi formali nello sviluppo del software.
      01.02 Linguaggi formali ed automi.
      01.03 Grammatiche a struttura di frase e classificazione di Chomsky.
      01.04 Approcci formali alla semantica dei linguaggi.
      01.05 Teoria della concorrenza, logiche ed algebre.

02. Linguaggi regolari e automi a stati finiti:
      02.01 Automi a stati finiti deterministici.
      02.02 Automi a stati finiti non deterministici.
      02.03 Automi a stati finiti con ε-transizioni.
      02.04 Minimizzazione ed equivalenza per automi a stati finiti.
      02.05 Relazione tra automi a stati finiti e grammatiche lineari destre.
      02.06 Proprietà dei linguaggi regolari e pumping lemma.
      02.07 Espressioni regolari.
      02.08 Relazione tra espressioni regolari e automi a stati finiti.

03. Linguaggi liberi e automi a pila:
      03.01 Grammatiche libere e alberi sintattici.
      03.02 Grammatiche libere in forma normale di Chomsky.
      03.03 Proprietà dei linguaggi liberi e pumping lemma.
      03.04 Automi a pila e relazione con grammatiche libere.
      03.05 Parsing top-down.
      03.06 Parsing bottom-up.

04. Semantica denotazionale:
      04.01 Semantica denotazionale di un linguaggio imperativo.
      04.02 Semantica denotazionale con blocchi e procedure.

05. Semantica operazionale:
      05.01 Semantica operazionale naturale di un linguaggio imperativo.
      05.02 Semantica operazionale naturale con blocchi e procedure.
      05.03 Semantica operazionale strutturata di un linguaggio imperativo.

06. Logiche temporali e model checking:
      06.01 Modelli di Kripke.
      06.02 Logiche temporali.
      06.03 Logiche linear-time vs. logiche branching-time.
      06.04 Algoritmi di model checking.

07. Algebre di processi ed equivalenze comportamentali:
      07.01 Concorrenza e nondeterminismo.
      07.02 Sintassi e semantica di operatori comportamentali.
      07.03 Equivalenza basata su tracce.
      07.04 Equivalenza basata su bisimulazione.

08. Linguaggi per la descrizione di architetture software:
      08.01 Componenti, connettori e stili architetturali.
      08.02 Sintassi di un linguaggio architetturale basato su algebra di processi.
      08.03 Semantica di un linguaggio architetturale basato su algebra di processi.09. Programmazione funzionale in Haskell:
      09.01 Introduzione al linguaggio Haskell.
      09.02 Funzioni, ricorsione, polimorfismo.
      09.03 Strutture complesse e funzioni di ordine superiore.
      09.04 Definizione di tipi di dato: alias di tipo e tipi algebrici.10. Attività di laboratorio:
      10.01 Modellazione di sistemi tramite strutture di Kripke.
      10.02 Model checking di sistemi descritti tramite strutture di Kripke.
      10.03 Esercizi in Haskell.
 

Eventuali Propedeuticità
Non vi sono propedeuticità obbligatorie.
 
Si suggerisce di sostenere l'esame di Linguaggi di Programmazione e Verifica del Software dopo aver sostenuto gli esami di Programmazione Procedurale e Logica, Architettura degli Elaboratori, Matematica Discreta.

Risultati di Apprendimento (Descrittori di Dublino)
Conoscenze e comprensione: lo studente sarà in grado di capire la semantica dei più comuni linguaggi di programmazione e i principi metodologici delle tecniche formali di modellazione e verifica di sistemi software illustrati nel programma; sarà inoltre in grado di applicare i principi della programmazione funzionale nel caso specifico del linguaggio Haskell.Capacità di applicare conoscenze e comprensione: lo studente sarà in grado di progettare i moduli base dei compilatori per linguaggi di programmazione e di modellare e verificare formalmente sistemi software tramite gli strumenti presentati a lezione; sarà inoltre in grado di sviluppare piccoli programmi funzionali in Haskell.Autonomia di giudizio: lo studente sarà in grado di valutare la correttezza di sintassi e semantica di qualunque linguaggio di programmazione e di rappresentare e confrontare formalmente le diverse specifiche di un sistema software in corso di progettazione e sviluppo.Abilità comunicative: lo studente sarà in grado di illustrare in modo appropriato le caratteristiche semantiche dei linguaggi di programmazione e di descrivere, in modo formale, le funzionalità e le proprietà di un sistema software tramite gli strumenti di modellazione e verifica utilizzati a lezione.Capacità di apprendimento: lo studente apprenderà la capacità di descrivere formalmente sintassi e semantica di linguaggi di programmazione e di modellare e verificare sistemi software; sarà inoltre in grado di capire e usare gli strumenti di programmazione funzionale messi a disposizione dai linguaggi di programmazione moderni.

Modalità Didattiche, Obblighi di Frequenza, Testi di Studio e Modalità di Accertamento
Modalità Didattiche
Lezioni teoriche ed esercitazioni guidate in laboratorio.
Obblighi di Frequenza
Sebbene fortemente consigliata, la frequenza non è obbligatoria.
Testi di Studio
Hopcroft, Motwani, Ullman, "Automi, Linguaggi e Calcolabilità", Addison-Wesley, 2009Hopcroft, Motwani, Ullman, "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley, 2007).Nielson, Nielson, "Semantics with Applications: An Appetizer", Springer, 2007Clarke, Grumberg, Peled, "Model Checking", MIT Press, 1999Aldini, Bernardo, Corradini, "A Process Algebraic Approach to Software Architecture Design", Springer, 2010
Modalità di Accertamento
Progetto individuale, prova scritta e prova orale.Il progetto consiste nella modellazione e verifica di un sistema software. Il testo del progetto, uno per sessione e uguale per tutti, è pubblicato almeno un mese prima dell'inizio di ogni sessione, con consegna entro le ore 12.00 di due giorni prima della prova scritta che si vuole sostenere. Il progetto, anche se superato, vale solo per la sessione cui viene associato. Il testo è dato dalla specifica di un sistema reale da modellare e verificare. Sono a libera scelta il livello di astrazione del modello, le varianti e configurazioni sotto analisi, e le proprietà da verificare. La consegna avviene tramite email con subject LPVS: consegna progetto nome_cognome e contenente file sorgenti con specifiche e risultati della verifica, ogni parte adeguatamente commentata. Il risultato pesa per un terzo del voto complessivo. Scopo del progetto è la verifica della capacità di autonomia dello studente nell'impiego pratico delle competenze acquisite in ambito di modellazione e verifica del sofware.La prova scritta può essere sostenuta solo dopo la consegna del progetto della stessa sessione. Ha una durata di 90 minuti e consiste di esercizi pratici. Appunti e materiale sono consultabili. Il risultato pesa per due terzi del voto complessivo. Nella sessione invernale è prevista una prova scritta parziale da integrare con una seconda prova parziale entro la sessione estiva. In questo caso le due prove sono associate al progetto della sessione estiva. Scopo della prova scritta è la verifica della capacità di comprensione in merito agli argomenti teorici affrontati nel corso e la verifica delle abilità di uso del paradigma funzionale.L'orale è obbligatorio sul progetto e facoltativo sul programma del corso. L'orale facoltativo comporta un aggiustamento positivo o negativo (di al più 5 punti) sul voto complessivo. Scopo dell'orale è la valutazione di autonomia di giudizio, abilità comunicative e livello di comprensione della materia.Per testi di progetti e compiti d'esame visitare questo link.

Note
 L'insegnamento è erogato anche on-line all'interno della piattaforma Moodle > elearning.uniurb.it