DRAKON.SU

Текущее время: Воскресенье, 27 Май, 2018 11:05

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




Начать новую тему Ответить на тему  [ Сообщений: 50 ]  На страницу 1, 2, 3  След.
Автор Сообщение
 Заголовок сообщения: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 18 Ноябрь, 2015 22:12 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 74
Формальные методы (Formal methods) базируются на формальной спецификации программ. Данная тема анонсирована в сообщении: http://forum.oberoncore.ru/viewtopic.php?f=140&t=5555#p93861. Цель темы -- дать краткое популярное изложение для всех, кто хотел бы получить представление о формальных методах, применяемых в программной инженерии. Материал будет изложен в виде набора коротких глав.

    Глава 1. Формальные спецификации

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

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

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

В качестве примера, рассмотрим известную программу вычисления наибольшего общего делителя чисел 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 -- квантор всеобщности.

Предусловие определяется формулой:
    nat a, b and a > 0 and b > 0
Здесь описатель nat определяет натуральный тип чисел; "nat a, b" означает, что a и b -- натуральные числа. Формула в целом определяет, что a и b являются натуральными положительными числами.

Чтобы записать формулу для постусловия, необходимо сначала определить подформулу divisor(a, x) для условия "число x является делителем числа a":
    divisor(a, x) = exists nat z > 0. x * z = a
Правая часть формулы определяет, что существует такое число z, которое при умножении на x дает a, т.е. число a делится на x без остатка.
На следующем шаге надо определить подформулу divisor2(a, b, x) для условия "число x является общем делителем для чисел a и b":
    divisor2(a, b, x) = divisor(a, x) and divisor(b, x)
Наконец, записывается формула для постусловия gcd(a, b, c), определяющего, что число c является общим делителем чисел a и b, причем этот делитель наибольший среди других возможных:
    gcd(a, b, c) = divisor2(a, b, c) and forall x. (divisor2(a, b, x) => x ≤ c)

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Четверг, 19 Ноябрь, 2015 15:59 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 208
Откуда: Казань
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 уровне, так как у них нет даже неформальных спецификаций.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Четверг, 19 Ноябрь, 2015 17:53 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
А у меня такой вопрос к коллегам:
Возможно ли на практике работать с формальными требованиями?
Т.е. есть ли у кого реальный положительный опыт, при использовании такого подхода?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Четверг, 19 Ноябрь, 2015 23:22 

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 140
Откуда: Троицк, Москва
ilovb писал(а):
Возможно ли на практике работать с формальными требованиями?
Т.е. есть ли у кого реальный положительный опыт, при использовании такого подхода?

Не вполне понятно, что имеется в виду, но в моём опыте -- чем лучше оформленность и чем точнее требования, тем лучше.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 20 Ноябрь, 2015 00:21 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Я про формальность в строгом математическом смысле.
Т.е. описание требований в виде набора логических формул.
При разработке ПО мы ведь держим в голове все эти [пред/пост]условия, инварианты и утверждения касаемо данной программы/системы или ее части. На практике часто бывает дико трудно объяснить программеру, что он должен реализовать. И наоборот от постановщика часто трудно добиться вменяемого описания того, что он хочет. Во многих таких случаях речь идет о каком-либо логическом утверждении касаемо разрабатываемой системы, и дело сдвигается с мертвой точки как только участники процесса осознают сей факт и родят это самое утверждение.
И в каждом таком случае я крепко задумываюсь почему мы не родили это утверждение с самого начала...!? А дальше приходит мысль, что в сущности система - это и есть набор утверждений об элементах оной, которые мы реализуем (или в рамках которых мы реализуем систему). И в голову не лезет более точного описания системы и хочется иметь такую строгую спецификацию с самого начала. И хочется исправлять архитектурные ошибки еще на этапе анализа этой спецификации. И хочется, чтобы программер имел возможность опереться на эту логическую схему при разработке и тестировании.
В общем много чего хочется, но совершенно непонятно как это можно внедрить на практике. А зуд таки не дает покоя. Каждый раз при реализации очередной программы ловлю себя на мысли, что в голове крутятся буквально формулы. И потом, спустя месяцы и годы я смотрю в свой код и в голове восстанавливаются все те же формулы и в этот момент приходит осознание, что формулы в этом коде вижу только я. А ведь суть написанного то как раз в них... Получается совершенно дурацкая ситуация. При решении задачи я эти инварианты/утверждения etc родил и опираясь на оные реализовал программу/систему. Но в реализации их нет! Они благополучно остались в моей голове. И коллеге придется буквально изучать мою реализацию и восстанавливать эти утверждения уже в своей голове. Все, чем мы реально пользуемся, остается в наших головах, а на материальных носителях у нас только реализация и бредовые неформальные описания на естественном языке.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 20 Ноябрь, 2015 06:52 

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 140
Откуда: Троицк, Москва
Насколько успел понять -- настолько со всем согласен.

ИМХО, сейчас главная "дыра" -- это недоподготовленность обеих сторон (постановщик-программер).
Нужно больше тренажу в формальной (и неформальной) логике.

Навык пользования этим аппаратом должен быть ... квази-врождённым :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 20 Ноябрь, 2015 09:51 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 105
Откуда: Псков
ilovb писал(а):
А у меня такой вопрос к коллегам:
Возможно ли на практике работать с формальными требованиями?
Т.е. есть ли у кого реальный положительный опыт, при использовании такого подхода?

Думаю, что касается предусловий, у многих есть реальный положительный опыт.
А вот по постусловиям сам я пока в большом скепсисе, возможно по дремучести. :) Одно, хотя бы, использование "forall" в логических формулах вызывает ступор - а как их использовать? (PS. Про индукцию я слышал :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 20 Ноябрь, 2015 10:05 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 74
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 уровне, так как у них нет даже неформальных спецификаций.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 20 Ноябрь, 2015 10:55 

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

К сожалению, такого задачника еще нет, и я не учился по нему. Но я использовал неформальную запись предусловий, постусловий и инвариантов в комментариях кода, когда разрабатывал компилятор и линкер Oberon-07M.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 20 Ноябрь, 2015 11:55 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 74
ilovb писал(а):
А у меня такой вопрос к коллегам:
Возможно ли на практике работать с формальными требованиями?
Возможно, но для этого надо владеть формальными методами.
Но сначала надо научиться работать с содержательными требованиями.

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

Цитата:
Я про формальность в строгом математическом смысле.
Т.е. описание требований в виде набора логических формул.
При разработке ПО мы ведь держим в голове все эти [пред/пост]условия, инварианты и утверждения касаемо данной программы/системы или ее части. На практике часто бывает дико трудно объяснить программеру, что он должен реализовать. И наоборот от постановщика часто трудно добиться вменяемого описания того, что он хочет.
Это действительно серьезная проблема, но она относится к другой теме -- инженерии требований.
Подождите, я скоро открою второй ликбез, и там все эти вопросы мы подробно обсудим.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 20 Ноябрь, 2015 12:19 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Спасибо за ссылочку. Расшифруйте еще, пожалуйста: "работать с содержательными требованиями".


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Воскресенье, 22 Ноябрь, 2015 12:01 

Зарегистрирован: Среда, 07 Январь, 2015 14:53
Сообщения: 715
Доклад Владимира Шелехова
"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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Вторник, 24 Ноябрь, 2015 23:34 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Цитата:
В статье есть примеры и обзорная часть, в которой имеется такая информация. Но статья, к сожалению, для специалистов.


Полистал, почитал ... А есть примеры из реальных задач? В статье уж совсем детские.
К примеру нужно поставить программистам задачу на разработку форума типа того, на котором мы тут пишем. Как это сделать по вашей методике? Как описать систему "форум" формально, понятно и достаточно полно? Тут 5-10 состояний автомата не прокатит.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 25 Ноябрь, 2015 00:19 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 105
Откуда: Псков
ilovb писал(а):
Полистал, почитал ...

То же, но за несколько попыток - текст читается с трудом. Собственно говоря, а как , гиперфункции с переходами не вызвали отторжения? У меня вызвало их (переходов ) "глобальность", что внутри г.функции, что снаружи. Может быть, конечно, ничего не понял из задумки.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 25 Ноябрь, 2015 00:55 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Как я понял там тупо машина Тьюринга в новой одежке.
В МТ операции - это печать символов на ленте и сдвиг головки. За операцией следует смена состояния. Т.е. изменяется память и внутреннее состояние.
Гиперфункция - это те же яйца в профиль. Только вместо ленты переменные и чуток императивщины над оными. Кроме того гиперфункция определяет в какое состояние переходим.
Все это во имя строгости окружено пред- и пост-условиями.

Автор поправит если я что-то не так понял.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 25 Ноябрь, 2015 09:16 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 105
Откуда: Псков
Думаю, что упоминание гиперфункции, что машины Тьюринга, в данном конкретном случае мало что даёт. Разве здесь применяется какой-то могучий мат.аппарат. Речь идёт всё же о конкретном практическом подходе к автоматному программированию, и, к тому же, не о какой-то супер-новизне.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 25 Ноябрь, 2015 09:46 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Так МТ - это и есть автоматное программирование. Тут то же самое, только чуток уровнем повыше.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 25 Ноябрь, 2015 09:56 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 105
Откуда: Псков
ilovb писал(а):
Так МТ - это и есть автоматное программирование. Тут то же самое, только чуток уровнем повыше.

Не надо отождествлять "конечный автомат" и "автоматное программирование"


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 25 Ноябрь, 2015 10:04 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Почему это?

Это же старый интернет-баян. Некий Шалыто взял автомат, добавил свистульки и назвал это новой технологией программирования.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 25 Ноябрь, 2015 10:09 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 105
Откуда: Псков
ilovb писал(а):
Почему это?

Это же старый интернет-баян. Некий Шалыто взял автомат, добавил свистульки и назвал это новой технологией программирования.

Напрасно иронизируете, весьма съедобная вещь :) И книжка "Автоматное программирование" хорошая.

PS.
Главное, надо относиться ко всему без фанатизма, больше пользы можно извлечь из чужого опыта:)


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

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


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

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


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

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