Редактирование: МФСП, 05 лекция (от 01 октября)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 1: | Строка 1: | ||
- | + | Средств спецификции в современных ЯП | |
- | * | + | * Расшир. взм. мделир. |
- | * | + | * Упрщение формльного анлиз |
* Сближение с ЯП | * Сближение с ЯП | ||
* ООП | * ООП | ||
- | * | + | * Прллелизм. синхронное взимдействие. Естественн, метды обмен информцией. В каждом новом языке сепециф. осн. внимние уделяется не всем возм. рсш., а ккму-т дст. узкрому клссу рсш. Если язык спец. исп. для пис. арх. систем рельнго времени со сложными хр-ками, большик кол-вом процессов, но бедным инф. бменм, тм много будет уделено внимния этим мехнизмам, а ... уделен не будет. |
- | Сейчас | + | Сейчас всеобщ. языка спец. нет, они бльшей чстью спец. |
- | Это не | + | Это не знчит, чт это истин в плсл. инфт., всё развивается циклически, и сейчас имеется большое кл-во языкв, кажый из кторых продв. свё нпр., и чт будет лет через 5---10, неизвестно. |
- | * | + | * Временные или темп. св-ва. Описание тких свойств. Отдельня тема. Дст. тесн связ. с прлл. Далек не все языки это пдд., н некрые активно рзв. эту блсть. |
- | + | Пявляются сейчас дост. экз. нпрвления, нпример | |
- | * | + | * Спецификция требовния к ресурсам. Объём выч., бъём пмяти, мжет быть вещи, связ с периферией, мгут быть требвания, связ. с кл. и кнф. прцессоров. Задча при спец. ресусов дост. слжня, кнечн, птму что когд систему кмпозируете, сложно скзать, скольк ресурсов нужно конкретному объекту или клссу. Сттически предскзть, скольк ресурсв потр. каждму и в совокупности, очень сложно. С одной стороны, эта тем отдельня, с другой, для оценки необх. отслеж. связь с фукнкц. |
- | + | ||
- | Есть некие совсем экзотические темы, например: | ||
- | * Спецификация ответственности. В больших системах всегда достаточно высокая вероятность отказа, а взаимоотношения между потребителями некоторых услуг и провайдерами ресурсом джлжны быть достаточно ясны. Если клиент за что-то заплатил и ему это предоставляется, то всё хорошо, если не предоставляется, то как эту коллизию разрешить. Провайдер, который выступает перед клиентом, теоретически мог бы взять ответственность за всё ПО, за весь компьютерный парк, за сетевые возможности и так далее. Но провайдер не хочет и не может сделать этого, он хочет ответственности только за то, что может отвечать. Тут возникает субподрядчик, который и должен отвечать. И взаимоотношения этих бяз, если бы ни были описаны, и если бы был бы механизм разбора инцидентов, то это была бы неплохая практика страховых компаний. | ||
- | Что можно было бы | + | * Тем безопсности. Свсем неспециф., пскольку сейчас все этй прблмой озбчены. Эт серьёзня вещь и хчется рссм. розные строны опис. системы как нез. спекты, в чстнсти, хтелось бы безоп. тд. от функц, но это удаётся длеко не всегда. |
+ | |||
+ | Есть некие свсем экз. темы, наз. | ||
+ | * Спецификация ответственности. В больших системх всегд дост. высокая вер. тказа, а взаимотн. междлу потр. некоторых услуг и првайдерм ресурсом джлжны быть дост. ясны. Если клиент з чт-то заплтил и ему эт предост., т всё ъхрошо, если не предост, то кк эту коллизию рзреш. Првйдер, который выст. перед гентм, теор. мг бы взять тветственнсть за всё по, хз весь комп. парк, з сетевые возм. и тк длее. Н првйдер не хчет и не мжет сделть этого, олн хочет отв. только з то, что может твечать. Тут возн. субпдрядчик, кторый и длжен твечать. И взаимотн. этих бяз, если бы ни были описаны, и если бы был бы мехнизм разбра инцидентв, то это была бы неплохя прктика страхвых кмпаний. | ||
+ | |||
+ | Что можно было бы скзать по части упрощ. анализ? Указанное выше — тенденция к услож. языкв специф. | ||
* Функциональные языки | * Функциональные языки | ||
- | * | + | * Упрощ. система типов |
- | * | + | * Строгя семнтика |
- | * | + | * Платфрмонез. спец. |
- | Приняли | + | Приняли реш., что языкми спец. польз. не будем, берём хороший язык пргр. и дп. его эл-тми спец.: дбвляем пред, пст усл. и инвринты. |
Spec# | Spec# | ||
- | * | + | * Рсширение C# |
- | * | + | * Кмпилятор |
- | * | + | * Верификтор — Boogie |
- | * | + | * SpecEcxplorer |
- | прект | + | прект бесплтный, но не ткрытый. Для пркт. пргрммиста это не совсем новый язык, а расширение известного. Выявляется дст. ширкий класс ошщибк за счёт исп. рзл. техник. |
- | Пример | + | Пример тог, кк выгдл, предусловие: |
'''class''' ArrayList | '''class''' ArrayList | ||
{ | { | ||
Строка 45: | Строка 47: | ||
} | } | ||
} | } | ||
- | В этом | + | В этом случе, если пдётся неке число, выход. з рамки грницы, выдётся предопр. иск., никк не окрш: requuires violation exception. Пр исключения и пр трактовку предусл. стит сказать тдельно. Рзрб. след. трктвке искл., ктря был ещё их предш. предлжен, и трктовк искл. следующя: исключения трактуются как ткз. Эти откзы бывают двух видов: клиентские и провайдерские. Клиентские — клиент нер. обр. к метду, иил когд релиз. метода сделн не тк, плучился тказ. Провайдесркие тказы в свю очередь делятся ещё н два клсса: admissible — допустимые ткзы, и observed program error. Первый и псл. вид — unchecked исключения, второй, единственный — checked. Любя пргр. длжн ожидть ткие жидемые искл. и опис., чт при этом делть. Если взн. unchecked, т зн., что релиз. некорр. |
- | Пример | + | Пример пис. admissible исключения: |
'''class''' ArrayList | '''class''' ArrayList | ||
{ | { | ||
Строка 60: | Строка 62: | ||
} | } | ||
- | + | Пстусловие: | |
'''ensures''' Count=='''old'''(Count) + 1; | '''ensures''' Count=='''old'''(Count) + 1; | ||
'''ensures''' value==this[index]; | '''ensures''' value==this[index]; | ||
Строка 66: | Строка 68: | ||
'''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 |
(тут история) | (тут история) | ||
Строка 83: | Строка 85: | ||
* 99 - JML | * 99 - JML | ||
* 2003 --- Spec# | * 2003 --- Spec# | ||
- | * Конец 90-х ( | + | * Конец 90-х (примерн 98; первые идеи в рйне 72 года) --- Extended Static Checker (ESC). Идея: когда мы гворили про пред и пст-усл, то считли, чт пракильное пвед. писн там. Есть другой пдхд: прграмма крректн, если в ней нет дурцких ошибок. Этот пдход — релизация этй идеи, и до посл. времени эти нлиз. и вериф., ктрые прверял корр. требваний и ... были дв незв. набор инстр. Сейчас две эти техники боъединены. |
- | Те | + | Те техникивериф, с которыми в втрой ччсти сем. позн., это именн те техники, н к-рых ... бзир. |
{{МФСП}} | {{МФСП}} | ||
{{Lection-stub}} | {{Lection-stub}} |