Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Статья 1988 года Э. В. Дайкстры "О жестокости настоящего обучения информатике" – научная статья 1988 года Э. В. Дайкстры, в которой утверждается, что компьютерное программирование следует понимать как область математики, и что формальная доказуемость программы является важнейшим критерием корректности. Вопреки названию, основная часть статьи посвящена попытке Дайкстры взглянуть на информатику в более широком научном контексте, а вопросы преподавания рассматриваются лишь в качестве следствия в конце. В частности, Дайкстра предложил "проект вводного курса программирования для первокурсников", основанный на логике Хоара как неинтерпретированной формальной системе.
1988 paper by E. W. Dijkstra
"On the Cruelty of Really Teaching Computing Science" is a 1988 scholarly article by E. W. Dijkstra which argues that computer programming should be understood as a branch of mathematics, and that the formal provability of a program is a major criterion for correctness. Despite the title, most of the article is on Dijkstra’s attempt to put computer science into a wider perspective within science, teaching being addressed as a corollary at the end. Specifically, Dijkstra made a “proposal for an introductory programming course for freshmen” that
consisted of Hoare logic as an uninterpreted formal system.
Дебаты о целесообразности
С момента появления термина «инженерия программного обеспечения» формальная верификация почти всегда считалась слишком затратной по ресурсам, чтобы быть практически применимой. В сложных приложениях сложность правильного определения того, что программа должна делать, также является распространенным источником ошибок. Для выявления и устранения ошибок обычно используются другие методы тестирования программного обеспечения, и при оценке качества программного обеспечения учитывается множество других факторов. До конца жизни Дейкстра считал, что основные задачи вычислительной техники не были решены в полной мере из-за недостаточного внимания к корректности программ (хотя он и не отрицал важности других требований, таких как поддерживаемость и эффективность).
Since the term "software engineering" was coined, formal verification has almost always been considered too resource intensive to be feasible. In complex applications, the difficulty of correctly specifying what the program should do in the first place is also a common source of error. Other methods of software testing are generally employed to try to eliminate bugs and many other factors are considered in the measurement of software quality. Until the end of his life, Dijkstra maintained that the central challenges of computing hadn't been met to his satisfaction, due to an insufficient emphasis on program correctness (though not obviating other requirements, such as maintainability and efficiency).
Педагогическое наследие
Сегодня преподавание компьютерных наук не всегда соответствует всем советам Дайкстры. Учебные программы обычно делают акцент на методах управления сложностью и подготовке к будущим изменениям, следуя ранним работам Дайкстры. К ним относятся абстракция, разработка по контракту и шаблоны проектирования. Методы программирования, направленные на предотвращение ошибок, и традиционные методы тестирования программного обеспечения преподаются как базовые требования, а студенты знакомятся с определенными математическими инструментами, однако формальные методы верификации обычно не включаются в учебную программу, разве что в качестве продвинутой темы. Таким образом, в некотором смысле идеи Дайкстры были восприняты, но не те, которые он считал наиболее важными. Новые учебные программы в области разработки программного обеспечения приняли рекомендации Дайкстры. В этих программах основное внимание уделяется формальному описанию требований к программному обеспечению и проектированию, чтобы облегчить формальную проверку корректности системы. В Канаде такие программы часто аккредитованы как инженерные степени с аналогичными базовыми компетенциями в области физики.
Computer science as taught today does not follow all of Dijkstra's advice. The curricula generally emphasize techniques for managing complexity and preparing for future changes, following Dijkstra's earlier writings. These include abstraction, programming by contract, and design patterns. Programming techniques to avoid bugs and conventional software testing methods are taught as basic requirements, and students are exposed to certain mathematical tools, but formal verification methods are not included in the curriculum except perhaps as an advanced topic. So in some ways, Dijkstra's ideas have been adhered to; however, the ideas he felt most strongly about have not been. Newly formed curricula in software engineering have adopted Dijkstra's recommendations. The focus of these programs is the formal specification of software requirements and design in order to facilitate the formal validation of system correctness. In Canada, they are often accredited engineering degrees with similar core competencies in physics based engineering.