Semantyka i weryfikacja programów: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycja
WizualnieWikikod
m Przywrócono przedostatnią wersję, jej autor to Tarlecki
Mengel (dyskusja | edycje)
1013 edycji
 
(Nie pokazano 4 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 35: Linia 35:
== Moduły ==
== Moduły ==


* [[Template:Semantyka_i_weryfikacja_programów/Wykład 1|Wykład 1. Wprowadzenie]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 1|Ćwiczenia 1. Semantyka operacyjna 1]])
=== Moduły wykładowe ===
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 2|Wykład 2. Semantyka operacyjna]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 2|Ćwiczenia 2. Semantyka operacyjna 2]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 1|Wykład 1. Wprowadzenie]]  
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 3| Wykład 3. Semantyka naturalna]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 3|Ćwiczenia 3. Semantyka operacyjna 3/Semantyka naturalna 1]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 2|Wykład 2. Semantyka operacyjna]]  
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 4| Wykład 4. Semantyka denotacyjna. While programy]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 4|Ćwiczenia 4. Semantyka naturalna 2]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 3| Wykład 3. Semantyka naturalna]]  
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 5| Wykład 5. Semantyka denotacyjna. Bloki i deklaracje]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 5|Ćwiczenia 5. Semantyka naturalna 3]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 4| Wykład 4. Semantyka denotacyjna. While programy]]  
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 6| Wykład 6. Semantyka denotacyjna. Przekazywanie parametrów. Wejście/wyjście]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 6|Ćwiczenia 6. Semantyka naturalna 4]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 5| Wykład 5. Semantyka denotacyjna. Bloki i deklaracje]]
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 7| Wykład 7. Semantyka denotacyjna. Kontynuacje]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 7|Ćwiczenia 7. Semantyka denotacyjna 1]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 6| Wykład 6. Semantyka denotacyjna. Przekazywanie parametrów. Wejście/wyjście]]
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 8| Wykład 8. Punkty stałe w porządkach zupełnych]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 8|Ćwiczenia 8. Semantyka denotacyjna 2]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 7| Wykład 7. Semantyka denotacyjna. Kontynuacje]]  
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 9| Wykład 9. Elementy teorii dziedzin]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 9|Ćwiczenia 9. Semantyka denotacyjna 3]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 8| Wykład 8. Punkty stałe w porządkach zupełnych]]  
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 10| Wykład 10. Logika Hoare'a. Poprawność częściowa]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 10|Ćwiczenia 10. Semantyka denotacyjna 4]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 9| Wykład 9. Elementy teorii dziedzin]]  
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 11| Wykład 11. Relatywna pełność logiki Hoare'a]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 11|Ćwiczenia 11. Semantyka denotacyjna 5]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 10| Wykład 10. Logika Hoare'a. Poprawność częściowa]]  
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 12| Wykład 12. Poprawność całkowita]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 12|Ćwiczenia 12. Semantyka denotacyjna 6]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 11| Wykład 11. Poprawność i relatywna pełność logiki Hoare'a]]
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 13| Wykład 13. Wyprowadzanie poprawnych programów]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 13|Ćwiczenia 13. Weryfikacja programów 1]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 12| Wykład 12. Poprawność całkowita]]  
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 14| Wykład 14. Systematyczne konstruowanie modularnych programów]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 14|Ćwiczenia 14. Weryfikacja programów 2]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 13| Wykład 13. Wyprowadzanie poprawnych programów]]  
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 15| Wykład 15. Modelowanie semantyki denotacyjnej w językach funkcyjnych]] ([[Semantyka_i_weryfikacja_programów/Ćwiczenia 15|Ćwiczenia 15. Weryfikacja programów 3]])
* [[Template:Semantyka_i_weryfikacja_programów/Wykład 14| Wykład 14. Systematyczne konstruowanie modularnych programów]]
<!--* [[Template:Semantyka_i_weryfikacja_programów/Wykład 15| Wykład 15. Modelowanie semantyki denotacyjnej w językach funkcyjnych]]-->
 
=== Moduły ćwiczeniowe ===
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 1|Ćwiczenia 1. Semantyka operacyjna 1]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 2|Ćwiczenia 2. Semantyka operacyjna 2]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 3|Ćwiczenia 3. Semantyka operacyjna 3/Semantyka naturalna 1]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 4|Ćwiczenia 4. Semantyka naturalna 2]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 5|Ćwiczenia 5. Semantyka naturalna 3]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 6|Ćwiczenia 6. Semantyka naturalna 4]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 7|Ćwiczenia 7. Semantyka denotacyjna 1]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 8|Ćwiczenia 8. Semantyka denotacyjna 2]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 9|Ćwiczenia 9. Semantyka denotacyjna 3]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 10|Ćwiczenia 10. Semantyka denotacyjna 4]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 11|Ćwiczenia 11. Semantyka denotacyjna 5]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 12|Ćwiczenia 12. Semantyka denotacyjna 6]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 13|Ćwiczenia 13. Weryfikacja programów 1]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 14|Ćwiczenia 14. Weryfikacja programów 2]]
* [[Semantyka_i_weryfikacja_programów/Ćwiczenia 15|Ćwiczenia 15. Weryfikacja programów 3]]

Aktualna wersja na dzień 14:58, 16 paź 2006

Forma zajęć

Wykład (30 godzin) + ćwiczenia (30 godzin)

Opis

Celem wykładu jest pokazanie roli i najważniejszych problemów i technik formalizacji opisu programów. Omawiane będą metody definiowania semantyki programów, z ich matematycznymi podstawami i praktycznymi technikami. Wprowadzone zostaną pojęcia poprawności programów oraz techniki i formalizmy dla ich dowodzenia. Przedstawione też będą najważniejsze idee systematycznego konstruowania poprawnych programów.

Sylabus

Autorzy

  • Marcin Engel
  • Sławomir Lasota
  • Andrzej Tarlecki

Wymagania wstępne

  • Wstęp do programowania
  • Wstęp do teorii mnogości i logiki

Zawartość

  • Formalny opis języków programowania
  • Operacyjne i denotacyjne metody definiowania semantyki programów
  • Semantyczne definicje podstawowych konstrukcji programistycznych
  • Matematyczne podstawy semantyki denotacyjnej
  • Pojęcia poprawności programów: poprawność częściowa i całkowita
  • Metody dowodzenia poprawności programów
  • Logika Hoare'a, jej wykorzystanie i własności formalne
  • Systematyczne konstruowanie poprawnych programów

Literatura

  1. P. Dembiński, J. Manuszynski. Matematyczne metody definiowania języków programowania. WNT, 1981.
  2. M. Gordon. Denotacyjny opis języków programowania. WNT, 1983.
  3. D. Gries. The Science of Programming. Springer-Verlag, 1981.
  4. E. Dijkstra. Umiejętność programowania. WNT, 1978.

Moduły

Moduły wykładowe

Moduły ćwiczeniowe

Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów&oldid=63660”