Tekst źródłowy strony SW wykład 1 - Wstęp

{{Semantyka i weryfikacja programów/Wykład 1}}

[[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>