SW wykład 1 - Wstęp: Różnice pomiędzy wersjami
m (SW wykład 1 - Slajd1 moved to SW wykład 1 - Wstęp) |
|||
| Linia 21: | Linia 21: | ||
wielu przypadkach wręcz niezbędne dla zapewnienia wysokiej jakości i | wielu przypadkach wręcz niezbędne dla zapewnienia wysokiej jakości i | ||
niezawodności budowanego oprogramowania. | niezawodności budowanego oprogramowania. | ||
| + | <font size="-2">[[Semantyka i weryfikacja programów#moduły|<<powrót do strony wykładu]]</font> | ||
Wersja z 09:28, 24 paź 2006
Wstęp Literatura Programy Programy, sprzeczne oczekiwania WielkiCel Składnia Semantyka Pragmatyka Logika Metodyka Implementacja Formalna semantyka Przykład Przykład, c.d. Przykład, reguła dowodzenia Uzasadnianie poprawności Plan zajęć
W ramach niniejszych zajęć będziemy przedstawiać wybrane metody i techniki formalnego opisu i analizy programów. Większość modułów poświęcimy omówieniu kilku podstawowych metod definiowania semantyki (precyzyjnie zdefiniowanego matematycznego znaczenia) programów, czy raczej języków programowania. Semantyka języka programowania jest bowiem podstawą dla opracowania wszelkich metod formalnych, które w poważny sposób chciałoby się stosować do konstrukcji i analizy programów danego języka. Wprowadzimy też klasyczne już pojęcia poprawności programów i metody dowodzenia poprawności. Końcowe zajęcia będą poświęcone wprowadzeniu do metod systematycznego konstruowania poprawnych programów i systemów oprogramowania.
Jednak poza przedstawieniem konkretnych metod i technik formalnego opisu i analizy programów, najważniejszym celem tych zajęć jest zaszczepienie przekonania, że wykorzystanie metod formalnych jest możliwe, może być efektywne, jest niezwykle ważne i użyteczne, a w wielu przypadkach wręcz niezbędne dla zapewnienia wysokiej jakości i niezawodności budowanego oprogramowania. <<powrót do strony wykładu
