SW wykład 1 - Wstęp: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| (Nie pokazano 5 wersji utworzonych przez 4 użytkowników) | |||
| Linia 3: | Linia 3: | ||
[[Grafika:sw0100.png|frame|center|]] | [[Grafika:sw0100.png|frame|center|]] | ||
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. | |||
<font size="-2">[[Semantyka i weryfikacja programów#moduły|<<powrót do strony wykładu]]</font> | |||
Aktualna wersja na dzień 09:29, 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.
