Scheda programma d'esame
PRINCIPLES FOR SOFTWARE COMPOSITION
(COMPUTATIONAL MODELS)
ROBERTO BRUNI
Anno accademico2020/21
CdSINFORMATICA
Codice375AA
CFU9
PeriodoSecondo semestre
LinguaInglese

ModuliSettore/iTipoOreDocente/i
MODELLI DI CALCOLOINF/01LEZIONI72
ROBERTO BRUNI unimap
Obiettivi di apprendimento
Learning outcomes
Conoscenze

Gli studenti dovranno acquisire solide basi di conoscenza circa i principi della semantica operazionale e denotazionale, le tecniche per relazionare l'una con l'altra nel caso di linguaggi imperativi e funzionali di ordine superiore. Inoltre dovranno familiarizzare con i principi della semantica operazionale e astratta per algebra di processi concorrenti, con le principali logiche temporali e modali (HM, LTL, CTL*, mu-calculus) usate per esprimere proprietà di tali processi e con modelli operazionali con probabilità. Gli ultimi saranno studiati dal punto di vista degli automi probabilistici e stocastici, delle catene di Markov e dal linguaggio di modellazione PEPA.

 

Knowledge

Students are expected to acquire solid knowledge about the principles of operational semantics, the principles of denotational semantics, and the techniques to relate one to the other for an imperative language and for a higher order functional language. Moreover, they will acquire some knowledge about the operational and observational semantics of two process description languages (CCS and pi-calculus), about temporal and modal logics (HM, LTL, CTL*, mu-calculus) and operational nondeterministic models with discrete probabilities. The latter are presented from the perspective of probabilistic and stochastic automata, and of the PEPA calculus.

Modalità di verifica delle conoscenze

In caso di didattica a distanza, gli esami scritti potranno essere sostituiti da test di auto-valutazione.

L'esame scritto servirà a verificare che gli studenti abbiano compreso il materiale presentato durante il corso e che siano in grado di organizzare e strutturare i concetti appresi in efficaci risposte scritte.

Durante l'esame orale gli studenti dovranno dimostrare di aver compreso gli aspetti più concettuali e di essere in grado di argomentare le risposte con proprietà di linguaggio usando i termini corretti.

Metodi di verifica:

  • Esame orale finale
  • Esame scritto finale
  • Compitini

Informazione aggiuntiva:

La valutazione sarà basata su esami scritti e orale. L'esame scritto finale non sarà necessario se i compitini saranno valutati positivamente.

 

 

 

Assessment criteria of knowledge

In case of virtual lectures, written exams will be replaced by self-assessment tests.

In the written exam the student must demonstrate his/her knowledge of the course material and to organise an effective and correctly written reply. During the oral exam the student must be able to demonstrate his/her knowledge of the course material and be able to discuss the reading matter thoughtfully and with propriety of expression.

Methods:

  • Final oral exam
  • Final written exam
  • Periodic written tests

Further information:
The evaluation will be based on written and oral exams. The written exam is not necessary if the mid-terms exams are evaluated positively.

 

Capacità

Al termine del corso gli studenti dovrebbero essere in grado di dimostrare semplici proprietà formali di linguaggi e sistemi imperativi, dichiarativi, concorrenti e probabilistici. In particolare dovrebbero essere in grado di applicare correttamente i più comuni principi di induzione e la teoria del punto fisso.

 

Skills

At the end of the course the student should be able to state and prove formal properties of imperative, declaratice, concurrent and probabilistic systems. In particular, they should be able to apply several induction principles and fixpoint theory.

Modalità di verifica delle capacità

In caso di didattica a distanza, gli esami scritti potranno essere sostituiti da test di auto-valutazione.

L'esame scritto consiste di esercizi che richiedono l'applicazione di tecniche formali di prova ad alcuni casi specifici accuratamente selezionati.

L'esame orale verte principalmente sulle definizioni e sulle proprietà mostrate nel corso, incluse le dimostrazioni dei risultati principali.

Assessment criteria of skills

In case of virtual lectures, written exams will be replaced by self-assessment tests.

The written exam consists of exercises that require to apply formal analysis techniques to some carefully chosen cases.

The oral exam focuses on the definitions and properties presented in the course.

Comportamenti

Alla fine del corso gli studenti dovrebbero essere in grado di comprendere e applicare sistemi logici e definizioni induttive, di definire la semantica di linguaggi di programmazione, e di ragionare su eventuali equivalenze e corrispondenze tra specifiche astratte.

 

Behaviors

At the end of the course the student should be able to understand logic systems and inductive definitions, to assign semantics to programs, to reason about program equivalence and compliance to abstract specifications. 

Modalità di verifica dei comportamenti

Esame scritto e orale.

 In caso di didattica a distanza, gli esami scritti potranno essere sostituiti da test di auto-valutazione.

Assessment criteria of behaviors

Written and oral exam.

In case of virtual lectures, written exams will be replaced by self-assessment tests.

Prerequisiti (conoscenze iniziali)

Non ci sono prerequisiti stringenti, ma ci si aspetta che gli studenti abbiano una buona familiarità con la matematica discreta, con le formule logiche del prim'ordine, con le grammatiche libere da contesto e siano in grado di comprendere frammenti di codice scritti in linguaggi imperativi e funzionali.

 

Prerequisites

There are no prerequisites, but the students are expected to have some familiarity with discrete mathematics, first-order logic formulas, context-free grammars, and code fragments in imperative and functional style.

Indicazioni metodologiche

Lezioni frontali e esercitazioni collettive.

Attività di apprendimento:

  • partecipazione attiva alle lezioni
  • domande e discussioni col docente
  • assegnamenti di esericizi a fine lezione, da dscutere nella lezione successiva
  • studio individuale e a gruppi

Frequenza: fortemente consigliata

 

Teaching methods

Delivery: face to face

Learning activities:

  • attending lectures
  • participation in discussions
  • home assignments, to be solved together in the next lecture
  • individual study

Attendance: Advised

Teaching methods:

  • Lectures
Programma (contenuti dell'insegnamento)

Introduzione di cinque modelli computazionali differenti e studio delle loro proprietà formali principali (imperativo: IMP, funzionale: HOFL, processi concorrenti: CCS, calcoli con nomi: pi-calculus, sistemi probabilistici e stocastici: Segala automata e PEPA) accompagnati da principi di induzione e da metodi di dimostrazione.

Syllabus

The introduction of five different computational models (imperative: IMP, functional: HOFL, processes: CCS, nominal: pi-calculus, probabilistic and stochastic: Segala automata and PEPA) together with induction principles and formal proof methods.

Bibliografia e materiale didattico

Testo principale:

Letture opzionali consigliate:

Bibliography

Main text:

Other readings:

Indicazioni per non frequentanti

Nessuna variazione.

Non-attending students info

No variation.

Modalità d'esame

In caso di didattica a distanza, gli esami scritti potranno essere sostituiti da test di auto-valutazione.

Esame scritto (due compitini o un esame finale) e esame orale.

L'esame scritto consiste di una serie di esercizi da risolvere in 2 ore. Ogni esercizio ha un punteggio assegnato e il voto finale è la somma dei punteggi conseguiti sui singoli esercizi. I testi delle sessioni di esame precedenti sono raggiungibili dalla pagina del corso.

L'esame orale prende spunto dalla discussione dell'esame scritto per poi affrontare gli argomenti principali presentati durante il corso. La durata tipica dell'esame orale è 30'/40'.

Avviso:

A causa dell'emergenza COVID-19, a partire dall'appello di giugno 2020 e fino a nuovo avviso le modalità di esame vengono modificate nella sola prova orale, in modo da permette agli studenti di sostenere l'esame a distanza.

 

 

Assessment methods

In case of virtual lectures, written exams will be replaced by self-assessment tests.

Written (two mid-term, or one regular) exam and oral exam.

The written exam consists of a series of exercises to be solved in 2 hours. Each exercise is assigned some score and the overal score is the sum of scores for each exercise. The texts of exams from previous sessions and academic years are linked from the web page of the course.

The oral exam can involve the discussion of the written exam as well as questions about the main topics of the course topics. The average duration of the oral exam is 30'/40' 

 
Notice:

Due to the COVID-19 countermeasures, for the current period, the evaluation will be solely based on oral exams.

 

Altri riferimenti web

Alcuni strumenti presentati nel corso:

  • Haskell, https://www.haskell.org/
  • Erlang, http://www.erlang.org/
  • Google Go, http://golang.org/
  • CAAL, http://caal.cs.aau.dk/
  • PEPA http://www.dcs.ed.ac.uk/pepa/
Additional web pages

Some teaching tools overviewed in the course are:

  • Haskell, https://www.haskell.org/
  • Erlang, http://www.erlang.org/
  • Google Go, http://golang.org/
  • CAAL, http://caal.cs.aau.dk/
  • PEPA http://www.dcs.ed.ac.uk/pepa/
Notes

None

Ultimo aggiornamento 03/08/2020 10:50