Re[4]: First fully verified operating system kernel.
От: thesz Россия http://thesz.livejournal.com
Дата: 17.08.09 14:10
Оценка:
Здравствуйте, fmiracle, Вы писали:

F>Здравствуйте, thesz, Вы писали:


T>>После чего я ещё раз повторю, что "теперь исправление спецификации менее трудоёмкий процесс, поскольку нам покажут, где что не так в остальном коде" и добавлю, что допустить ошибки в спецификации можно только весьма высокоуровневые, которые ловятся гораздо меньшим количеством тестов.

T>>Если раньше (и сейчас) спецификация находилась в начале программы и исправление ошибок в ней были самые дорогие, то в будущем это всё будет не сложней исправлений ошибок типизации в языках типа C++.
F>Потому что для этого нужно формальное описание спецификации.

"Потому, что" открывает ответ на вопрос "почему".

Я не обнаружил вопроса в своих двух параграфах выше.

Какой же вопрос я задавал?

F>А создается спецификация на человеческом (т.е. неформальном) языке, понятном экспертам предметной области, которые формулируют задачу.

F>Перевод спецификации с человеческого языка в строгий формальный синтаксис лежит где-то очень близко к написанию собственно кода.

Ты, прошу прощения, комбинаторными библиотеками пользовался?

F>По сути дела код программы — это и есть формальное описание спецификации на языке C++, C# и т.д.


Nope. Close, but nope.

Код программы — это доказательство существования решения проблемы в ограничениях языка (C++, C#, Java, Haskell).

Спецификация — описание проблемы.

F>И проблемы возникают из-за

F>1. неверной формулировки задачи экспертом при составлении человеческой спецификации.
F>2. ошибки при переводе с неформального человеческого языка в формальное описание того же самого на C++, Хаскель, и прочих языках.

Вот здесь не надо всех равнять. Языки разные.

F>В данном случае п.1 никак не отменяется, а п.2 заменяется возможными ошибками при переводе на "язык формального описания спецификаций".


Построение доказательства существования решения подчиняется строгим правилам.

Чем лучше организованы эти правила (лучше система типов), тем быстрее мы получим ответ "ошибка в спецификации".

F>Я не говорю что пользы тут нет никакой — плюс тут может быть, если данный язык описания формальных спецификаций будет проще и понятнее, чем соответственно текущие языки разработки. Но это радикальное решение проблемы, а частное улучшение текущей ситуации.


Ну, да.

Иерархия вселенных.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.