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-MA-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:
Strona przedmiotu: https://e.uksw.edu.pl/course/view.php?id=14642
Punkty ECTS i inne: 5.00
zobacz reguły punktacji
Język prowadzenia: polski
Poziom przedmiotu:

podstawowy

Symbol/Symbole kierunkowe efektów uczenia się:

I2_W01, I2_W05, I2_K01

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.

Efekty kształcenia i opis ECTS:

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

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

I2_K01 - Student jest gotów do identyfikacji ograniczeń własnej wiedzy i do ustawicznego samokształcenia

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:

Brak

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: Mirosław Kurkowski, Michał Mazur
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: Mirosław Kurkowski, Michał Mazur
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.