- poniedziałki, 12-14 s. 5440
Warunki zaliczenia i egzaminu:
Prace domowe: Zaliczenie ćwiczeń i dopuszczenie do egzaminu odbędzie się na podstawie prac domowych. Będą trzy prace domowe, każde złożone z jednego zadania, oceniane na skali 0-1. Zadania będą wspólne dla wszystkich grup, ale sprawdzane i omawiane przez prowadzących poszczególne grupy ćwiczeniowe.
Do zaliczenia ćwiczeń i dopuszczenia do pierwszego terminu egzaminu niezbędne jest uzyskanie nie mniej niz 1.8 punktu z trzech prac domowych razem.
- Pierwsza praca domowa: rozwiązania proszę nadsyłać do niedzieli 26 listopada. Odpowiedzi na często zadawane pytania można znaleźć tutaj.
- Druga praca domowa: rozwiązania proszę nadsyłać do niedzieli 7 stycznia.
- Trzecia praca domowa i jej wersja tekstowa do ewentualnego wykorzystania w pracy z systemem HAHA. Rozwiązania proszę nadsyłać do soboty 27 stycznia. Użycie systemu HAHA nie jest obowiązkowe, ale może pomóc w uniknięciu wielu pomyłek, więc zachęcam do skorzystania z niego.
Egzamin: Oto treści pierwszego i drugiego zadania egzaminacyjnego z pierwszego terminu.
Slajdy do wykładu
- 2 października: Wprowadzenie i sprawy organizacyjne
- 9 października: Język TINY i semantyka operacyjna małych kroków
- 16 października: Semantyka operacyjna dużych kroków. Równoważność semantyczna. Bisymulacja
- 23-30 października: Semantyka denotacyjna języka TINY.
- 30 października - 6 listopada: Semantyka bloków, deklaracji i procedur.
- 20 listopada - 4 grudnia: Semantyka denotacyjna w ujęciu kontynuacyjnym
- 11-18 grudnia: Logika Hoare'a
- 7 stycznia: System HAHA. Projekt Compcert
Semantyka denotacyjna jako program funkcyjny
Poniższe programy są napisane w języku Haskell.
- Język TINY, przykładowy program: obliczanie liczb Fibonacciego.
- Bloki i deklaracje zmiennych.
- Procedury.
- Język TINY w ujęciu kontynuacyjnym.