МФСП, 05 лекция (от 01 октября)

Материал из eSyr's wiki.

(Различия между версиями)
Перейти к: навигация, поиск
(Новая: Средств спецификции в современных ЯП * Расшир. взм. мделир. * Упрщение формльного анлиз * Сближение с Я...)
 
(2 промежуточные версии не показаны)
Строка 1: Строка 1:
-
Средств спецификции в современных ЯП
+
Средства спецификации в современных ЯП
-
* Расшир. взм. мделир.
+
* Расширение взаимного моделирования
-
* Упрщение формльного анлиз
+
* Упрощение формального анализа
* Сближение с ЯП
* Сближение с ЯП
* ООП
* ООП
-
* Прллелизм. синхронное взимдействие. Естественн, метды обмен информцией. В каждом новом языке сепециф. осн. внимние уделяется не всем возм. рсш., а ккму-т дст. узкрому клссу рсш. Если язык спец. исп. для пис. арх. систем рельнго времени со сложными хр-ками, большик кол-вом процессов, но бедным инф. бменм, тм много будет уделено внимния этим мехнизмам, а ... уделен не будет.
+
* Параллелизм. синхронное взаимодействие. Естественные, методы обмен информацией. В каждом новом языке спецификации основное внимание уделяется не всем возможным расширениям, а какому-то достаточно узкому классу расширений. Если язык спецификации используется для описания архитектуры систем реального времени со сложными характеристиками, большик количеством процессов, но бедным информационным обменом, там много будет уделено внимания этим механизмам, а уделен не будет.
-
Сейчас всеобщ. языка спец. нет, они бльшей чстью спец.
+
Сейчас всеобщего языка спецификации нет, они большей частью специализированные.
-
Это не знчит, чт это истин в плсл. инфт., всё развивается циклически, и сейчас имеется большое кл-во языкв, кажый из кторых продв. свё нпр., и чт будет лет через 5---10, неизвестно.
+
Это не значит, что это истина в последней инстанции, всё развивается циклически, и сейчас имеется большое количество языков, каждый из которых продвигает своё направление, и что будет лет через 5—10, неизвестно.
-
* Временные или темп. св-ва. Описание тких свойств. Отдельня тема. Дст. тесн связ. с прлл. Далек не все языки это пдд., н некрые активно рзв. эту блсть.
+
* Временны́е или темпоральные свойства. Описание таких свойств — отдельная тема. Достаточно тесно связана с приложениями. Далеко не все языки это поддерживают, некоторые активно развивают эту область.
-
Пявляются сейчас дост. экз. нпрвления, нпример
+
Появляются сейчас достаточно экзотические направления, например
-
* Спецификция требовния к ресурсам. Объём выч., бъём пмяти, мжет быть вещи, связ с периферией, мгут быть требвания, связ. с кл. и кнф. прцессоров. Задча при спец. ресусов дост. слжня, кнечн, птму что когд систему кмпозируете, сложно скзать, скольк ресурсов нужно конкретному объекту или клссу. Сттически предскзть, скольк ресурсв потр. каждму и в совокупности, очень сложно. С одной стороны, эта тем отдельня, с другой, для оценки необх. отслеж. связь с фукнкц.
+
* Спецификация требований к ресурсам. Объём вычислений, объём памяти, может быть вещи, связанные с периферией, могут быть требования, связанные с классификацией и конфигурацией процессоров. Задача при спецификации ресурсов достаточно сложная, конечно, потому что когда систему композируете, сложно сказать, сколько ресурсов нужно конкретному объекту или классу. Сттически предсказать, сколько ресурсов потребуется каждому и в совокупности, очень сложно. С одной стороны, это тема отдельная, с другой, для оценки необходимо отслеживать связь с функциональностью.
 +
* Тема безопасности. Совсем неспецифицирована, поскольку сейчас все этой проблемой озабочены. Это серьёзная вещь и хочется рассмотреть разные стороны описания системы как независимые аспекты, в частности, хотелось бы безопасность отделить от функциональности, но это удаётся далеко не всегда.
 +
Есть некие совсем экзотические темы, например:
 +
* Спецификация ответственности. В больших системах всегда достаточно высокая вероятность отказа, а взаимоотношения между потребителями некоторых услуг и провайдерами ресурсом джлжны быть достаточно ясны. Если клиент за что-то заплатил и ему это предоставляется, то всё хорошо, если не предоставляется, то как эту коллизию разрешить. Провайдер, который выступает перед клиентом, теоретически мог бы взять ответственность за всё ПО, за весь компьютерный парк, за сетевые возможности и так далее. Но провайдер не хочет и не может сделать этого, он хочет ответственности только за то, что может отвечать. Тут возникает субподрядчик, который и должен отвечать. И взаимоотношения этих бяз, если бы ни были описаны, и если бы был бы механизм разбора инцидентов, то это была бы неплохая практика страховых компаний.
-
* Тем безопсности. Свсем неспециф., пскольку сейчас все этй прблмой озбчены. Эт серьёзня вещь и хчется рссм. розные строны опис. системы как нез. спекты, в чстнсти, хтелось бы безоп. тд. от функц, но это удаётся длеко не всегда.
+
Что можно было бы сказать по части упрощённого анализа? Указанное выше — тенденция к усложению языков спецификации
-
 
+
-
Есть некие свсем экз. темы, наз.
+
-
* Спецификация ответственности. В больших системх всегд дост. высокая вер. тказа, а взаимотн. междлу потр. некоторых услуг и првайдерм ресурсом джлжны быть дост. ясны. Если клиент з чт-то заплтил и ему эт предост., т всё ъхрошо, если не предост, то кк эту коллизию рзреш. Првйдер, который выст. перед гентм, теор. мг бы взять тветственнсть за всё по, хз весь комп. парк, з сетевые возм. и тк длее. Н првйдер не хчет и не мжет сделть этого, олн хочет отв. только з то, что может твечать. Тут возн. субпдрядчик, кторый и длжен твечать. И взаимотн. этих бяз, если бы ни были описаны, и если бы был бы мехнизм разбра инцидентв, то это была бы неплохя прктика страхвых кмпаний.
+
-
 
+
-
Что можно было бы скзать по части упрощ. анализ? Указанное выше — тенденция к услож. языкв специф.
+
* Функциональные языки
* Функциональные языки
-
* Упрощ. система типов
+
* Упрощённая система типов
-
* Строгя семнтика
+
* Строгая семантика
-
* Платфрмонез. спец.
+
* Платформонезависимая спецификация
-
Приняли реш., что языкми спец. польз. не будем, берём хороший язык пргр. и дп. его эл-тми спец.: дбвляем пред, пст усл. и инвринты.
+
Приняли решение, что языками спецификации пользоваться не будем, берём хороший язык программирования и дополняем его элементами спецификации: добавляем предусловия, постусловия и инвринты.
Spec#
Spec#
-
* Рсширение C#
+
* Расширение C#
-
* Кмпилятор
+
* Компилятор
-
* Верификтор — Boogie
+
* Верификатор — Boogie
-
* SpecEcxplorer
+
* SpecExplorer
-
прект бесплтный, но не ткрытый. Для пркт. пргрммиста это не совсем новый язык, а расширение известного. Выявляется дст. ширкий класс ошщибк за счёт исп. рзл. техник.
+
прект бесплатный, но не открытый. Для программиста-практика это не совсем новый язык, а расширение известного. Выявляется достаточно широкий класс ошибок за счёт использования различных техник.
-
Пример тог, кк выгдл, предусловие:
+
Пример того, как выглядит, предусловие:
'''class''' ArrayList
'''class''' ArrayList
{
{
Строка 47: Строка 45:
}
}
}
}
-
В этом случе, если пдётся неке число, выход. з рамки грницы, выдётся предопр. иск., никк не окрш: requuires violation exception. Пр исключения и пр трактовку предусл. стит сказать тдельно. Рзрб. след. трктвке искл., ктря был ещё их предш. предлжен, и трктовк искл. следующя: исключения трактуются как ткз. Эти откзы бывают двух видов: клиентские и провайдерские. Клиентские — клиент нер. обр. к метду, иил когд релиз. метода сделн не тк, плучился тказ. Провайдесркие тказы в свю очередь делятся ещё н два клсса: admissible — допустимые ткзы, и observed program error. Первый и псл. вид — unchecked исключения, второй, единственный — checked. Любя пргр. длжн ожидть ткие жидемые искл. и опис., чт при этом делть. Если взн. unchecked, т зн., что релиз. некорр.
+
В этом случае, если попадается некое число, выходящее за рамки границы, выдаётся предопределённое исключение, никак не окрш: requires violation exception. Про исключения и прочую трактовку предусловий стоит сказать отдельно. Разработчики следуют трактовке исключений, которая была ещё их предшественниками предложена, и трактовка исключений следующая: исключения трактуются как отказы. Эти отказы бывают двух видов: клиентские и провайдерские. Клиентские — клиент неправильно обращается к методу, или когда реализация метода не сделана или некорректна. Провайдерские отказы, в свою очередь, делятся ещё н два класса: admissible — допустимые отказы, и observed program error. Первый и последующий виды — unchecked исключения, второй, единственный — checked. Любая программа должна ожидать такие ожидаемые исключения и описывать, что при этом делать. Если возникло unchecked, то значит, что реализация некорректна.
-
Пример пис. admissible исключения:
+
Пример описания admissible исключения:
'''class''' ArrayList
'''class''' ArrayList
{
{
Строка 62: Строка 60:
}
}
-
Пстусловие:
+
Постусловие:
'''ensures''' Count=='''old'''(Count) + 1;
'''ensures''' Count=='''old'''(Count) + 1;
'''ensures''' value==this[index];
'''ensures''' value==this[index];
Строка 68: Строка 66:
'''ensures''' Forall{'''int''' i '''in''' index:'''old'''(Count): '''old'''(this[i])==this[i+1]}
'''ensures''' Forall{'''int''' i '''in''' index:'''old'''(Count): '''old'''(this[i])==this[i+1]}
-
Для постусловаия важнй бывет ситуация,кгд выд. кке искл, нужно сказть, чт вып., что не вып. Чт релиз. должн грантирвать? Если я рбтю с нек. файлом
+
Для постусловия важной бывает ситуация, когда выдаётся какое-то исключение, нужно сказать, что выполняется, что не выполняется. Что реализация должна гарантировать? Если я работаю с некоторым файлом
'''throws''' EndOFileException '''ensure''' a.Count==old(a.Count); {...}
'''throws''' EndOFileException '''ensure''' a.Count==old(a.Count); {...}
Минусы:
Минусы:
-
* Нет обратной свместимости
+
* Нет обратной совместимости
-
* Спец. с реализ.
+
* Спецификация с реализацией
Плюсы:
Плюсы:
* Библиотеки
* Библиотеки
-
* Единя система типв
+
* Единая система типов
-
* Пдхд deign by contract
+
* Подходит для design by contract
(тут история)
(тут история)
Строка 85: Строка 83:
* 99 - JML
* 99 - JML
* 2003 --- Spec#
* 2003 --- Spec#
-
* Конец 90-х (примерн 98; первые идеи в рйне 72 года) --- Extended Static Checker (ESC). Идея: когда мы гворили про пред и пст-усл, то считли, чт пракильное пвед. писн там. Есть другой пдхд: прграмма крректн, если в ней нет дурцких ошибок. Этот пдход релизация этй идеи, и до посл. времени эти нлиз. и вериф., ктрые прверял корр. требваний и ... были дв незв. набор инстр. Сейчас две эти техники боъединены.
+
* Конец 90-х (примерно 98; первые идеи в районе 72 года) --- Extended Static Checker (ESC). Идея: когда мы говорили про предусловия и постусловия, то считали, что правильное поведение описано там. Есть другой подход: программа корректна, если в ней нет дурацких ошибок. Этот подход реализация этой идеи, и до после времени эти анализаторы и верификаторы, которые проверяли корректность требований и были два независимых набора инструментов. Сейчас две эти техники объединены.
-
Те техникивериф, с которыми в втрой ччсти сем. позн., это именн те техники, н к-рых ... бзир.
+
Те техники верификации, с которыми во второй части сем. позн., это именно те техники, на которых … базируется ….
{{МФСП}}
{{МФСП}}
{{Lection-stub}}
{{Lection-stub}}

Текущая версия

Средства спецификации в современных ЯП

  • Расширение взаимного моделирования
  • Упрощение формального анализа
  • Сближение с ЯП
  • ООП
  • Параллелизм. синхронное взаимодействие. Естественные, методы обмен информацией. В каждом новом языке спецификации основное внимание уделяется не всем возможным расширениям, а какому-то достаточно узкому классу расширений. Если язык спецификации используется для описания архитектуры систем реального времени со сложными характеристиками, большик количеством процессов, но бедным информационным обменом, там много будет уделено внимания этим механизмам, а … уделен не будет.

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

Это не значит, что это истина в последней инстанции, всё развивается циклически, и сейчас имеется большое количество языков, каждый из которых продвигает своё направление, и что будет лет через 5—10, неизвестно.

  • Временны́е или темпоральные свойства. Описание таких свойств — отдельная тема. Достаточно тесно связана с приложениями. Далеко не все языки это поддерживают, некоторые активно развивают эту область.

Появляются сейчас достаточно экзотические направления, например

  • Спецификация требований к ресурсам. Объём вычислений, объём памяти, может быть вещи, связанные с периферией, могут быть требования, связанные с классификацией и конфигурацией процессоров. Задача при спецификации ресурсов достаточно сложная, конечно, потому что когда систему композируете, сложно сказать, сколько ресурсов нужно конкретному объекту или классу. Сттически предсказать, сколько ресурсов потребуется каждому и в совокупности, очень сложно. С одной стороны, это тема отдельная, с другой, для оценки необходимо отслеживать связь с функциональностью.
  • Тема безопасности. Совсем неспецифицирована, поскольку сейчас все этой проблемой озабочены. Это серьёзная вещь и хочется рассмотреть разные стороны описания системы как независимые аспекты, в частности, хотелось бы безопасность отделить от функциональности, но это удаётся далеко не всегда.

Есть некие совсем экзотические темы, например:

  • Спецификация ответственности. В больших системах всегда достаточно высокая вероятность отказа, а взаимоотношения между потребителями некоторых услуг и провайдерами ресурсом джлжны быть достаточно ясны. Если клиент за что-то заплатил и ему это предоставляется, то всё хорошо, если не предоставляется, то как эту коллизию разрешить. Провайдер, который выступает перед клиентом, теоретически мог бы взять ответственность за всё ПО, за весь компьютерный парк, за сетевые возможности и так далее. Но провайдер не хочет и не может сделать этого, он хочет ответственности только за то, что может отвечать. Тут возникает субподрядчик, который и должен отвечать. И взаимоотношения этих бяз, если бы ни были описаны, и если бы был бы механизм разбора инцидентов, то это была бы неплохая практика страховых компаний.

Что можно было бы сказать по части упрощённого анализа? Указанное выше — тенденция к усложению языков спецификации

  • Функциональные языки
  • Упрощённая система типов
  • Строгая семантика
  • Платформонезависимая спецификация

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

Spec#

  • Расширение C#
  • Компилятор
  • Верификатор — Boogie
  • SpecExplorer

прект бесплатный, но не открытый. Для программиста-практика это не совсем новый язык, а расширение известного. Выявляется достаточно широкий класс ошибок за счёт использования различных техник.

Пример того, как выглядит, предусловие:

class ArrayList
{
  public virtual void Insert(int index, obect value)
    requires 0 <= index && index <= Count;
    requires !IsReadOnly && !IsixedSize;
  {
    ...
  }
}

В этом случае, если попадается некое число, выходящее за рамки границы, выдаётся предопределённое исключение, никак не окрш: requires violation exception. Про исключения и прочую трактовку предусловий стоит сказать отдельно. Разработчики следуют трактовке исключений, которая была ещё их предшественниками предложена, и трактовка исключений следующая: исключения трактуются как отказы. Эти отказы бывают двух видов: клиентские и провайдерские. Клиентские — клиент неправильно обращается к методу, или когда реализация метода не сделана или некорректна. Провайдерские отказы, в свою очередь, делятся ещё н два класса: admissible — допустимые отказы, и observed program error. Первый и последующий виды — unchecked исключения, второй, единственный — checked. Любая программа должна ожидать такие ожидаемые исключения и описывать, что при этом делать. Если возникло unchecked, то значит, что реализация некорректна.

Пример описания admissible исключения:

class ArrayList
{
  public virtual void Insert(int index, obect value)
    requires 0 <= index && index <= Count
      otherwise ArgumentOutORangeException;
    requires !IsReadOnly && !IsixedSize
      otherwise NotSupportedException;
  {
    ...
  }
}

Постусловие:

ensures Count==old(Count) + 1;
ensures value==this[index];
ensures Forall{int i in 0:index: old(this[i])==this[i]}
ensures Forall{int i in index:old(Count): old(this[i])==this[i+1]}

Для постусловия важной бывает ситуация, когда выдаётся какое-то исключение, нужно сказать, что выполняется, что не выполняется. Что реализация должна гарантировать? Если я работаю с некоторым файлом

throws EndOFileException ensure a.Count==old(a.Count); {...}

Минусы:

  • Нет обратной совместимости
  • Спецификация с реализацией

Плюсы:

  • Библиотеки
  • Единая система типов
  • Подходит для design by contract

(тут история)

  • 75 --- Gypsy
  • 80-90 Eiel, Spark
  • 99 - JML
  • 2003 --- Spec#
  • Конец 90-х (примерно 98; первые идеи в районе 72 года) --- Extended Static Checker (ESC). Идея: когда мы говорили про предусловия и постусловия, то считали, что правильное поведение описано там. Есть другой подход: программа корректна, если в ней нет дурацких ошибок. Этот подход — реализация этой идеи, и до после времени эти анализаторы и верификаторы, которые проверяли корректность требований и … были два независимых набора инструментов. Сейчас две эти техники объединены.

Те техники верификации, с которыми во второй части сем. позн., это именно те техники, на которых … базируется ….


Формальная спецификация и верификация программ


Лекции

01 02 03 04 05 06 07 08 09 10 11 12 13 14


Календарь

Сентябрь
03 10 17 24
Октябрь
01 08 15 22 29
Ноябрь
12 19 26
Декабрь
03 17
Семинары

01 02 03 04 05 06


Календарь

Сентябрь
01 08 15 22 29
Октябрь
06

Оформление задач|Проведение экзамена


Эта статья является конспектом лекции.

Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
Личные инструменты
Разделы