Scheda programma d'esame
LOGICA PER LA PROGRAMMAZIONE
ANDREA CORRADINI
Anno accademico2018/19
CdSINFORMATICA
Codice009AA
CFU6
PeriodoPrimo semestre
LinguaItaliano

ModuliSettore/iTipoOreDocente/i
LOGICA PER LA PROGRAMMAZIONEINF/01LEZIONI48
ANDREA CORRADINI unimap
RICCARDO GUIDOTTI unimap
Obiettivi di apprendimento
Learning outcomes
Conoscenze

L'obiettivo del corso è introdurre gli elementi di base della logica matematica e il suo uso per analizzare la correttezza di semplici programmi. Gli studenti impareranno a conoscere il calcolo proposizionale e la logica del primo ordine, e il loro utilizzo nella formalizzazione di enunciati dichiarativi in linguaggio naturale. Inoltre saranno in grado di utilizzare alcune tecniche formali di dimostrazione e di applicarle alla verifica di semplici programmi imperativi attraverso le triple di Hoare.

Knowledge

The goal of the course is to introduce the basic elements of Mathematical Logic and its use to analyse the correctness of simple programs. The students will become familiar with the Propositional Calculus and First Order Logic, and their use in formalizing natural language statements. They will also be able to use some formal proof techniques and to apply them to the verification of simple imperative programs via Hoare's triples.

Modalità di verifica delle conoscenze

La prova scritta ha l'obiettivo di accertare che lo studente abbia acquisito sufficiente familiarità nella dimostrazione di validità di formule, nella formalizzazione di enunciati e nella verifica di triple di Hoare. Con la prova orale si verificherà che lo studente abbia assimilato in modo critico i concetti introdotti nel corso.

Assessment criteria of knowledge

The written test aims to ensure that the student has acquired sufficient familiarity with the proof of validity of formulas, formalization of statements, and verification of Hoare's triples. The oral exam will assess that the student has critically assimilated the concepts introduced in the course.

Capacità

Al termine del corso lo studente avra' consapevolezza dell'importanza di descrivere formalmente le proprieta' desiderate dei programmi e piu' in generale dell'importanza delle logiche per l'informatica. Sara' inoltre in grado di individuare e gestire casi di ambiguita' nella specifica di un programma.

Skills

At the end of the course the student will be aware of the importance of describing formally the desired properties of programs, and more generally the importance of logics for computer science. It will also be able to detect and manage cases of ambiguity in the specification of a program.

Modalità di verifica delle capacità

L'accertamento delle capacita' avviene tramite colloquio nell'esame finale del corso.

Assessment criteria of skills

Colloquium with the lecturer in the final oral exam.

Indicazioni metodologiche
  • La frequenza e' fortemente consigliata.
  • Le lezioni frontali si svolgono con uso di slide e della lavagna.
  • Le esercitazioni si svolgono in aula: gli studenti svolgono degli esercizi, anche in gruppo, sotto la supervisione del docente.
  • L'interazione con il docente avviene con colloqui (in orario di ricevimento o su appuntamento) e tramite posta elettronica.
  • Sulla pagina web del corso vengono pubblicati progressivamente i lucidi presentati in ogni lezione, con riferimenti ai corrispondenti argomenti nei libri di testo. Vengono anche pubblicati i testi degli esercizi proposti per le esercitazioni.
  • Il materiale didattico e alcuni esempi di testi di esame sono accessibile sulla pagina web del corso.
  • Il corso prevede due prove intermedie il cui superamento esonera lo studente dalla prova scritta di esame.
Teaching methods
  • Attendence is strongly advised.
  • Frontal lessons are performed using slides and blackboard.
  • Exercises take place in the classroom: students practice exercises, even in groups, under the supervision of the lecturer.
  • Interaction with the teacher is done through interviews (on fixed office hours or by appointment) and by e-mail.
  • On the web page of the course, the slides presented in each lesson are published progressively, with references to corresponding topics in the textbooks. The texts of the exercises proposed for the exercises are also published.
  • The teaching material and some examples of exam texts are accessible on the course web page.
  • The course provides two intermediate tests, the passing of which exempts the student from the written exam.
Programma (contenuti dell'insegnamento)
  1. Introduzione alla logica matematica e sua rilevanza per la programmazione
  2. Calcolo proposizionale e tecniche di dimostrazione
  3. Calcolo dei predicati del primo ordine
  4. Formalizzazione di asserzioni in linguaggio naturale
  5. Intervalli di numeri e relativi connettivi
  6. Triple di Hoare per un sottoinsieme del linguaggio C
Syllabus
  1. Introduction to Mathematical Logic and its relevance to programming
  2. Propositional Calculus and proof techniques
  3. First Order Predicate Calculus
  4. Formalizing natural language assertions
  5. Number ranges and related connectives
  6. Hoare's triples for a subset of the C language
Bibliografia e materiale didattico

Slides presentate durante le lezioni e dispense scaricabili dalla pagina web del corso

Bibliography

Slides presented during the lectures and lecture notes downloadable from the course's web page

Indicazioni per non frequentanti

Gli studenti non frequentanti possono trovare sulla pagina web del corso l'elenco degli argomenti presentati per ogni singola lezione, con le slide proiettate e i riferimenti al materiale didattico rilevante. Le modalita' d'esame per gli studenti non frequentanti sono identiche a quelle per gli studenti frequentanti.

Non-attending students info

Non-attending students can find on the course web page the list of topics presented for each lesson, with the projected slides and references to the relevant teaching material. Examination methods for non-attending students are identical to those for attending students.

Modalità d'esame

L'esame è composto da una prova scritta ed una prova orale. Il superamento di due prove in itinere equivale al superamento della prova scritta.
La prova scritta consiste in piú problemi da risolvere in circa due ore. Se superata, la prova rimane valida per tutti gli appelli della sessione di esami in corso.
La prova orale consiste in un colloquio tra il candidato e il docente, della durata di circa quaranta minuti.

Assessment methods

The exam consists of a written test and an oral exam. Passing the two mid-term exams is equivalent to passing the written test.
The written test consists of a few problems to be solved in about two hours. If passed, the test remains valid for the ongoing exam session.
The oral test consists of an interview between the candidate and the lecturer, which lasts approximately fourty minutes.

Ultimo aggiornamento 09/01/2019 20:44