OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Пятница, 16 Ноябрь, 2018 10:22

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




Начать новую тему Ответить на тему  [ Сообщений: 24 ]  На страницу Пред.  1, 2
Автор Сообщение
СообщениеДобавлено: Воскресенье, 04 Ноябрь, 2018 16:55 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 726
Откуда: Казань
Валерий Лаптев писал(а):
Еще порекомендую книжку по Model Checking Карпова
http://avidreaders.ru/book/model-checki ... ennyh.html
Это как раз о верификации параллельных программ

Есть статья Loop Invariants: Analysis, Classification, and Examples там говорится:
Цитата:
Some of these techniques, such as model checking [Clarke et al. 1999] and abstract interpretation [Cousot and Cousot 1977], are directed at finding specific errors, such as the possible violation of a safety property. An advantage of these techniques is that they work on programs as they are, without imposing a significant extra annotation effort on programmers. For full functional correctness—the task of proving that a program satisfies a complete specification—the approach of choice remains, for imperative programs, the Floyd-Hoare-Dijkstra style of axiomatic semantics. In this approach, programs must be equipped with annotations in the form of assertions. Every loop, in particular, must have a loop invariant.

То есть, насколько я понимаю, здесь говорится о том, что метод model checking позволяет проверять какие-то свойства безопасности, например, отсутствие зацикливания или блокировки - это свойства безопасности. Но полную функциональную корректность этим методом нельзя (или очень сложно) проверить.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Воскресенье, 04 Ноябрь, 2018 17:41 

Зарегистрирован: Суббота, 07 Март, 2009 15:39
Сообщения: 2933
Откуда: Астрахань
Авторы получили премию Тьюринга за это дело.
Там темпоральные логики - позволяют хоть как-то разрулить проблему
доказательства для параллельных процессов.
Вот исходная работа:
http://bookre.org/reader?file=437236


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 08 Ноябрь, 2018 20:53 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 237
Rifat писал(а):
Начал смотреть на книгу Кушниренко и Лебедева "Программирование для математиков" немного под другим углом. Во многих книгах в качестве предусловия, постусловия, инварианта обычно выступают какие-то арифметические выражения. Но многие вещи очень сложно записать формально, поэтому необходимо записывать эти утверждения как-то неформально на естественном языке. Одно время я искал в гугле и в яндексе и на русском и на английском какие-нибудь источники, где бы были примеры утверждений на естественном языке. В этом плане данная книга - это как раз то, что я искал. Там большинство алгоритмов содержат дано (предусловие), получить (постусловие) и инвариант на естественном языке и служат примером как можно использовать естественный язык для описания утверждений.

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

Постановка задач и определение фактов осуществляется на математическом языке, близком к естественному языку математических публикаций:
Спецификация: http://nevidal.org/download/forthel.pdf
Краткое описание: Особенности обработки математических текстов в системе автоматизированной дедукции

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 08 Ноябрь, 2018 20:58 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 237
Rifat писал(а):
То есть, насколько я понимаю, здесь говорится о том, что метод model checking позволяет проверять какие-то свойства безопасности, например, отсутствие зацикливания или блокировки - это свойства безопасности. Но полную функциональную корректность этим методом нельзя (или очень сложно) проверить.

Кстати, у Глушковцев базис "алгоритма очевидности" повлиял на расширение их "системы алгоритмических алгебр" -- от "статики" (вычислительные алгоритмы по схеме "дано->алгоритм->результат" и их дедуктивная верификация) до "динамики" -- взаимодействующие активные (реактивные) объекты в виде "инсерционного" программирования/моделирования (от "insert" -- активный объект "погружается" в среду). Однако, если часть технологии, которую можно обозвать как "model checking", кое-где используется в промышленности (согласно доступным публикациям первоначально проект расширялся для Мотороллы в рамках задач верификации требований, протоколов взаимодействия), то "полный фарш", по-видимому, есть лишь как академические исследования.
Публикации необходимо выискивать в инете, часть доступна на сайте APS (Algebraic Programming System):
http://www.apsystems.org.ua/

Программирование/моделирование на APLAN -- базовый математический язык в APS -- напоминает предикатное (и автоматное) программирование от В.И. Шелехова, представленное здесь на форуме (или на форуме Дракон-а). Схожесть в том смысле, что применяется "математический программный" язык вместо языка программирования (или необходимого конечного технологического языка моделирования) с дополнительными сопровождающими спецификациями требований и ограничений, и возможен последующий синтез программ/моделей на конечном языке (однако у технологий математический базис разный).


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 24 ]  На страницу Пред.  1, 2

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


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

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


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

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