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

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

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

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

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

Это не значит, что это истина в последней инстанции, всё развивается циклически, и сейчас имеется большое количество языков, каждый из которых продвигает своё направление, и что будет лет через 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). Идея: когда мы гворили про пред и пст-усл, то считли, чт пракильное пвед. писн там. Есть другой пдхд: прграмма крректн, если в ней нет дурцких ошибок. Этот пдход — релизация этй идеи, и до посл. времени эти нлиз. и вериф., ктрые прверял корр. требваний и ... были дв незв. набор инстр. Сейчас две эти техники боъединены.

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