SW wykład 1 - Slajd8: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| (Nie pokazano 1 wersji utworzonej przez jednego użytkownika) | |||
| 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ą | ||
syntaktyczną, czy nawet semantyczną poprawność budowanych programów, | syntaktyczną, czy nawet semantyczną poprawność budowanych programów, | ||
ale o zasady, na ogół nieco nieformalne, celowego wykorzystania | ale o zasady, na ogół nieco nieformalne, celowego wykorzystania | ||
poszczególnych konstrukcji programistycznych | poszczególnych konstrukcji programistycznych zgodnie z ich | ||
przeznaczeniem i rozumieniem. Ma to z jednej strony usprawnić | przeznaczeniem i rozumieniem. Ma to z jednej strony usprawnić | ||
budowanie programów przez programistę, a z drugiej | budowanie programów przez programistę, a z drugiej zapewnić lepsze | ||
rozumienie napisanego kodu. Mieszczą się tu choćby tak trywialne i | rozumienie napisanego kodu. Mieszczą się tu choćby tak trywialne i | ||
oczywiste, mam nadzieję, dla Państwa wskazówki, jak "używaj znaczących | oczywiste, mam nadzieję, dla Państwa wskazówki, jak "używaj znaczących | ||
nazw zmiennych" --- ale i znacznie bardziej | nazw zmiennych" --- ale i znacznie bardziej skomplikowane wskazówki, | ||
ułatwiające na przykład weryfikację merytoryczną powstałego kodu, | 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". | (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".
