SW wykład 1 - Slajd8: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| (Nie pokazano 3 wersji utworzonych przez 2 użytkowników) | |||
| Linia 1: | Linia 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ą | |||
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 skomplikowane wskazówki, | |||
ułatwiające na przykład weryfikację merytoryczną powstałego kodu, na przykład "ograniczaj do minimum odwołania do globalnego stanu | |||
(zewnętrznych zmiennych) w procedurach". | |||
Aktualna wersja na dzień 08:05, 27 wrz 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 skomplikowane wskazówki, ułatwiające na przykład weryfikację merytoryczną powstałego kodu, na przykład "ograniczaj do minimum odwołania do globalnego stanu (zewnętrznych zmiennych) w procedurach".
