DRAKON.SU https://forum.drakon.su/ |
|
Формальные методы. Ликбез https://forum.drakon.su/viewtopic.php?f=140&t=5568 |
Страница 1 из 3 |
Автор: | Владимир Шелехов [ Среда, 18 Ноябрь, 2015 22:12 ] |
Заголовок сообщения: | Формальные методы. Ликбез |
Формальные методы (Formal methods) базируются на формальной спецификации программ. Данная тема анонсирована в сообщении: http://forum.oberoncore.ru/viewtopic.php?f=140&t=5555#p93861. Цель темы -- дать краткое популярное изложение для всех, кто хотел бы получить представление о формальных методах, применяемых в программной инженерии. Материал будет изложен в виде набора коротких глав.
Спецификация программы -- декларативное описание, определяющее программу в целом, в частности интерфейс программы с пользователем. Спецификация -- внешнее описание программы, абстрагированное от особенностей ее реализации. Рассмотрим сначала программы-функции, у которых взаимодействие с окружением программы ограничивается вводом входных данных и выводом результатов вычисления; других взаимодействий с окружением нет. Спецификация программы-функции состоит из предусловия и постусловия. Предусловие -- набор условий, определяющих область входных данных. Постусловие -- набор условий, определяющих связи между значениями входных данных и результатов. Спецификация определяет условие математической задачи, решением которой является программа-функция. Исходные переменные задачи соответствуют входным данным, а неизвестные переменные -- результатам программы. В качестве примера, рассмотрим известную программу вычисления наибольшего общего делителя чисел a и b: Код: loop { if (a == b) return a; if (a < b) b = b – a else a = a – b } Спецификация программы представлена фразой "наибольший общий делитель". Делитель -- известное математическое понятие, и поэтому данная фраза вроде бы должна иметь строгий математический смысл. Однако при a = 0 и b = 1.5 программа не работает. Делитель, как известно, второй операнд в операции деления. Оказывается, нет. Здесь подразумевается совсем другое понятие делителя в смысле делимости нацело, причем это свойство определено только для целых чисел. Значит, что значение b = 1.5 не годится. Далее, делитель для a = 0 смысла не имеет. Таким образом, содержательная формулировка спецификации в виде текста на русском языке может содержать различного рода неточности, которые потенциально могут привести к неверной программе. Чтобы избежать этого, необходимо использовать формальные спецификации в виде набора логических формул на одном из строгих языков спецификаций. Таких языков много. Наиболее известные из них: VDM, Z, B. Представим формальную спецификацию программы наибольшего общего делителя на некотором языке спецификаций, который определен здесь с учетом ограниченного алфавита допустимых литер в сообщениях Форума. В языке спецификаций используются следующие обозначения: and -- конъюнкция, => -- импликация, exists -- квантор существования, forall -- квантор всеобщности. Предусловие определяется формулой:
Чтобы записать формулу для постусловия, необходимо сначала определить подформулу divisor(a, x) для условия "число x является делителем числа a":
На следующем шаге надо определить подформулу divisor2(a, b, x) для условия "число x является общем делителем для чисел a и b":
Формальные спецификации программ являются обязательными для всех видов формальных методов, проверяющих корректность программ относительно спецификаций применением различного вида инструментов доказательства теорем, представленных формулами на языке спецификаций. |
Автор: | Rifat [ Четверг, 19 Ноябрь, 2015 15:59 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
Jonathan P. Bowen (London South Bank University) и Michael G. Hinchey (NASA Software Engineering Laboratory) в статье "Ten Commandments of Formal Methods ... Ten Years Later" выделяют несколько уровней использования формальных методов: Уровень 0 - Формальные спецификации. Использование формальной нотации только для описания требований без анализа и доказательств. Уровень 1 - Формальная разработка/верификация. Доказательство свойств и использование исчисления уточнений (refinement calculus). Уровень 2 - Доказательства проверяемые машиной. Использование доказателя теорем для доказательства согласованности. Насколько я понимаю, большинство фирм на сегодняшний день находятся на -1 уровне, так как у них нет даже формальных спецификаций, а есть только неформальные спецификации. А некоторые фирмы находятся даже на -2 уровне, так как у них нет даже неформальных спецификаций. |
Автор: | ilovb [ Четверг, 19 Ноябрь, 2015 17:53 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
А у меня такой вопрос к коллегам: Возможно ли на практике работать с формальными требованиями? Т.е. есть ли у кого реальный положительный опыт, при использовании такого подхода? |
Автор: | Info21 [ Четверг, 19 Ноябрь, 2015 23:22 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
ilovb писал(а): Возможно ли на практике работать с формальными требованиями? Т.е. есть ли у кого реальный положительный опыт, при использовании такого подхода? Не вполне понятно, что имеется в виду, но в моём опыте -- чем лучше оформленность и чем точнее требования, тем лучше. Правда, есть задачи по природе плохо поставленные (новые-небывалие). И есть, наверное, оптимальный предел формалистики, но до него нужно еще дойти. В реальности формализму обычно не хватает. |
Автор: | ilovb [ Пятница, 20 Ноябрь, 2015 00:21 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
Я про формальность в строгом математическом смысле. Т.е. описание требований в виде набора логических формул. При разработке ПО мы ведь держим в голове все эти [пред/пост]условия, инварианты и утверждения касаемо данной программы/системы или ее части. На практике часто бывает дико трудно объяснить программеру, что он должен реализовать. И наоборот от постановщика часто трудно добиться вменяемого описания того, что он хочет. Во многих таких случаях речь идет о каком-либо логическом утверждении касаемо разрабатываемой системы, и дело сдвигается с мертвой точки как только участники процесса осознают сей факт и родят это самое утверждение. И в каждом таком случае я крепко задумываюсь почему мы не родили это утверждение с самого начала...!? А дальше приходит мысль, что в сущности система - это и есть набор утверждений об элементах оной, которые мы реализуем (или в рамках которых мы реализуем систему). И в голову не лезет более точного описания системы и хочется иметь такую строгую спецификацию с самого начала. И хочется исправлять архитектурные ошибки еще на этапе анализа этой спецификации. И хочется, чтобы программер имел возможность опереться на эту логическую схему при разработке и тестировании. В общем много чего хочется, но совершенно непонятно как это можно внедрить на практике. А зуд таки не дает покоя. Каждый раз при реализации очередной программы ловлю себя на мысли, что в голове крутятся буквально формулы. И потом, спустя месяцы и годы я смотрю в свой код и в голове восстанавливаются все те же формулы и в этот момент приходит осознание, что формулы в этом коде вижу только я. А ведь суть написанного то как раз в них... Получается совершенно дурацкая ситуация. При решении задачи я эти инварианты/утверждения etc родил и опираясь на оные реализовал программу/систему. Но в реализации их нет! Они благополучно остались в моей голове. И коллеге придется буквально изучать мою реализацию и восстанавливать эти утверждения уже в своей голове. Все, чем мы реально пользуемся, остается в наших головах, а на материальных носителях у нас только реализация и бредовые неформальные описания на естественном языке. |
Автор: | Info21 [ Пятница, 20 Ноябрь, 2015 06:52 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
Насколько успел понять -- настолько со всем согласен. ИМХО, сейчас главная "дыра" -- это недоподготовленность обеих сторон (постановщик-программер). Нужно больше тренажу в формальной (и неформальной) логике. Навык пользования этим аппаратом должен быть ... квази-врождённым |
Автор: | albobin [ Пятница, 20 Ноябрь, 2015 09:51 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
ilovb писал(а): А у меня такой вопрос к коллегам: Возможно ли на практике работать с формальными требованиями? Т.е. есть ли у кого реальный положительный опыт, при использовании такого подхода? Думаю, что касается предусловий, у многих есть реальный положительный опыт. А вот по постусловиям сам я пока в большом скепсисе, возможно по дремучести. Одно, хотя бы, использование "forall" в логических формулах вызывает ступор - а как их использовать? (PS. Про индукцию я слышал |
Автор: | Владимир Шелехов [ Пятница, 20 Ноябрь, 2015 10:05 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
Rifat писал(а): Jonathan P. Bowen (London South Bank University) и Michael G. Hinchey (NASA Software Engineering Laboratory) в статье "Ten Commandments of Formal Methods ... Ten Years Later" выделяют несколько уровней использования формальных методов: Спасибо за ссылку на интересную статью. Хотя здесь две статьи малоизвестных авторов: 10 заповедей по формальным методам 1995г. и Ревизия 10 заповедей 2005г., оформленных в фольклорном стиле с подражанием известному брэнду. Но них почти никто не ссылается. Логично было бы появление их третьей статьи в этом году, отражающей существенный прогресс за последние 10 лет, в частности, обусловленный SMT-решателями. На мой взгляд, в этих статьях много спорного, а с чем-то я просто не согласен.Rifat писал(а): Jonathan P. Bowen и Michael G. Hinchey ... выделяют несколько уровней использования формальных методов: Уровень 0 - Формальные спецификации. Использование формальной нотации только для описания требований без анализа и доказательств. Уровень 1 - Формальная разработка/верификация. Доказательство свойств и использование исчисления уточнений (refinement calculus). Уровень 2 - Доказательства проверяемые машиной. Использование доказателя теорем для доказательства согласованности. Насколько я понимаю, большинство фирм на сегодняшний день находятся на -1 уровне, так как у них нет даже формальных спецификаций, а есть только неформальные спецификации. А некоторые фирмы находятся даже на -2 уровне, так как у них нет даже неформальных спецификаций. Здесь я с Вами соглашусь. И беда в том, что неформальные спецификации, если они есть, часто очень плохого качества. |
Автор: | Rifat [ Пятница, 20 Ноябрь, 2015 10:55 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
А.П. Ершов в статье "Предварительные соображения о лексиконе программирования" писал: "Давайте вообразим, ....Доказательное программирование является основой курса программирования, подкрепленного каторжным тренингом в духе лучших задачников по математическому анализу. Программиста бьют по рукам, если он посмеет написать оператор цикла, не найдя перед этим его инварианта." К сожалению, такого задачника еще нет, и я не учился по нему. Но я использовал неформальную запись предусловий, постусловий и инвариантов в комментариях кода, когда разрабатывал компилятор и линкер Oberon-07M. Сейчас я знаю больше формальных методов записи и стараюсь применять эти формы записи, но это не просто. Возникает много вопросов по ходу программирования, допустим, встретился, линейный список, как его записать формально. Если начать углубляться в литературу, то в одной книге линейный список формально определяется одним способом, в современных публикациях используется много разных "эспериментальных" подходов, к обозначению, различные Shape Analysis и другие. Многие из этих методов не расчитаны на применение средним программистом, а расчитаны видимо только на публикацию в научном издании или же защиту диссертации. |
Автор: | Владимир Шелехов [ Пятница, 20 Ноябрь, 2015 11:55 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
ilovb писал(а): А у меня такой вопрос к коллегам: Возможно, но для этого надо владеть формальными методами.Возможно ли на практике работать с формальными требованиями? Но сначала надо научиться работать с содержательными требованиями. Цитата: Т.е. есть ли у кого реальный положительный опыт, при использовании такого подхода? В статье есть примеры и обзорная часть, в которой имеется такая информация. Но статья, к сожалению, для специалистов.Цитата: Я про формальность в строгом математическом смысле. Это действительно серьезная проблема, но она относится к другой теме -- инженерии требований.Т.е. описание требований в виде набора логических формул. При разработке ПО мы ведь держим в голове все эти [пред/пост]условия, инварианты и утверждения касаемо данной программы/системы или ее части. На практике часто бывает дико трудно объяснить программеру, что он должен реализовать. И наоборот от постановщика часто трудно добиться вменяемого описания того, что он хочет. Подождите, я скоро открою второй ликбез, и там все эти вопросы мы подробно обсудим. |
Автор: | ilovb [ Пятница, 20 Ноябрь, 2015 12:19 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
Спасибо за ссылочку. Расшифруйте еще, пожалуйста: "работать с содержательными требованиями". |
Автор: | LKom [ Воскресенье, 22 Ноябрь, 2015 12:01 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
Доклад Владимира Шелехова "TMPA-2014: Optimization of Automata Based Programs by means of Requirements Transformation Method", "Разработка автоматных программ методом трансформации требований" - http://www.youtube.com/watch?v=p2Am_NaRJI4 Время: 10:30 о планах использовать Дракон 11:30 реплика из зала - "идеолог Дракона по образованию психолог" ---- Смотрите - http://forum.oberoncore.ru/viewtopic.php?p=89744#p89744 |
Автор: | ilovb [ Вторник, 24 Ноябрь, 2015 23:34 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
Цитата: В статье есть примеры и обзорная часть, в которой имеется такая информация. Но статья, к сожалению, для специалистов. Полистал, почитал ... А есть примеры из реальных задач? В статье уж совсем детские. К примеру нужно поставить программистам задачу на разработку форума типа того, на котором мы тут пишем. Как это сделать по вашей методике? Как описать систему "форум" формально, понятно и достаточно полно? Тут 5-10 состояний автомата не прокатит. |
Автор: | albobin [ Среда, 25 Ноябрь, 2015 00:19 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
ilovb писал(а): Полистал, почитал ... То же, но за несколько попыток - текст читается с трудом. Собственно говоря, а как , гиперфункции с переходами не вызвали отторжения? У меня вызвало их (переходов ) "глобальность", что внутри г.функции, что снаружи. Может быть, конечно, ничего не понял из задумки. |
Автор: | ilovb [ Среда, 25 Ноябрь, 2015 00:55 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
Как я понял там тупо машина Тьюринга в новой одежке. В МТ операции - это печать символов на ленте и сдвиг головки. За операцией следует смена состояния. Т.е. изменяется память и внутреннее состояние. Гиперфункция - это те же яйца в профиль. Только вместо ленты переменные и чуток императивщины над оными. Кроме того гиперфункция определяет в какое состояние переходим. Все это во имя строгости окружено пред- и пост-условиями. Автор поправит если я что-то не так понял. |
Автор: | albobin [ Среда, 25 Ноябрь, 2015 09:16 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
Думаю, что упоминание гиперфункции, что машины Тьюринга, в данном конкретном случае мало что даёт. Разве здесь применяется какой-то могучий мат.аппарат. Речь идёт всё же о конкретном практическом подходе к автоматному программированию, и, к тому же, не о какой-то супер-новизне. |
Автор: | ilovb [ Среда, 25 Ноябрь, 2015 09:46 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
Так МТ - это и есть автоматное программирование. Тут то же самое, только чуток уровнем повыше. |
Автор: | albobin [ Среда, 25 Ноябрь, 2015 09:56 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
ilovb писал(а): Так МТ - это и есть автоматное программирование. Тут то же самое, только чуток уровнем повыше. Не надо отождествлять "конечный автомат" и "автоматное программирование" |
Автор: | ilovb [ Среда, 25 Ноябрь, 2015 10:04 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
Почему это? Это же старый интернет-баян. Некий Шалыто взял автомат, добавил свистульки и назвал это новой технологией программирования. |
Автор: | albobin [ Среда, 25 Ноябрь, 2015 10:09 ] |
Заголовок сообщения: | Re: Формальные методы. Ликбез |
ilovb писал(а): Почему это? Это же старый интернет-баян. Некий Шалыто взял автомат, добавил свистульки и назвал это новой технологией программирования. Напрасно иронизируете, весьма съедобная вещь И книжка "Автоматное программирование" хорошая. PS. Главное, надо относиться ко всему без фанатизма, больше пользы можно извлечь из чужого опыта:) |
Страница 1 из 3 | Часовой пояс: UTC + 3 часа |
Powered by phpBB® Forum Software © phpBB Group https://www.phpbb.com/ |