Politechnika Warszawska - Centralny System Uwierzytelniania
Strona główna

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 )-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 Podstawowe informacje o zasadach przyporządkowania punktów ECTS:
  • roczny wymiar godzinowy nakładu pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się dla danego etapu studiów wynosi 1500-1800 h, co odpowiada 60 ECTS;
  • tygodniowy wymiar godzinowy nakładu pracy studenta wynosi 45 h;
  • 1 punkt ECTS odpowiada 25-30 godzinom pracy studenta potrzebnej do osiągnięcia zakładanych efektów uczenia się;
  • tygodniowy nakład pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się pozwala uzyskać 1,5 ECTS;
  • nakład pracy potrzebny do zaliczenia przedmiotu, któremu przypisano 3 ECTS, stanowi 10% semestralnego obciążenia studenta.
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 2021/2022 - sem. zimowy" (zakończony)

Okres: 2021-10-01 - 2022-02-22
Wybrany podział planu:
Przejdź do planu
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 2020/2021 - sem. letni" (zakończony)

Okres: 2021-02-20 - 2021-09-30
Wybrany podział planu:
Przejdź do planu
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 2020/2021 - sem. zimowy" (zakończony)

Okres: 2020-10-01 - 2021-02-19
Wybrany podział planu:
Przejdź do planu
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 2019/2020 - sem. letni" (zakończony)

Okres: 2020-02-22 - 2020-09-30
Wybrany podział planu:
Przejdź do planu
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:
Przejdź do planu
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:
Przejdź do planu
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:
Przejdź do planu
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

Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Politechnika Warszawska.
pl. Politechniki 1, 00-661 Warszawa tel: (22) 234 7211 https://pw.edu.pl kontakt deklaracja dostępności USOSweb 7.0.0.0-7 (2024-03-18)