Some of the materials are behind a password. Ask the instructor for one.
| Date |
Topic |
Material |
Reading |
| Tue 22.8 |
Introduction |
intro-slides ms-talk.pptx parnas |
|
| Wed 23.8 |
no class |
|
|
| Tue 29.8 |
Preliminaries |
magnolia-intro-slides |
Appendix A. |
| Wed 30.8 |
Signatures, Algebras |
|
Sections 2.1–2.3 |
| Tue 5.9 |
Getting started with Magnolia |
|
|
| Wed 6.9 |
Getting started with Magnolia |
|
Tutorials 1–3 |
| Tue 12.9 |
Homomorphisms, Satisfaction |
|
Section 2.4 |
| Wed 13.9 |
Logics for Axioms (EL, CEL) |
|
Section 2.6, Tutorial 5 |
| Tue 19.9 |
Discussing assignment 3 |
|
|
| Wed 20.9 08:30 |
Logics for Axioms (QFPL, PL), reuse of specifications |
|
Sections 2.6.2, 2.7.1 |
| Tue 26.9 08:30 |
Renaming specifications; Software Institutions |
|
Section 2.7.2, 2.8 |
| Wed 27.9 |
no class |
|
|
| Fri 29.9 12:15 |
Relating theory to Magnolia |
Example program Fib.mg |
Section 3.1, 3.2 |
| Tue 3.10 |
Domain engineering in Magnolia |
|
Chapter 6 |
| Wed 4.10 |
Domain engineering in Magnolia |
|
|
| Tue 10.10 |
Generic programs and testing |
Multiarrays paper |
|
| Wed 11.10 |
Loops in Magnolia; About the graph domain |
FibLoop.mg BGL |
|
| Fri 20.10 |
Graph concepts and algorithms in Magnolia |
|
|
| Tue 24.10 |
no class, work on assignment 6 |
|
|
| Wed 25.10 |
no class, work on assignment 6 |
|
|
| Tue 31.10 |
Program verification |
verification |
|
| Wed 1.11 |
A6 discussion; Introduction to Dafny |
dafny tutorial-examples.dfy |
|
| Tue 7.11 |
Loop invariants, arrays, quantifiers |
array-searches.dfy |
|
| Wed 8.11 |
Guiding verification with lemmas, misc. features |
rus.dfy reverse.dfy simple.dfy |
|
| Tue 14.11 |
Verifying OO programs |
Section 8 here counters.dfy |
|
| Wed 15.11 |
Pre/post and class invariants and Inheritance, glance at SMT solvers |
|
|
| Tue 21.11 |
Review for exam |
|
|
| Wed 22.11 |
no class |
|
|
| Mon 27.11 |
EXAM |
|
|
| Tue 28.11 |
|
|
|
| Wed 29.11 |
|
|
|