Насколько я понял, не следует смешивать верификацию программ (о которой говорил captain cobalt) и формальную спецификацию.
Согласен, что в случае необходимости надо быть способным определить инвариант цикла, но это другое.
Языки спецификаций все-таки существуют (например, SDL), но говорят, что они слишком сложны в использовании (т.е. их использование скорее усложнит задачу, чем реально поможет).
Интересно, есть ли у кого-нибудь из участников соответствующий опыт?

Также и проверка типов всего лишь гарантирует совместимость "по разъемам", но не более того.
Вот отрывок из электронной книги Вирта "Programming in Oberon" (2004):

Concluding this introduction to the module concept, we postulate that adequate implementations
provide full type compatibility checking between objects, independent of whether these objects are
declared in the same or in different modules, i.e. the checking mechanism of the compiler functions also
across module boundaries. However, the programmer must realize that this checking provides no
absolute safeguard against mistakes. After all, it concerns formal, syntactic aspects only; it does not
cover the semantics. It would not detect, for instance, the replacement of the algorithm for the sine
function by that of the cosine function. However, it must not be regarded as the duty of a compiler to
protect programmers against malicious "colleagues".


Так я пока и не понял, как же мыслит программист.
Напротив, у меня в голове все смешалось, как в доме Облонских. :)
Наверное, за лучшее -- просто писать программы, как пишешь, и не лезть в дебри. :(
Но иногда так хочется понять, чем же ты все-таки занимаешься. :)

Ответ на »сообщение 982« (captain cobalt)

Опять бессмысленное утверждение.

Как чисто формально задать правило, что идентификаторы должны быть сначало где-то определены? Как чисто формально запретить определение идентификатора если данное имя уже было определено где-то выше? Как чисто формально сказать, что переменная должна быть инициализирована перед использованием?..

Ответ на »сообщение 982« (captain cobalt)
___________________________

Ответ на »сообщение 980« (Илья Ермаков)
___________________________

Естетственно, я знаю о формальных методах определения семантики.
Каких? ;-)


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

Ответ на »сообщение 982« (captain cobalt)
___________________________
Задача компилятора - оттранслировать алгоритм из терминов операций одного виртуального компьютера в термины операций другого. Но так или иначе упираемся в описание этого компьтера (машины Тьюринга, например), которое может быть выполнено только на естественном языке. Не все может быть выражено формально - существует теорема о принципиальной неполноте формальных систем.

Ответ на »сообщение 980« (Илья Ермаков)
___________________________

Естетственно, я знаю о формальных методах определения семантики.
Каких? ;-)

Однако полностью определить семантику формально все равно невозможно, такого же ознозначного аналога, как БНФ для синтаксиса здесь не существует.
Опять бессмысленное утверждение.
Примерно как "комплексных чисел не существует".

Именно поэтому описать ЯП, не прибегая к естественному языку, невозможно.
Давайте подумаем логически.

Без возможности полностью формально описать семантику языка компиляторы были бы невзможны. Задача компилятора - извлечь семантику из исходного текста и сохранить её в выходной программе. Как же компилятор это делает?

P.S. Бонус:
Philipp W. Kutter -- Dynamic semantics of the Oberon programming language (1996)
http://e-collection.ethbib.ethz.ch/show?type=incoll&nr=392&part=text

Ответ на »сообщение 980« (Илья Ермаков)
___________________________

Описание в какой-нибудь алгебраической нотации действительно трудно сделать, т.к. алгебраическая нотация плохо подходит для вещей типа NEW или сбор мусора :-)
Главное, потом практически использовать тоже малореально.

Ведь доказательство корректности программы тоже должно быть веррифицировано, а оно как правило гораздо длиннее и зануднее самой программы.

Но и естественный язык плох: обратите внимание, что Вирт в описании Оберона использует некое довольно ограниченное и довольно формальное подмножество естественного языка.

Тот факт, что формализм Дейкстры реально применим редко, хорошо известен и подробно и разумно обсуждался: сложные "по сути" алгоритмы встречаются крайне редко, а сложность больше "тривиальная" -- в большом количестве мелочей.
Каждая из которых довольно тривиальна, но возможно много тривиальных же вариаций, и какого-то хитроумного формализма для управления такого рода сложностью не нужно, просто много внимания и терпения и т.п. ...

С другой стороны, то, что более-менее часто используется, можно выделить в виде стандартных схем (шахматы хорошая аналогия -- как в шахматах есть классы стандартных схем, начиная от мелочей вроде вилки и вскрытого шаха) и просто применять их вместо полного формализма.

Но изредка приходится и по полной программе цикл строить -- с нетривиальным инвариантом и несколькими охранами (LOOP с телом из одного большого IF с несколькими ветвями и EXIT'ом на ELSE).
У меня за 10 лет такое случилось один раз, но без применения метода Дейкстры справиться не удалось, и алгоритм из числа ключевых и часто используемых (в моих задачах).

Ответ на »сообщение 979« (сcaptain cobalt)
___________________________

Естетственно, я знаю о формальных методах определения семантики. Однако полностью определить семантику формально все равно невозможно, такого же ознозначного аналога, как БНФ для синтаксиса здесь не существует. Именно поэтому описать ЯП, не прибегая к естественному языку, невозможно.

Формальная семантика языков программирования - это хорошо теоретически разработанная тема.

Читаются курсы в вузах.

Например:

http://ric.uni-altai.ru/Fundamental/cat-mat.htm

http://www.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/RMain.html

Стыдно говорить что

»сообщение 945« (Илья Ермаков)
___________________________

Полностью описать семантику большинства универсальных языков програмирования формально, не прибегая к естественному языку, невозможно.

Ответ на »сообщение 977« (Илья Ермаков)
___________________________


Остается уповать именно что на интуитивный, упрощенный вариант такого формального доказательства, который опытный программист постоянно прокручивает в уме. И ему не нужно выписывать все формулы так же, как, например, опытному шахматисту не нужно перебирать все дерево возможных ходов...

В сущности, в том и вопрос, как мыслит (или должен мыслить) программист.

Кстати, шахматная программа также не перебирает всех вариантов, а использует альфа-бета отсечение и эвристические методы оценки позиции.

Ответ на »сообщение 976« (Сергей Перовский)
___________________________
Знать методы формального доказательства программ полезно, их можно применять в некоторых необходимых случаях (для критичного ПО, и т.п.), однако для сложных систем все равно они малоприменимы...
Остается уповать именно что на интуитивный, упрощенный вариант такого формального доказательства, который опытный программист постоянно прокручивает в уме. И ему не нужно выписывать все формулы так же, как, например, опытному шахматисту не нужно перебирать все дерево возможных ходов...