Politechnika Warszawska - Centralny System UwierzytelnianiaNie jesteś zalogowany | zaloguj się
katalog przedmiotów - pomoc

Specyfikacje formalne i programy funkcyjne

Informacje ogólne

Kod przedmiotu: 103B-INxxx-MSP-SPOP Kod Erasmus / ISCED: (brak danych) / (brak danych)
Nazwa przedmiotu: Specyfikacje formalne i programy funkcyjne
Jednostka: Wydział Elektroniki i Technik Informacyjnych
Grupy: ( Przedmioty techniczne )---EITI
( Przedmioty zaawansowane )-Automatyka i robotyka-dr.-EITI
( Przedmioty zaawansowane )-Informatyka-dr.-EITI
( Przedmioty zaawansowane )-Systemy informacyjno-decyzyjne-mgr.-EITI
( Przedmioty zaawansowane obieralne )-Inżynieria systemów informatycznych-mgr.-EITI
( Przedmioty zaawansowane techniczne )--mgr.-EITI
Punkty ECTS i inne: 4.00
Język prowadzenia: polski
Jednostka decyzyjna:

103000 - Wydział Elektroniki i Technik Informacyjnych

Kod wydziałowy:

SPOP

Numer wersji:

2

Skrócony opis:

Celem przedmiotu jest przedstawienie metod i języków specyfikacyjnych w procesie tworzenia oprogramowania. Treść wykład obejmuje języki funkcyjne oraz metody weryfikowania specyfikacji. Ćwiczenia laboratoryjne umożliwiają studentom nabycie praktycznej umiejętności programowania w języku Haskel i zapoznanie się z techniką specyfikacji systemu w języku Alloy oraz analizy specyfikacji z użyciem narzędzia Alloy Analyzer.

Pełny opis:

Celem przedmiotu jest przedstawienie metod i języków specyfikacyjnych w procesie tworzenia oprogramowania. Treść wykład obejmuje języki funkcyjne oraz metody weryfikowania specyfikacji. Ćwiczenia laboratoryjne umożliwiają studentom nabycie praktycznej umiejętności programowania w języku Haskel i zapoznanie się z techniką specyfikacji systemu w języku Alloy oraz analizy specyfikacji z użyciem narzędzia Alloy Analyzer.

Treść wykładu

  • Wprowadzenie (4h): rola języków specyfikacji w procesie tworzenia oprogramowania, nieformalne i formalne języki specyfikacji, metody weryfikacji specyfikacji, specyfikacje wykonywalne i języki funkcyjne.
  • Programowanie funkcyjne (12h): programowanie imperatywne a programowanie funkcyjne, wprowadzenie do programowanie w języku Haskell: proste typy danych, listy, krotki, typy polimorficzne, klasy typów, typy rekurencyjne, funkcje, lambda abstrakcje, dopasowywanie wzorca, leniwe wyliczanie, nieskończone struktury danych, definiowanie operatorów, operacje wejścia/wyjścia, monady, moduły, przykłady.
  • Modelowanie oprogramowania przy użyciu języka Alloy (6h): notacja języka Alloy: relacje, operatory, kwantyfikatory, sygnatury i pola, definiowanie predykatów i faktów; analiza modeli przy użyciu narzędzia Alloy Analyzer, przykłady.
  • Modelowanie oprogramowania przy użyciu sieci Petriego (6h): podstawowa definicja sieci Petriego, właściwości sieci, metody analizy, zastosowanie - przykłady weryfikacji programów; sieci kolorowane, właściwości sieci kolorowanych i metody ich analizy.
  • Kolokwium (2h): zadania.

    Zakres laboratorium
    W ramach laboratorium studenci nabierają praktycznych umiejętności programowania w języku Haskell, realizując kilka prostych zadań oraz pisząc jeden większy program. Szczegółowa treść zadań jest określana przez prowadzących i w przypadku większego programu może uwzględniać indywidualne zainteresowania studentów. Odrębnym zadaniem laboratoryjnym jest napisanie specyfikacji zadanego systemu w języku Alloy oraz jej analiza z użyciem narzędzia Alloy Analyzer. W trakcie zajęć laboratoryjnych wykorzystane będą innowacyjne metody kształcenia.

Literatura:

    1. K. Sacha, Projektowanie oprogramowania systemów sterujących, Oficyna Wydawnicza PW, Warszawa, 1996.
    2. Dokumentacja języka Haskell dostępna na stronie http://www.haskell.org.
    3. Dokumentacja języka Alloy dostępna na stronie http://alloy.mit.edu.

Metody i kryteria oceniania:

Zaliczenie przedmiotu odbywa się na podstawie ocen z dwóch kolokwiów
(pierwsze dotyczy programowania funkcyjnego, drugie języka Alloy i
sieci Petriego) oraz oceny z projektu w języku Haskell . Za każde z
kolokwiów można maksymalnie otrzymać 15 pkt., natomiast za projekt - 20
pkt. Łącznie można uzyskać 50 pkt. Uzyskana liczba punktów przekłada
się na ostateczną ocenę w sposób następujący: ocena 2 (mniej niż 26
pkt.); 3 (26 - 30 pkt.); 3,5 (31 - 35 pkt.); 4 (36 - 40 pkt.); 4,5 (41
- 45 pkt.); 5 (co najmniej 46 pkt.).

Zajęcia w cyklu "rok akademicki 2019/2020 - sem. letni" (w trakcie)

Okres: 2020-02-22 - 2020-09-30

Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 48 miejsc więcej informacji
Wykład, 30 godzin, 48 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2019/2020 - sem. zimowy" (zakończony)

Okres: 2019-10-01 - 2020-02-21
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 60 miejsc więcej informacji
Wykład, 30 godzin, 60 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2018/2019 - sem. letni" (zakończony)

Okres: 2019-02-18 - 2019-09-30
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 48 miejsc więcej informacji
Wykład, 30 godzin, 48 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2018/2019 - sem. zimowy" (zakończony)

Okres: 2018-10-01 - 2019-02-17
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 48 miejsc więcej informacji
Wykład, 30 godzin, 48 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2017/2018 - sem. letni" (zakończony)

Okres: 2018-02-19 - 2018-09-30
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 48 miejsc więcej informacji
Wykład, 30 godzin, 48 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2017/2018 - sem. zimowy" (zakończony)

Okres: 2017-10-01 - 2018-02-18
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 48 miejsc więcej informacji
Wykład, 30 godzin, 48 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2016/2017 - sem. letni" (zakończony)

Okres: 2017-02-20 - 2017-09-30
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 60 miejsc więcej informacji
Wykład, 30 godzin, 60 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2016/2017 - sem. zimowy" (zakończony)

Okres: 2016-10-01 - 2017-02-19
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 70 miejsc więcej informacji
Wykład, 30 godzin, 70 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2015/2016 - sem. letni" (zakończony)

Okres: 2016-02-23 - 2016-09-30
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 60 miejsc więcej informacji
Wykład, 30 godzin, 60 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2015/2016 - sem. zimowy" (zakończony)

Okres: 2015-10-01 - 2016-02-22
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 60 miejsc więcej informacji
Wykład, 30 godzin, 60 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2014/2015 - sem. letni" (zakończony)

Okres: 2015-02-23 - 2015-09-30
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 48 miejsc więcej informacji
Wykład, 30 godzin, 48 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2014/2015 - sem. zimowy" (zakończony)

Okres: 2014-09-29 - 2015-02-22
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 48 miejsc więcej informacji
Wykład, 30 godzin, 48 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2013/2014 - sem. letni" (zakończony)

Okres: 2014-02-24 - 2014-09-28
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 56 miejsc więcej informacji
Wykład, 30 godzin, 56 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2013/2014 - sem. zimowy" (zakończony)

Okres: 2013-10-01 - 2014-02-23
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 60 miejsc więcej informacji
Wykład, 30 godzin, 60 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2012/2013 - sem. letni" (zakończony)

Okres: 2013-02-20 - 2013-09-30
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 60 miejsc więcej informacji
Wykład, 30 godzin, 60 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Zajęcia w cyklu "rok akademicki 2012/2013 - sem. zimowy" (zakończony)

Okres: 2012-10-01 - 2013-02-19
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 15 godzin, 55 miejsc więcej informacji
Wykład, 30 godzin, 55 miejsc więcej informacji
Koordynatorzy: Marcin Szlenk
Prowadzący grup: Marcin Szlenk
Lista studentów: (nie masz dostępu)
Zaliczenie: Ocena łączna
Jednostka realizująca:

103100 - Instytut Automatyki i Informatyki Stosowanej

Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Politechnika Warszawska.