rv82 писал(а):
Если честно, с трудом себе представляю, о чём идёт речь...
Ух очень я привык к Смолтоку. А с КП слишком мало "общался", так что некоторые вещи в нём пока непонятны.
Дык, батенька, инвариант и формальный вывод - это не зависящая от языка концепция. Это введенный некогда Э. Дейкстрой метод математического обоснования корректности кода.
Можно либо доказывать правильность уже написанного - что трудоемко и не особо удобно, поэтому лучше поступать наоборот - начинать с формальных выкладок и по ним "раскручивать" код, ну, конечно, только в тех местах, где он неочевиден - сложные циклы, например.
Для знакомства с инвариантом цикла могу предложить INTUIT.RU:
http://www.intuit.ru/department/se/pbmsu/5/ - хотя мне года два назад это объяснение не понравилось. Я лично разобрался окончательно этой осенью, когда готовил по этой теме лекции для своего "Программного конструирования" в ОГУ - и разобрался по конспектам лекций Info21 на физфаке МГУ, за что ему огромное спасибо. Очень надеюсь, у него когда-нибудь дойдут руки довести свои материалы до публичного вида!
Есть очень хорошая брошюрка Р. Бейбера "Программное обеспечение без ошибок: приемы и секреты создания правильных программ". Издавалась в 1996 г., библиографическая редкость - совершенно случайно этой осенью я ее купил в Москве в Доме книги... Я ее давно хочу пересканировать, для общего пользования. Постараюсь сегодня это, наконец, сделать.
Вход
FAQ
Поиск
