Uniwersytet Kardynała Stefana Wyszyńskiego w Warszawie - Centralny System UwierzytelnianiaNie jesteś zalogowany | zaloguj się
katalog przedmiotów - pomoc

Semantyka i weryfikacja programów

Informacje ogólne

Kod przedmiotu: WM-I-SWP Kod Erasmus / ISCED: (brak danych) / (brak danych)
Nazwa przedmiotu: Semantyka i weryfikacja programów
Jednostka: Wydział Matematyczno-Przyrodniczy. Szkoła Nauk Ścisłych
Grupy:
Punkty ECTS i inne: 6.00
zobacz reguły punktacji
Język prowadzenia: polski
Poziom przedmiotu:

średnio-zaawansowany

Symbol/Symbole kierunkowe efektów uczenia się:

dla kierunku informatyka II st.:

X2A_W01, X2A_W03, X2A_W04, X2A_W01, I2_W01, I2_W05

dla kierunku matematyka II st.:

X2A_W01, X2A_W03, X2A_W04, X2A_W01, MA2_W02, MA2_W11


Skrócony opis:

Poziom przedmiotu: średnio-zaawansowany

Cele przedmiotu: Zapoznać słuchaczy z elementami specyfikacji i weryfikacji oprogramowania, w tym systemów kryptograficznych.

Wymagania wstępne: podstawowa umiejętność programowania

Pełny opis:

Treści merytoryczne:

1. Przykłady niepoprawnych programów

2. Przykłady semantyk operacyjnych, naturalnych, denotacyjnych

3. Logiki specyficzne

4. Różne własnośći poprawności systemów

5. Przykłady różnych modeli obliczeń. Struktury Kripkego

6. Sieci (zsynchronizowanych) automatów

7. Sieci Petriego (z czasem, kolorowane)

8. Modele czasowe

9. Logiki temporalne i ich zastosowania

10. Własności poprawności

11. Weryfikacja własności protokołów komunikacyjnych

Metody oceny:

egzamin ustny.

Literatura:

1. red. T. Szmuc, M. Szpyrka, Metody formalne w inżynierii oprogramowania systemów czasu rzeczywistego, WNT 2010.

2. M. Gordon. Denotacyjny opis języków programowania. WNT, 1983.

3. P. Dembiński, J. Manuszynski. Matematyczne metody definiowania języków programowania. WNT, 1981.

Efekty kształcenia i opis ECTS:

Student zna podstawy teorii informacji, teorii algorytmów i kryptografii oraz ich praktyczne zastosowania. 3 pkt ECTS

Metody i kryteria oceniania:

I2_W01:

Ocena 5.0 - Student doskonale zna i rozumie zastosowania rozwiązań informatycznych w różnych obszarach

Ocena 4.5 - Student bardzo dobrze zna i rozumie zastosowania rozwiązań informatycznych w różnych obszarach

Ocena 4.0 - Student dobrze zna i rozumie zastosowania rozwiązań informatycznych w różnych obszarach

Ocena 3.5 - Student zna i rozumie wybrane zastosowania rozwiązań informatycznych w różnych obszarach

Ocena 3.0 - Student zna i rozumie kilka zastosowań rozwiązań informatycznych w różnych obszarach

Ocena 2.0 - Student nie zna i nie rozumie kilku zastosowań rozwiązań informatycznych w różnych obszarach

I2_W05:

Ocena 5.0 - Student doskonale zna i rozumie metody weryfikacji semantyki programów, a także pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia

Ocena 4.5 - Student bardzo dobrze zna i rozumie metody weryfikacji semantyki programów, a także pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia

Ocena 4.0 - Student dobrze zna i rozumie metody weryfikacji semantyki programów, a także pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia

Ocena 3.5 - Student zna i rozumie kilka metod weryfikacji semantyki programów, a także podstawowe pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia

Ocena 3.0 - Student zna i rozumie kilka metod weryfikacji semantyki programów, a także podstawowe pojęcia poprawności programów

Ocena 2.0 - Student nie zna i nie rozumie kilku metod weryfikacji semantyki programów, a także podstawowych pojęć poprawności programów

I2_K01:

Ocena 5.0 - Student jest całkowicie gotów do identyfikacji ograniczeń własnej wiedzy i do nieustannego ustawicznego samokształcenia

Ocena 4.5 - Student jest częściowo gotów do identyfikacji ograniczeń własnej wiedzy i do ciągłego ustawicznego samokształcenia

Ocena 4.0 - Student jest częściowo gotów do identyfikacji ograniczeń własnej wiedzy i do ustawicznego samokształcenia w wybranych okresach czasu

Ocena 3.5 - Student jest czasami gotów do identyfikacji ograniczeń własnej wiedzy i do samokształcenia w wybranych okresach czasu

Ocena 3.0 - Student jest czasami gotów do identyfikacji ograniczeń własnej wiedzy i do samokształcenia

Ocena 2.0 - Student nie jest gotów do identyfikacji ograniczeń własnej wiedzy i do samokształcenia

Praktyki zawodowe:

Nie dotyczy

Zajęcia w cyklu "Semestr zimowy 2019/20" (zakończony)

Okres: 2019-10-01 - 2020-01-31
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Mirosław Kurkowski
Prowadzący grup: Jakub Gąsior, Mirosław Kurkowski
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzaminacyjny
Typ przedmiotu:

obowiązkowy

Grupa przedmiotów ogólnouczenianych:

nie dotyczy

Zajęcia w cyklu "Semestr zimowy 2020/21" (zakończony)

Okres: 2020-10-01 - 2021-01-31
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Mirosław Kurkowski
Prowadzący grup: Jakub Gąsior, Mirosław Kurkowski
Strona przedmiotu: https://e.uksw.edu.pl/course/view.php?id=14642
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzaminacyjny
E-Learning:

E-Learning (pełny kurs) z podziałem na grupy

Typ przedmiotu:

obowiązkowy

Grupa przedmiotów ogólnouczenianych:

nie dotyczy

Skrócony opis:

Przedmiot ma za zadanie zaoznanie studentów z:

- metodami formalnego określania semantyk wykonań algorytmów (programów),

- modelowania formalnego ich własności,

- badania tychże własności w oparciu o modele formalne.

Pełny opis:

W ramach przedmiotu studenci zostaną zapoznani z metodami formalnego opisu wykonań algorytmów (programów). Przedstawione zostaną semantyki naturalne, denotacyjne i operacyjne. Bazą do tych rozważań będzie wprowadzenie do teorii automatów, języków formalnych i obliczeń. Studenci zapoanzją się z podstawowymi struktorami i algorytmami tej teorii. Przedstawiona zostanie hierarchia Chomsky'ego. Na odpowiednich przykładach zostaną zaprezentowane własności algorytmó (programów) oraz metody ich weryfjikacji.

Literatura:

1. J. Hopcroft, J. Ullman, Wprowadzenie do teorii automatów, języków i obliczeń, PWN, Warszawa 2003.

2. J. Hopcroft, R. Motwani, J. Ullman, Wprowadzenie do teorii automatów, języków i obliczeń, PWN, Warszawa 2005.

3. A. Kościelski, Teoria obliczeń, wyd. UWr, Wrocław 1997.

Wymagania wstępne:

Podstawowa wiedza z Logiki matematycznej

Zajęcia w cyklu "Semestr zimowy 2021/22" (w trakcie)

Okres: 2021-10-01 - 2022-01-31
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Laboratorium, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Mirosław Kurkowski
Prowadzący grup: Jakub Gąsior, Mirosław Kurkowski
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzaminacyjny
E-Learning:

E-Learning (pełny kurs) z podziałem na grupy

Typ przedmiotu:

obowiązkowy

Grupa przedmiotów ogólnouczenianych:

nie dotyczy

Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Kardynała Stefana Wyszyńskiego w Warszawie.