Questo insegnamento ha lo scopo di introdurre lo studente ai principi e fondamenti dei linguaggi di programmazione, al fine di comprenderne la struttura ed interpretare correttamente il comportamento dei programmi. In primo luogo questo obiettivo viene perseguito attraverso lo studio della teoria dei linguaggi formali, i relativi strumenti di definizione della sintassi (tramite grammatiche e automi), e la formalizzazione della loro semantica. In secondo luogo, nel contesto di tali strumenti formali, vengono affrontate alcune tecniche per modellare sistemi software complessi e verificarne le relative proprietà attraverso l'uso di metodologie basate su automi e logiche.

01. Fondamenti dei linguaggi di programmazione:
      01.01 Teoria dei linguaggi formali.
      01.02 Classificazione di Chomsky delle grammatiche a struttura di frase. 
      01.03 Teoria degli automi e delle macchine di Turing.
      01.04 Calcolabilità.

02. 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.

03. Linguaggi regolari:
      03.01 Relazione tra automi a stati finiti e grammatiche lineari destre.
      03.02 Proprietà dei linguaggi regolari e pumping lemma.
      03.03 Espressioni regolari.
      03.04 Relazione tra espressioni regolari e automi a stati finiti.

04. Linguaggi liberi:
      04.01 Grammatiche libere e alberi sintattici.
      04.02 Grammatiche libere in forma normale di Chomsky.
      04.03 Proprietà dei linguaggi liberi e pumping lemma.

05.  Automi a pila e parsing:
      05.01 Automi a pila e relazione con grammatiche libere.
      05.02 Parsing top-down.
      05.03 Grammatiche LL(1).
      05.04 Parsing bottom-up.
      05.05 Grammatiche SLR, LR(1), LALR(1).

06. Semantica denotazionale:
      06.01 Semantica denotazionale di programmi sequenziali aciclici.
      06.02 Semantica denotazionale dell'operatore WHILE. 
      06.03 Semantica denotazionale con blocchi e procedure.

07. Semantica operazionale:
      07.01 Semantica operazionale naturale di programmi sequenziali.
      07.02 Semantica operazionale naturale con blocchi e procedure.
      07.03 Semantica operazionale strutturata.

08. Modellazione e verifica di sistemi reattivi:
      08.01 Strutture di Kripke.
      08.02 Logica linear-time.
      08.03 Logica branching-time.
      08.04 Algoritmi di model checking.

09. Attività di laboratorio:
      09.01 Macchine a stati finiti.
      09.02 Modellazione e verifica in NuSMV.
      09.03 Sistemi reattivi complessi in NuSMV.
 

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 e Modellazione a Oggetti, Ingegneria e Architettura del Software, Sistemi Operativi, e di rispettare le propedeuticità relative a questi.

Conoscenze e comprensione: lo studente sarà in grado di capire la struttura sintattica, le regole di compilazione, e la semantica dei più comuni linguaggi di programmazione, nonché i principi metodologici delle tecniche formali di modellazione e verifica di sistemi software illustrati nel programma.

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.

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.

Il materiale didattico predisposto dalla/dal docente in aggiunta ai testi consigliati (come ad esempio diapositive, dispense, esercizi, bibliografia) e le comunicazioni della/del docente specifiche per l'insegnamento sono reperibili all'interno della piattaforma Moodle › blended.uniurb.it

Modalità didattiche

Lezioni teoriche ed esercitazioni guidate in laboratorio.

Didattica innovativa

La modalità didattica in presenza verrà arricchita con esercitazioni di laboratorio basate sul problem solving, individuali e di gruppo.

Obblighi

Sebbene fortemente consigliata, la frequenza non è obbligatoria.

Testi di studio

I due testi alternativi: Hopcroft, Motwani, Ullman, "Automi, Linguaggi e Calcolabilità" (Terza Edizione, Pearson) e Aiello, Pirri, "Strutture, logica, linguaggi" (Pearson) offrono entrambi i contenuti relativi alle sezioni 01-05 del programma del corso. La versione originale del primo testo è Hopcroft, Motwani, Ullman, "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley.

Le sezioni 06 e 07 sono tratte da Nielson, Nielson, "Semantics with Applications: An Appetizer" (Springer). Testo alternativo: Semantica operazionale e denotazionale dei linguaggi di programmazione, di Rocco De Nicola (1999, CittàStudiEdizioni, Torino). 

Gli argomenti della sezione 08 sono coperti da Clarke, Grumberg, Peled, Veith, "Model Checking" (Second Edition, MIT Press). 

La sezione 09 si basa sul software tool NuSMV http://nusmv.fbk.eu/

Modalità di
accertamento

Progetto individuale, prova scritta e prova orale.

Il progetto consiste nella modellazione e verifica di un sistema software tramite il tool NuSMV. 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 matricola e contenente file sorgenti con specifiche e risultati della verifica, ogni parte adeguatamente commentata. 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. Il progetto deve essere presentato e discusso oralmente il giorno della prova scritta. Sono oggetto di valutazione la rispondenza del modello alle specifiche e la varietà di proprietà prese in considerazione. Il progetto si ritiene sufficiente se valutato con il punteggio minimo di 6/10 (il risultato pesa per un terzo del voto complessivo).

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 relativi a grammatiche, automi, e semantica formale (sezioni 01-07 del programma). Appunti e altro materiale sono consultabili. Scopo della prova scritta è la verifica della capacità di applicare le conoscenze acquisite in merito agli argomenti teorici affrontati nel corso. Sono oggetto di valutazione la correttezza della soluzione e dell'approccio alla soluzione degli esercizi, nonché il rigore metodologico. La prova si ritiene sufficiente se superata con il punteggio minimo di 12/20 (il risultato pesa per due terzi del voto complessivo).

L'orale è facoltativo sul programma del corso e comporta un aggiustamento positivo o negativo (di al più 5 punti) sul voto complessivo determinato dalla somma di voto del progetto e voto della prova scritta. 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.

Disabilità e DSA

Le studentesse e gli studenti che hanno registrato la certificazione di disabilità o la certificazione di DSA presso l'Ufficio Inclusione e diritto allo studio, possono chiedere di utilizzare le mappe concettuali (per parole chiave) durante la prova di esame.

A tal fine, è necessario inviare le mappe, due settimane prima dell’appello di esame, alla o al docente del corso, che ne verificherà la coerenza con le indicazioni delle linee guida di ateneo e potrà chiederne la modifica.