Scheda programma d'esame
PRINCIPLES FOR SOFTWARE COMPOSITION
(COMPUTATIONAL MODELS)
ROBERTO BRUNI
Anno accademico2023/24
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 e/o progetti software individuali.

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

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 and/or individual software projects.

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

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à

Il corso comprende test di auto-valutazione e/o progetti software individuali.

L'esame orale verte principalmente sulle definizioni e sulle proprietà mostrate nel corso, incluse le dimostrazioni dei risultati principali e può includere lo svolgimento di esercizi analoghi a quelli visti a lezione.

Assessment criteria of skills

The course includes self-assessment tests and/or individual software projects.

The oral exam focuses on the definitions and properties presented in the course and can include written exercises analogous to the ones presented during classrooms.

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

Test di auto-valutazione e/o progetti software individuali.

Assessment criteria of behaviors

Written and oral exam.

Self-assessment tests and/or individual software projects.

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

Il corso comprende test di auto-valutazione e/o progetti software individuali.

L'esame orale verte principalmente sulle definizioni e sulle proprietà mostrate nel corso, incluse le dimostrazioni dei risultati principali e può includere lo svolgimento di esercizi analoghi a quelli visti a lezione.

Assessment methods

The course includes self-assessment tests and/or individual software projects.

The oral exam focuses on the definitions and properties presented in the course and can include written exercises analogous to the ones presented during classrooms.

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/
Note

Nessuna

Notes

None

Ultimo aggiornamento 31/07/2023 10:18