OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Пятница, 18 Август, 2017 15:35

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 17 ] 
Автор Сообщение
СообщениеДобавлено: Вторник, 04 Февраль, 2014 11:21 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 549
Откуда: Казань
А.П. Ершов в своей знаменитой статье "Предварительные соображения о лексиконе программирования" выдвинул концепцию "лексикона программирования":
Цитата:
Чем лексикон отличается от языка программирования? Он выражает не только и не столько программы, сколько их свойства и наши суждения о них. Язык программирования кодирует объекты предметной области задачи, а наше знание об этих объектах остается за пределами программного текста. Лексикон же является средством описания объектов предметных областей и содержит нотацию для построения баз знаний о предметных областях. Программа, выраженная средствами лексикона, в определенном смысле содержит в своем тексте описание своей семантики в виде совокупности нетривиальных фактов о вычисляемой ею функции – в отличие от "чистых" программ, которые не говорят ничего о своих функциональных свойствах.

Лексикон, в отличие от конкретного языка программирования, является открытой системой. Для него в целом не ставится задача трансляции любого его текста в машинную программу, хотя любая машинная программа в случае необходимости может быть выражена в лексиконе. Аналогично естественному языку лексикон обладает способностью описания одной своей части средствами другой своей же части.

Не надо думать, что лексикон – это все и навсегда. Это тщательно отобранная, но развивающаяся система удачных обозначений. Степень его успеха определяется степенью общезначимости и общепонятности его нотации.


Развил ли кто-нибудь идеи о лексиконе программирование Ершова и где можно почитать об этих разработках?


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 04 Февраль, 2014 11:47 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 2046
Вот отсюда обсуждалось. Этим занимался, допустим, по-своему Зверев, как я понимаю. В том смысле, что "лексикон" можно понимать как язык "математической алгоритмизации" здесь...


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 04 Февраль, 2014 12:03 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 549
Откуда: Казань
Насчет Зверева не знаю насколько это то, так как не читал его книг. А, во-вторых, в списке литературы в его книгах нет ссылки на статью "Предварительные соображения о лексиконе программирования", в одной только его книге есть ссылка на Ершова на статью про информатику.

Насчет прошедшего обсуждения на oberoncore, как я понял, там обсуждение шло в ключе, что Оберон - это и есть лексикон программирования. Но с этим не полностью согласен, так как в соответствие с тем, что писал Ершов: "Он выражает не только и не столько программы, сколько их свойства и наши суждения о них", "Лексикон, в отличие от конкретного языка программирования, является открытой системой. " и "Для него в целом не ставится задача трансляции любого его текста в машинную программу". А этим критериям Оберон не удовлетворяет.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 04 Февраль, 2014 21:03 

Зарегистрирован: Суббота, 07 Март, 2009 15:39
Сообщения: 2846
Откуда: Астрахань
С сегодняшнего времени смотря на те размышления Ершова, можно говорить о построении онтологии программирования. Или более широко - онтологии ИТ :)
То есть системы понятий и связей между ними.
Это и будет тот самый лексикон.
Конкретный язык программирования, естественно, не может претендовать на эту роль.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 04 Февраль, 2014 21:21 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 316
Откуда: Москва
Rifat писал(а):
Не надо думать, что лексикон – это все и навсегда. Это тщательно отобранная, но развивающаяся система удачных обозначений. Степень его успеха определяется степенью общезначимости и общепонятности его нотации.

Мне кажется, что Андрей Петрович Ершов мыслил в рамках текстового (не визуального) программирования. Он представлял себе лексикон как чисто текстовую (не визуальную) систему.
Он умер в 1988 году и не мог предвидеть, что визуальные идеи (понимаемые как расширение текста с помощью графики) будут получать все более широкое распространение.

Тот факт, что он умело использовал графику при анализе схем Янова, не меняет дела. Не меняет в том смысле, что Андрей Петрович (как мне кажется) не допускал даже мысли, что со временем в состав лексикона — наряду с текстом — обязательно войдет графика.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 04 Февраль, 2014 23:26 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 549
Откуда: Казань
Вообще статья, конечно, многогранна и каждый может увидеть там что-то свое.

Мое понимание этой статьи основывается на следующих фразах:
Цитата:
...Конечно, здесь мы сознательно умалчиваем о более глубоких средствах: верификаторах и трансформаторах программ, но эти средства мы побережем для развития главной идеи.

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

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

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

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

...Синтезированную программу нужно объединять с заготовленным программным модулем, который, в свою очередь, получается конкретизацией более общей программы. Полученная программа должна быть составлена на разные машины и опираться на библиотеки, выраженные на разных языках. Сразу появляется задача о языковой среде, в которой должен выполняться проект, включая и его логическую, доказательную сторону. В качестве альтернативы единому языку программирования мы выдвигаем понятие о языковой среде, которую мы называем лексиконом программирования. Лексикон программирования – это лингвистическая система с фразовой структурой, содержащая в себе формальную нотацию для выражения всех общезначимых конструкций, употребляемых при формулировании условий задачи, при синтезе и преобразовании программ.

В качестве основы лексикон содержит стандартную математическую символику алгебры, теории множеств, математической логики. В дополнение к ней лексикон содержит нотацию для основных конструкций и примитивов программирования на самых разных уровнях. Смысл этих конструкций сам выражается средствами лексикона. Лексикон содержит развитую систему именования и разнообразные правила подстановки.


То есть, программы на условном языке, например, на языке придуманном Дейкстрой и дополненные предусловиями, постусловиями, инвариантами на математическом языке логики, претендует на вариант лексикона программирования (см. вложенный файл)
Вложение:
Комментарий к файлу: Алгоритм из книги Гриса "Наука программирования"
lex.PNG
lex.PNG [ 18.9 КБ | Просмотров: 6135 ]


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 05 Февраль, 2014 13:08 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 549
Откуда: Казань
Валерий Лаптев писал(а):
С сегодняшнего времени смотря на те размышления Ершова, можно говорить о построении онтологии программирования. Или более широко - онтологии ИТ :)
То есть системы понятий и связей между ними.
Это и будет тот самый лексикон.
Конкретный язык программирования, естественно, не может претендовать на эту роль.

Вы понимаете слово лексикон не в том значении, которое подразумевал Ершов. Возможно, что он просто выбрал неудачное слово, которое многими понимается в другом ключе: лексикон - тезаурус или профессиональный словарь.
А он под этим словом подразумевал протоязык (первичный язык, на котором описывается задача и спецификация программы).


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 05 Февраль, 2014 13:11 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 549
Откуда: Казань
Владимир Паронджанов писал(а):
Rifat писал(а):
Не надо думать, что лексикон – это все и навсегда. Это тщательно отобранная, но развивающаяся система удачных обозначений. Степень его успеха определяется степенью общезначимости и общепонятности его нотации.

Мне кажется, что Андрей Петрович Ершов мыслил в рамках текстового (не визуального) программирования. Он представлял себе лексикон как чисто текстовую (не визуальную) систему.
Он умер в 1988 году и не мог предвидеть, что визуальные идеи (понимаемые как расширение текста с помощью графики) будут получать все более широкое распространение.

Тот факт, что он умело использовал графику при анализе схем Янова, не меняет дела. Не меняет в том смысле, что Андрей Петрович (как мне кажется) не допускал даже мысли, что со временем в состав лексикона — наряду с текстом — обязательно войдет графика.

Если исходить из следующих критериев:
1) "Он выражает не только и не столько программы, сколько их свойства и наши суждения о них",
2) "Лексикон, в отличие от конкретного языка программирования, является открытой системой. "
То, допустим, графический язык Дракон удовлетворяет первому пункту лишь частично, он позволяет отследить поток управления, но не выражает суждения о программе и другие свойства программы. А второму пункту он не удовлетворяет вообще, так как правила языка Дракон фиксированные и не могут расширяться.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 05 Февраль, 2014 15:07 

Зарегистрирован: Понедельник, 23 Март, 2009 10:35
Сообщения: 98
Откуда: Ханты-Мансийск
Валерий Лаптев писал(а):
С сегодняшнего времени смотря на те размышления Ершова, можно говорить о построении онтологии программирования. Или более широко - онтологии ИТ :)
То есть системы понятий и связей между ними.
Это и будет тот самый лексикон.
Конкретный язык программирования, естественно, не может претендовать на эту роль.

Согласен.
Об онтологиях программирования можно поискать у Анатолия Левенчука ailev.livejournal.com


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 05 Февраль, 2014 18:13 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 2046
Ну, в общем, это то, чем Лавров занимался, так что ли?..
Кстати, была бы модель, а формы записи можно (и нужно, наверное) определить для неё разные... и текстовые, и графические...


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 21 Февраль, 2014 21:01 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 549
Откуда: Казань
Нашел упоминание "лексикона" в книге "Прикладные методы верификации программ":
Цитата:
Языки спецификации свойств программ, в отличие от языков спецификации задач, должны быть приближены к соответствующим языка программирования высокого уровня (ADA, Паскаль, ПЛ/1 и др.), свойства конструкций который они должны характеризовать. Целесообразно рассматривать поэтому язык спецификации свойств программ как составную часть общей с языком программирования языковой среды (лексикона), используемой разработчиком программ.
Лексикон как смесь двух и более формальных языков, есть язык более высокого уровня, чем обычный язык программирования. Если на языке программирования описываются только обрабатываемая информация и процессы вычислений (алгоритм, реализующий задачу), то на языке спецификации свойств программ дополнительно может описываться метаинформация о программе - свойствах объектов программы и процессов вычислений по программе. Такая метаинформация представляется, как уже отмечалось в гл. 1, в виде контролирующих структур, сопровождающих программный текст и используемых в процессе разработки или (и) сопровождения программы, а иногда и в процессе выполнения программы.
Заметим, что спецификация свойств программы в процессе разработки поддерживает необходимую обратную связь между объектом разработки (программой) и спецификацией задачи (на языке функциональной спецификации), обеспечивая итеративный характер процесса разработки. Сопоставление спецификации задачи и спецификации свойств программы позволяет проводить коррекцию задачи или программы при последующих итерациях. Это создает основу для эффективных технологий надежного проектирования программ.
Наиболее развитыми возможностями обладают логические языки спецификации свойств программ. Они создаются обычно на базе логических выражений языка программирования, расширенных свойствами квантификации и аксиоматического определения новых понятий проблемной области. Элементами утверждений о свойствах программ обычно являются логические инварианты - формулы языка спецификации, связанные с соответствующими точками текста программы или объектами программы.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 20 Март, 2014 01:01 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 549
Откуда: Казань
Нашел еще одно упоминание о лексиконе программирования в книге "Прикладные методы верификации программ". Данное описание достаточно хорошо определяет что же такое "лексикон программирования":
Цитата:
Специфицировать программу - это значит указать на достаточно высоком уровне абстракции, какими свойствами должно обладать ее выполнение. Достичь этого можно, записывая соответствующие формулы (спецификации) в тексте программы (перед или после отдельных фрагментов либо всей программы). Они являются утверждениями о том, что должно быть истинно в соответствующих точках программы. Указанные утверждения назовем индуктивными утверждениями.
Различие между спецификациями (индуктивными утверждениями) и инвариантами состоит в том, что индуктивные утверждения отражают лишь желаемые свойства, которые при наличии ошибок могут не соответствовать фактическим свойствам (инвариантам).
Программа с записанными индуктивными утверждениями о ней или ее фрагментах является аннотированной программой. Аннотированная программа - качественно новый объект по сравнению с обычной программой. Если обычная программа представляет лишь алгоритм решения задачи, то аннотированная - формальное утверждение о программе (алгоритме и, возможно, о данных программы). Это означает, что аннотированные программы можно рассматривать как некоторый специальный вид логических формул, способных принимать значения true или false.
Образно говоря, аннотированная программа - формула на лексиконе (язык программирования + логический язык спецификации). Такое ее рассмотрение открывает широкие возможности для формальных преобразований аннотированных программ и формальных доказательств свойств программ, что является основой для верификации и оптимизации программ. Аннотированные программы являются также ценным компонентом документации и могут эффективно использоваться в процессах отладки (тестирования) и контроля работы программы.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 26 Октябрь, 2016 12:40 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 549
Откуда: Казань
Данную цитату, как мне кажется, можно считать определением лексикона программирования, в том смысле, как его понимал А.П. Ершов (цитата взята из книги "Практические методы верификации программ"):
Цитата:
2.3 ЛОГИЧЕСКИЙ ЯЗЫК СПЕЦИФИКАЦИИ СВОЙСТВ ПРОГРАММ

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

Следует иметь в виду, что оба эти качества формального языка спецификации не могут быть безграничны в своем приближении к естественному языку и к неформальным способам рассуждений. Для этого достаточно богатого формального логического языка существуют как невыразимые утверждения естественного языка, так и недоказуемы (но истинные) формальные утверждения.

С практической точки зрения логический язык спецификации свойств программ должен обладать следующими свойствами.

А. Расширяемостью, т.е. возможностью включения в язык новых понятий, определяемых пользователем (программистом). Успех формализации часто зависит от того, насколько удачен выбор понятий, характеризующих искомую проблемную область. Потребности спецификации нельзя покрыть лишь стандартными, универсальными понятиями; поэтому развитый язык спецификации должен быть открыт для последующих расширений пользователями.

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

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

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

Для удовлетворения всем этим требованиям изобразительные средства языка спецификации должны быть более развитые, чем обычные средства языка логики предикатов, создающие для него лишь теоретическую основу. Будем считать также, что каждый логический язык спецификации есть дополнение к некоторому базовому языку программирования, составляющему с ним общую языковую среду (лексикон).


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 27 Октябрь, 2016 06:42 

Зарегистрирован: Суббота, 16 Февраль, 2008 07:58
Сообщения: 285
Откуда: Россия, Стерлитамак
Rifat писал(а):
Данную цитату, как мне кажется, можно считать определением лексикона программирования, в том смысле, как его понимал А.П. Ершов (цитата взята из книги "Практические методы верификации программ")

А в этой книге примеры есть на данную тему? Сложно усваиваю теорию без примеров. Начал читать Эрика Эванса по DDD, вроде как перекликается в чём-то. Может быть там примеры найду, если тут не окажется


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 27 Октябрь, 2016 09:37 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 549
Откуда: Казань
adva писал(а):
А в этой книге примеры есть на данную тему?

Пример модуля, который вводит новые понятия для спецификации и верификации алгоритмов сортировки.
Код:
 module area Sort_array;
    use:area Ar_int_m;
    var M:array; i, j: integer;
    fun неопр. константы: →array; rep ωA;
                           →Boolean; rep ωB;
                           →integer; rep ωI;
        перестановка: array✕array→Boolean; rep perm(M1, M2);
        упорядоч. массив: array✕integer✕integer→Boolean; rep ord(M1, i, j);
        длина массива: array→integer; rep λ(M)
    end fun
  axioms /* аксиомы предиката perm */
  A.Perm1. perm(M1, M2)⇒λ(M1)=λ(M2);
  A.Perm2. perm(M1, M2)=perm(M2,M1);
  A.Perm3. M1=M2⇒perm(M1, M2);
  A.Perm4. perm(M1, M)⋀perm(M, M2)⇒perm(M1, M2);
  A.Perm5. (1≤j≺i≺λ(M))⇒perm(M, upd(M, j, M[i]), i, M[j]);
         /* аксиомы предиката ord */
  A.Ord1. (i≤j)⇒ord(M, i, j);
  A.Ord2. (i≤k≺j)⇒ord(M, i, j)=ord(M, i, k)⋀ord(M, k+1, j)⋀M[k]≤M[k+1];
         /* аксиомы функции длины λ */
  A.L1. λ(M1)≠λ(M2)⇒perm(M1, M2)=ωB;
  A.L2. 0≥j≻λ(M)⇒M[j]=ωI;
  A.L2. 0≻j, i≻λ(M)⇒upd(M, j, e)=ωA⋀ord(M, i, j)=ωB;
end Sort_array.

Здесь есть:
- расширяемость (вы можете дополнить модуль своими аксиомами и понятиями);
- модульность (понятия, касающиеся сортировки массива, вынесены в данный модуль);
- иерархичность (модуль опирается на аксиомы массива, которые определены в Ar_int_m);
- приближение к языку программирования (например, M[k]≤M[k+1]).

Совокупность таких модулей, например, для спецификации алгоритмов сортировки, поиска, для описания различных типов данных, таких как стек, очередь, дерево и другие, а также различные модули для более узкоспециализированных задач и составили бы Лексикон программирования в том понимании, как это понимал А.П.Ершов.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 27 Октябрь, 2016 14:51 

Зарегистрирован: Суббота, 16 Февраль, 2008 07:58
Сообщения: 285
Откуда: Россия, Стерлитамак
А меня зацепил момент:
Цитата:
Расширяемостью, т.е. возможностью включения в язык новых понятий, определяемых пользователем (программистом). Успех формализации часто зависит от того, насколько удачен выбор понятий, характеризующих искомую проблемную область.

а именно "понятий, характеризующих искомую проблемную область". Хотя может я и нет акценты воспринял.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 27 Октябрь, 2016 15:23 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 549
Откуда: Казань
Да, смысл в том, чтобы не просто закрепить какие-то аксиомы для типа boolean, integer и все на этом, а в том, чтобы можно было добавлять новые понятия, например, для:
- операций линейной алгебры;
- геометрии;
- аксиомы, касающиеся, редактирования текста, например;
- аксиомы, касающиеся парсинга текста, например;
- и так далее, всего того, что поддаётся спецификации и аксиоматизации.


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 17 ] 

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2017, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB