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

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

Версия 21:56, 29 сентября 2010

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

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

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

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

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

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

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

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

Есть некие свсем экз. темы, наз.

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

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

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

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

Spec#

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

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

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

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

В этом случе, если пдётся неке число, выход. з рамки грницы, выдётся предопр. иск., никк не окрш: requuires 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); {...}

Минусы:

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

Плюсы:

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

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

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

Те техникивериф, с которыми в втрой ччсти сем. позн., это именн те техники, н к-рых ... бзир.