SW wykład 1 - Slajd8: Różnice pomiędzy wersjami
Nie podano opisu zmian |
mNie podano opisu zmian |
||
Linia 1: | Linia 1: | ||
{{Semantyka i weryfikacja programów/Wykład 1}} | {{Semantyka i weryfikacja programów/Wykład 1}} | ||
[[Grafika:sw0107.png|frame|center|]] | [[Grafika:sw0107.png|frame|center|]] | ||
Koniecznie trzeba podkreślić, że nie chodzi tu o formalną | Koniecznie trzeba podkreślić, że nie chodzi tu o formalną |
Wersja z 11:14, 17 sie 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ęć

Koniecznie trzeba podkreślić, że nie chodzi tu o formalną syntaktyczną, czy nawet semantyczną poprawność budowanych programów, ale o zasady, na ogół nieco nieformalne, celowego wykorzystania poszczególnych konstrukcji programistycznych, zgodnie z ich przeznaczeniem i rozumieniem. Ma to z jednej strony usprawnić budowanie programów przez programistę, a z drugiej, zapewnić lepsze rozumienie napisanego kodu. Mieszczą się tu choćby tak trywialne i oczywiste, mam nadzieję, dla Państwa wskazówki, jak "używaj znaczących nazw zmiennych" --- ale i znacznie bardziej skomplikowanego wskazówki ułatwiające na przykład weryfikację merytoryczną powstałego kodu, w rodzaju "ograniczaj do minimum odwołania do globalnego stanu (zewnętrznych zmiennych) w procedurach".