Referințe Bibliografice

• Slides
• Dafny Reference Manual
• Dafny Tutorial

Plan de lucru

Week 1 - Programare Funcțională în Dafny (1)

• Lecture #1
• Exercise Sheet (PDF)
• Bibliography: Dafny Tutorial

Week 2 - Programare Funcțională în Dafny (2)

• Lecture #2 (Part A - Sequences)
• Lecture #2 (Part B - Sets)
• Lecture #2 (Part C - Multisets)
• Lecture #2 (Part D - Maps)
• Lecture #2 (Part E - ADTs)
• Exercise Sheet (PDF)

Week 3 - Programare Imperativă în Dafny

• Lecture #3 (Part A)
• Lecture #3 (Part B)
• Exercise Sheet (PDF)

Week 4 - Programare Orientată Obiect în Dafny

• Lecture #4 (Part A - Basics)
• Lecture #4 (Part B - Class Invariants)
• Lecture #4 (Part C - Linked List)
• Lecture #4 (Part D - traits)
• Exercise Sheet (PDF)

Week 5 - Propoziții Logice

• Lecture #5
• Exercise Sheet (PDF)

Week 6 - Demonstrații (1)

• Lecture #6
• Exercise Sheet (.dfy)

Week 7 - Demonstrații (2)

• Lecture #7
• Exercise Sheet: fill in previous work sheets

Week 8

Week 9 - Verificarea Extrinsecă a Programelor Funcționale

• Lecture #9
• Exercise Sheet, part I (.dfy, roughly 30 minutes)
• Exercise Sheet, part II: work on project

Week 10 - Verificarea Intrinsecă a Programelor Funcționale

• Lecture #10
• Exercise Sheet, part I (.dfy, roughly 15 minutes)
• Exercise Sheet, part II: work on project

Week 11 - Verificarea Programelor Imperative

• Lecture #11
• Exercise Sheet: work on project

Week 12 - Verificarea Programelor Orientate Obiect (1)

• Exercise Sheet: work on project

Week 13 - Verificarea Programelor Orientate Obiect (2)

• Exercise Sheet: work on project

Week 14 - Exemplu Complet de Verificare a unui Sistem (1)

• Exercise Sheet: work on project