LINUX.ORG.RU

Как меняется стоимость кода в зависимости от требований к его надёжности?

 


0

3

Что-то не могу ничего найти, хотя помню, что полгода назад где-то обсуждал и находил какую-то инфу на эту тему. Спор начался с того, что кто-то утверждал, что в Open Source на 3 порядка меньше ошибок на 1000 строк, чем в коммерческих программах. Это оказалось враньём и по ходу дела нашлись цифры и о плотности ошибок, и о стоимости программы.

★★★★★
Ответ на: комментарий от olelookoe

Что это за места, если не секрет?

как именно ты будешь оценивать надежность без тестирования,

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

den73 ★★★★★
() автор топика
Последнее исправление: den73 (всего исправлений: 1)
Ответ на: комментарий от anonymous

Что значит, при чём? Они взяли баш с башдором в солярис и продали его своим клиентам. Значит, ответственность несут они. В случае линукса всё сразу написано: «никаких гарантий», поэтому ответственность за башдор в линуксе несёт тот, кто установил линукс.

den73 ★★★★★
() автор топика
Последнее исправление: den73 (всего исправлений: 3)
Ответ на: комментарий от den73

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

anonymous
()
Ответ на: комментарий от den73

Они взяли баш с башдором в солярис и продали его своим клиентам. Значит, ответственность несут они

Нет. Это продавцы, а не эксперты по безопасности. Предъявлять ты можешь только своим сотрудникам, которые за это деньги получают.

anonymous
()
Ответ на: комментарий от Nervous

Если человека закидывать купюрами, то при достижении определённой суммы он начинает писать идеальный код.

anonymous
()

Это зависит не от кода, а от набора тестов. Если писать «надёжный» код без тестов – то любой код на 100% надёжен. Если с тестами – то надёжен, после исправления в рамках покрытия.

Отношение величины покрытия к объёму тестов падает с каждой строкой тестов. И зависимость здесь кривая.

Получаем так:

  1. Цена увеличивается с надёжностью.
  2. Цена поддержи и доработки – аналогично.
  3. Рост цены нелинеен. Может быть квадратичен.
anonymous
()
Ответ на: комментарий от den73

Не понимаешь, что надежная программа с отсутствием ошибок совсем не гарантирует надежную систему.

anonymous
()
Ответ на: комментарий от anonymous

Где я утверждал, что гарантирует? Это твой домысел.

den73 ★★★★★
() автор топика
Последнее исправление: den73 (всего исправлений: 1)
Ответ на: комментарий от den73

К сожалению, это качественное, а надо количественное.

Это и есть количественное, не туда поехавший.

anonymous
()
Ответ на: комментарий от den73

Я не видел мест, где тестировщиков было бы столько же, сколько разработчиков. Обычно их в несколько раз меньше. Так что скорее важен тот факт, что они «вываливают»

Минимально сложный GUI тестируется только руками — я довольно много работал в компании с толпой тестировщиков. Сейчас потребность в тестировании не снизилась — снизилась лишь планка качества.

byko3y ★★★★
()
Ответ на: комментарий от anonymous

а сколько бы стоила нормальная операционка, которая не решето?

Solaris - 8 млн. человеко-лет

Откуда такие цифры оценки? Даже если подумать, что сотня человек каким-то магическим образом писала это ось 20 лет — получается всего-лишь 2000 человеколет. Ты пробовал когда-нибудь хотя бы десяток человек впрячь в разработку одного тесносвязанного проекта?

Ну и я бы на твоем месте уточнил, что есть «норм операционка», потому что на самом деле ОС может быть сильно проще, чем bloatware с драйверами в дереве сорцов и совместимостью с бесчисленными устаревшими стандартами.

byko3y ★★★★
()
Ответ на: комментарий от den73

Они взяли баш с башдором в солярис и продали его своим клиентам. Значит, ответственность несут они

Индустрия уже давно привыкла к тому, что ОС пишется на Си, а значит бэкдоры и удаленное выполнение там будет всегда, это неизбежно для любой сишной программы сложнее «Hello World». И ответственность за это никто не будет нести, потому что так делают ВСЕ.

byko3y ★★★★
()
Ответ на: комментарий от anonymous

Если человека закидывать купюрами, то при достижении определённой суммы он начинает писать идеальный код

Хах! Если речь идет про единственного человека, то было даже исследование, которое показывало, что чем меньше платят человеку. тем лучше он работает. В идеале человек должен забесплатно писать опенсорс, хе-хе.

byko3y ★★★★
()

извини, весь тред не читал, просто тема заинтересовала.

  1. писать без ошибок неьзя.
  2. надежность неизмерима.
  3. мы имеем дело не с программой, а с апаратно-программными комплексами

от сюда можно сделать выводы:

  • нет такого понятия «надежная программа», есть вылезанная. существуют программы, которые рабтают десятками лет у тысяч операторов. на них люди полагаются. тем не менее их код может быть ужасен, и работать она может только в определенных условиях. это не отменяет того, что ей можно доверять.
  • только время использования может дать ответ о том, можно ли доверять программе.
  • программа не отделима от окруженя. сменишь окружение (железо, ос...) и вся предыдущая оценка более ничего не значит. она применема только к тем условиям, в которых уже эксплуатировали по.
  • ошибка с прогаммной и доме́нных позиций принципиально разные, таким образом без доме́нной области оценить «надежность» также не получится.
zerhud
()

поищи у стива макколена «совершенный код», там несколько исслеований (ссылки на них в материалах книги).

zerhud
()

Ясно только одно, цена будет выше.

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

Конкретных цифр или законов ты не выведешь. Это невозможно.

umren ★★★★★
()
Последнее исправление: umren (всего исправлений: 1)
Ответ на: комментарий от anonymous

Это зависит не от кода, а от набора тестов. Если писать «надёжный» код без тестов – то любой код на 100% надёжен. Если с тестами – то надёжен, после исправления в рамках покрытия

Ты находишься в глубоком заблуждении по поводу того, что любое «прокрытие» не представляет собой на самом деле 0% покрытия сценариев выполнения в пределах погрешности. А именно это и есть суровая реальность. Опять-таки, если речь идет не про «Hello World» — поскольку кол-во сценариев выполнения растет примерно экспоненциально со сложностью, потому «Hello World» можно покрыть процентов на 100%, прогу на тысячу строк по обработке пары массивов покрыть на 20% — это уже достижение, а иметь 5% покрытия на миллионнике — это почти нереально. К частью, модель машины Тьюринга приводит к тому, что те 0.007%, который ты покрыл своими тестами, пересекаются по своей сути со многими подобными немного отличающимися сценариями. Но9 нет никакого способа гарантировано сказать «ага, эти два сценария похожи, потому нам достаточно покрыть только один» — потому тебе нужно покрывать оба, два сценария тут, два здесь, и вот с ростом проекта тебе уже нужно покрывать 2^83 сценариев, а тестов у тебя сколько? Тысяча? Две тысячи?

byko3y ★★★★
()
Ответ на: комментарий от byko3y

Индустрия уже давно привыкла к тому, что ОС пишется на Си, а значит бэкдоры и удаленное выполнение там будет всегда

прекрати квасить.

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

alysnix ★★★
()
Ответ на: комментарий от zerhud

А что значит «с доменных позиций» - то, что ты описал про условия применения? Касаемо программно-аппаратного комплекса - можно его понимать под «программой», суть не меняется.

den73 ★★★★★
() автор топика
Последнее исправление: den73 (всего исправлений: 1)
Ответ на: комментарий от zerhud

Спасибо, в принципе уже поздно. Когда-то эту книжку смотрел, кажется, была даже на бумаге, может даже ещё и осталась. Попадётся - посмотрю.

den73 ★★★★★
() автор топика
Последнее исправление: den73 (всего исправлений: 1)
Ответ на: комментарий от den73

можно его понимать под «программой»

Нельзя вобще то. Программа не гниет, у неё не барахлят контакты и она не промокнет. Что будет с программой, которая хорошо работала 20 лет, а потом сломалось устройство, которым она управляла (не критичная поломка, но все же) . Будет она надежной? Получается что такое не было протестированно.

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

zerhud
()
Ответ на: комментарий от zerhud

надежность неизмерима

Очень даже измерима. «В рамках теории надёжности вводят количественные показатели надёжности технических систем.» Матчасть начинаем учить девочки, чтобы не выглядеть полными дурами.

anonymous
()
Ответ на: комментарий от den73

А что с чем сравнивать то? Качество кода у разных проектов разное. Есть и коммерческий говнокод и опенсорсный. От людей зависит всё.

peregrine ★★★★★
()
Последнее исправление: peregrine (всего исправлений: 1)
Ответ на: комментарий от zerhud

понятно примерно. Это тогда можно тоже включить в рассмотрение.

den73 ★★★★★
() автор топика
Последнее исправление: den73 (всего исправлений: 1)
Ответ на: комментарий от zerhud

Программа не гниет, у неё не барахлят контакты и она не промокнет

и надёжно подвергается старым уязвимостям, если её не патчить. Аналогия с ржавением в агрессивной среде вот прям на поверхности.

t184256 ★★★★★
()
Ответ на: комментарий от t184256

А здесь вилы: если не патчить, то подвержена старым. Если патчить, то подвержена новым.

den73 ★★★★★
() автор топика
Ответ на: комментарий от den73

не секрет?

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

olelookoe ★★★
()
Ответ на: комментарий от t184256

надёжно подвергается старым уязвимостям, если её не патчить

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

Аналогия с ржавением в агрессивной среде

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

zerhud
()
Ответ на: комментарий от zerhud

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

Привет вам там в параллельной реальности. В нашей даже самые консервативные сидят на каком-нибудь RHEL-6 или 7.2 и при этом требуют бэкпортировать им все самое-самое.

в чем же эта аналогия? ржавчина со временем меняет систему: сначала ее нет, потом появилась небольшая ржавчина, потом больше и в конце концов механизм придет в негодность

Ну. Код тот же самый, а заставить его делать что-то не то способов все больше и больше. Там срыв буфера без возможности удаленного эксплуатирования, там DoS, но непрактичный, и тут бац, критическая уязвимость, все тот же самый код теперь может поиметь любой желающий. Даже самым толерантным к замшелому приходится апдейтиться.

t184256 ★★★★★
()
Ответ на: комментарий от t184256

еще раз. изменения в окружении обнуляют то, что было известно о работе программы. есть какой-нибудь контроллер, он управляет механизмом, интернет не подключен. с программой внутри ничего никогда не случится. она работала и будет работать пока оборудование будет позволять. (как тут выше указали, n / t == 0 так как n == 0, а потому смысла в таком измерении нет).

если мы имеет дело сетью, то тут все меняется очень быстро. приложение перестает работать так как среда изменилась, а не приложение. (n / t снова мимо, так как t==1 год, например, не одно и тоже 5 лет назад и сейчас.) возьмем к примеру http. 25 лет назад поднял сервак, который знать не знает о сертефекатах, и нормально тогда было. сейчас нужен https так как браузеры отказываются работать с http. окружение поменялось, предыдущая оценка более не действительна - приложение не может исполнять свою роль.

Даже самым толерантным к замшелому

не важно как человек относится к замшелому, важно с какой средой он имеет дело. рабочий за станком, возможно, даже не подозревает. что там по обновлять можно.

zerhud
()
Ответ на: комментарий от t184256

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

den73 ★★★★★
() автор топика
Ответ на: комментарий от den73

Да вы примерно одно и то же говорите

Именно, но он с чем-то спорит, а я недоумеваю.

просто ты проскочил от обсуждения описания видов ржавчины сразу к методам её устранения. К тому же твой собеседник вежлив, а ты зачем-то грубишь.

Ни слова не сказал ни грубого, ни про методы устранения ржавчины окромя замены.

t184256 ★★★★★
()

Выступление состоялось, вот кадр, про который была тема:

https://youtu.be/htIFeXv4L4U?t=1237

Хоббит - ты можешь посмотреть первую часть, примерно 20 минут. Там я пытаюсь объяснить, почему твой вариант не работает.

den73 ★★★★★
() автор топика
Ответ на: комментарий от t184256

Мне кажется, что «параллельная реальность» - это такой тонкий намёк на то, что собеседник неадекватен, но если ты имел в виду что-то другое, то извини.

den73 ★★★★★
() автор топика
Ответ на: комментарий от svv20624

код обновляется КАЖДЫЙ ДЕНЬ, меняются используемые библиотеки, меняется железо и компиляторы…

Особенно в марсоходе или контроллере двигателя самолёта.

hateyoufeel ★★★★★
()
Ответ на: комментарий от den73

Как меняется стоимость кода в зависимости от требований к его надёжности?

нелинейно, в зависимости от возможностей автоматизации формальной верификации и автоматизации проверки соответствия требований

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

на сайте adacore полно прохладных историй про SPARK и формальную верификацию, поищи там.

на сайте ada-ru.org есть переводы и презентации (или там в новостях, статьях, на форуме – или на mediascan.by).

ищи что-то вроде Controlling-Costs-with-Software-Language-Choice-AdaCore-VDC-WP.pdf со схемами, графиками, цифрами и моделями расчёта затрат вроде TCO.

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

например, на adacore был где-то пример про «формально верифицируемый тетрис». который был написан на SPARK как контрактное программирование, с доказательным программированием – про кванторы, на которых и формулировался «формально верифицируемый тетрис», с инвариантами, предусловиями, постусловиям.

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

возможно, для такого вот профиля и реально доказать надёжность и те же гарантии по ограничению по времени на реализацию сисколлов, и прочих вызовов.

anonymous
()
Ответ на: комментарий от anonymous

вообще ада любопытный пример того, как развивается такая вот система:

  • сначала берём язык «ограниченный паскаль», в духе Ada83: объектный, но не объектно-ориентированный. вообще, если говорить например про «ООП как концепцию», то можно говорить на нескольких уровнях: концепутально объекты это некие повторно используемые компоненты, модули. например, в книгах «объектно-ориентированное конструирование», «почувствуй класс с эйфель» показано как исходя из некоторого псевдокода и «теории ООП», некоторых принципов последовательно выводятся из инвариантов теории свойства и способ конструирования. например: системная динамическая корректность, системная статическая корректность (на уровне системы типов), контракты (времени выполнения или компиляции), как ограничения и далее механизмы реализации такого вот ООП (например, ковариантность которая в эйфеле может быть задана явно, на уровне языка). это если взять эйфель.

если взять CLOS с AMOP и мультиметодами (типа фреймов), или смоллток с метаклассами (типа акторов) – то это высокоуровневые «концептуальные объекты».

если взять, прости господи, С++ – это средний весьма уровень ООП (логический) (из-за FBC problem и например virtual методов, где этот спецификатор должен быть задан явно – в отличие от других объектных систем, где его можно было бы вывести, специализируя родовые обобщённые методы или контракты, «объектный сервер», «объектный клиент» (метаобъектного протокола)).

или например, Active Oberon с модулями и AWAIT активными объектами.

если взять какой-нибудь VB6, 1C, HLA и т.п. – то это пример объектного но не объектно-ориентированного программирования. то есть: поскольку не first class object а например сгенерирован в design time движок/среда с предопределёнными не расширяемыми объектами.

это будет «низкий уровень ООП», физический.

  • далее про Аду и например оберон: Blackbox/Component Pascal, A2/Active Oberon.

ада – язык системный. в котором есть task/entry, контролируемая память, тегированые указатели (access), иерархические модули (package), полиморфизм дженериков, параметризация модулей, исключения.

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

в этом смысле обероны – прикладные ООП языки (более системный Oberon07, более прикладной активный оберон с активными объектами).

можно сказать, что модуль kernel среды и system языка – где реализованы сборка мусора и загрузка модулей – и реализуют такую среду на активных объектах.

anonymous
()
Ответ на: комментарий от anonymous
  • далее про тулинг.

например, в оберонах пытаются переписать всё на самом себе, словно метапрог эдакий. например, в A2 есть ассемблер, дизассемблер, линкер (не говоря уже о компиляторе Fox и редакторе PET). потому что не нужен сложный линкер/лоадер если не держаться за ELF/PE. а нужен более с метаданными расширяемый формат модулей (.sym файлы и т.п., разные .obw, .obx, .obj, .abw и т.п.)

сравнивая тулинг блекбокса – в A2 менее герметично, и более запускаемо отдельно, но всё ещё «вещь в себе».

сравнивая тулинг ады – есть пакетный менеджер alire и среда сборки gprbuild, которые запускают стандартный gcc driver и его кодогенератор и линкер из binutils, linker scripts с нестандартным фронтендом gnat.

например, gcc -fdump-spec-ada file.c -o file.ads из gnat умеет генерировать бингинги к сишке автоматически. к С++ – чуть сложнее из-за нестандартизированного ABI C++ и манглинга (например, нужно понимать виртуальный или нет метод, чтобы линковать правильно) – но тоже не очень сложно, см. примеры в статьях.

статьи (gems) есть переведённые на русском – на ada-org.ru (или на mediascan.by) и на adacore оригинальные. там например, про привязку к питону, C++, POSIX и GNATCOL.

  • вообще ада пример того как можно прокачать твою тачку – паскалеподобный человекочитаемый язык с простым синтаксисом.

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

– берём настраиваемые рантаймы (физический уровень)

– берём профили рантаймов, на которых можно гарантировать какие-то характеристики про поддержку высокоуровневых фич языка (или их отсутствие) – (логический уровень) ) – берём сам достаточно системный язык (высокий, логический уровень)

– поверх строим на SPARK контракты и формальную верификацию (концептуальный уровень)

=>> в результате получаем способ вообще что-то верифицировать, контролировать и гарантировать через формальную верификацию

anonymous
()
Ответ на: комментарий от den73

про MIPS уже всё – см. новости на том же например 3dnews.ru

если коротко, несмотря на открытие архитектуры и активность того же Ю. Панчула по популяризации, там череда банкротств компаний-владельцев IP технологии MIPS.

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

anonymous
()
Ответ на: комментарий от den73
  • prezent20110927.pdf стр.9 – приведены «Стандарты безопасности ПО», «Уровни оценки безопасности (EALs)», «Международные стандарты на критичное к безопасности ПО», «Уровни критичности ПО согласно DO-178B», «Уровни безопасности-сложности-целостности SCIL (Safety-Complexity-Integrity Levels)», «Уровни целостности предложенные MISRA»

  • http://www.ada-ru.org/slides 01-intro-ru.pdf – тоже это приведено

  • Ada-AdaCore.pdf стр. 26: «Чего стоят такие меры обеспечения надежности»

стр.27:

IEEE Software, 1987, #1, pp40-44:
• производительность разработчиков на полном
цикле (>= 20_000 SLOC):
– Ада - 12 строк/день
– другие языки - 10 строк/день
• распределение затрат в проекте
             +проектирование+реализация+отладка+
Ада          ! 64.4         ! 27.1     ! 8.3
другие языки ! 28-40        ! 17-58    ! 24-50  

стр. 27, график

Ада; C; другие языки, ориентированные на человека

объёмы проектов в SLOC, по оси X -- feature point, functional points
по оси Y -- стоимость разработки, в килобаксах

стр. 28 «Исследования компании Ziegler: Сравнение языков C и Ада»

исследования 1995 на примере компилятора VADS : 4.5M SLOC, 22000 файлов, стоимость >28M USD на протяжении 10 лет

примерно одинаковый объём кода на Си и на Аде, ещё какой-то DSL

следующая стр. 29 «Стоимость реализации на свойство»

график: 1) C, 300k 2)C, включая Makefiles (чуть больше 300k) 3)Ada, ~180k

следующая стр. 30 «Дефекты, обнаруженные (пользователями) после поставки продукта»

гистограмма C/Ada по видам дефектов (критические, серьёзные, средние, всего)

видно, что всего С ~1000, всего Ада примерно 150. по видам на аде примерно одинаковых по 50, по С – критических ~200, серьёзных ~570, средних ~230.

стр.33/37 «Резюме»

Разработка ПО на Аде обошлась на 60% дешевле чем на C
Код написанный на Аде содержал в 9 раз меньше ошибок чем
аналогичный на C
Была ли в целом Ада лучше? *ДА*
• На протяжении разработки и сопровождения разных подмножеств VADS
• Для опытных программистов И для новичков
• Как для экспертов C ТАК И для экспертов Ады
• Как для наиболее ТАК И для наименее квалифицированных программистов,
принимавших участие в проекте
Сложно ли было изучать Аду? *Нет*
Был ли написанный на Аде код более надежен? *ДА*
http://www.adaic.com/whyada/ada-vs-c/cada_art.html

http://edb.jacob-sparre.dk/Posix_in_Ada/ Subject: Understanding Unix/Linux Programming

книга Safe_and_Secure.pdf Джон Барнс «Безопасное и надежное программное обеспечение Ada 2012 (адаптировано для SPARK 2014)» есть на русском.

скачал где-то в районе ada-ru.org – в статьях, слайдах или по ссылкам на форуме (там где Announce_ AdaStudio-2021 release 14_12_2021 free edition_1 Qt6Ada и т.п. – на гуглдрайве у него есть переведённые книжки на русском).

  • RU_Ada_for_the_Embedded_C_Developer.pdf

  • AdaCore_FACE.pdf

– тоже где-то там лежит

anonymous
()
Ответ на: комментарий от anonymous

например, на adacore был где-то пример про «формально верифицируемый тетрис»

что-то вроде такого: SPARK-to-C_Tetris_Demo, только это с рантаймом для ардуины, а я вроде бы простой обычный как приложение видел (а потом его допилили до Barebones. или его теперь объединили в один репозиторий, старое в SPARK_Tetris_Native. или в той другой реализации там всё было на Аде, без кодогенерации SPARK в сишку)

вот, полюбуйся на контракты и инварианты на SPARK во всей красе: например, tetris_functional.ads:L189

ещё имеются пятнашки на SPARK

anonymous
()
Ответ на: комментарий от anonymous

или tetris_functional.ads:L156

тут даже нагляднее – for all с кванторами, and then/or else = short circuit версии, ну и ниже про Pre, Post, Global – контракты с предусловиями, постусловиями, инвариантами во все поля

anonymous
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.