[Kabdim 0]

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

[AlexandrY 3]

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

Там просто сделана проверка на соотвествтвие спецификации. Саму спецификацию ребята не показали.

Т.е. проверка на соответсвтвие коня в вакууме реализации на С да еще на ядре с виртуализацией памяти, с запрещенными прерываниями (только поллинг) и еще кучей чертовщины.

В топку.

[Kabdim 0]

Саму спецификацию ребята не показали.

Вы не смогли зайти на гитхаб?

[syoma 1]

Можно было бы попытаться дать гарантию безошибочности (100 %, или хотябы 9.999 ), если бы весь "продукт" был свой, доморощенный.

до последнего бита и проводка.

1. Читаем errata на ВСЕ что используется из комплекующих, и пытаемся ЭТО предусмотреть в коде.

2. Читаем errata, и "мечтаем", что там моежт появиться в следующей ревизии (но глючек уже в этой).

3. Неоткрытая элементарная частица из Вселенной влетает в ГЛАВНЫЙ РЕГИСТР системы и все рушится.

(одна надежда, что по вероятности ОНО не затронет WD).

Ну вообще-то известно, что каждая 9-ка такой гарантии увеличивает стоимость разработки на 100%. Т.е достичь гарантии в 99.9% по сравнению с 99% будет стоить, как новая разработка и так далее. Но мне это и не нужно - в моем проекте в этом случае дешевле угробить оборудование и возместить убытки, чем пытаться защититься от таких сбоев.

 

 

[AlexandrY 3]

Вы не смогли зайти на гитхаб?

Имеете какое-то отношение к этому проекту или просто купились на фразу - "все формально проверено"?

Только взглянул на спецификацию и чуть крыша не съехала.

Вы напрмер можете человеческим языком объяснить что такое higher-order logic?

Чем эти сектанты там вообще занимаются?

[Kabdim 0]

Если осилите HoL, то скорее всего вам не потребуются объяснения. Эти "сектанты" называются прикладными математиками.

[AlexandrY 3]

Если осилите HoL, то скорее всего вам не потребуются объяснения.

Даже не собираюсь.

Изъян этого подхода очевиден. Ребята выдвигают принципиально неосуществимое условие - полностью формализовать спецификацию.

 

А реальному программису надо хотя бы узнать как в действительности работает API.

Само изучение API превращается в исследование. Так же с аппаратными ресурсами.

"Прикладные математики" здесь отдыхают.

 

[Kabdim 0]

Я даже готов с вами отчасти согласится о ненужности этого для простого кодера и/или для изделий без ответственности. Ну а кто-то другой возможно возьмет из этой дискуссии больше.

[mantech 34]

Можно было бы попытаться дать гарантию безошибочности (100 %, или хотябы 9.999 ), если бы весь "продукт" был свой, доморощенный.

до последнего бита и проводка.

 

Даже в этом случае такой гарантии не дадите, если только не мигание светодиодом через программную задержку.

 

Люди даже в "hellо world" умудряются ошибки вывода в терминал делать...

[Студент заборстроительного 0]

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

Потому что "Задача покрытия" относится к задачам NP-класса. Поэтому в общем виде не решается за обозримое время

[AlexandrY 3]

Потому что "Задача покрытия" относится к задачам NP-класса. Поэтому в общем виде не решается за обозримое время

Не, не то.

Они тестировали спецификацию, а не программу.

Представляете!? Есть чудаки которые сначала пишут спецификацию, тестируют ее каким-то образом с хаскелем, и только потом делают из нее программу.

Но ту программу уже не тестируют.

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

До реальной программы еще как до луны, но куча работы уже проделана, можете идти требовать надбавку.

[Kabdim 0]

Ну хватит уже фантазировать о том что не осилили. Это уже какое-то болезненное себялюбие - высасывание контраргументов из фантазий.

Потому что "Задача покрытия" относится к задачам NP-класса. Поэтому в общем виде не решается за обозримое время

Ну и вы я так понимаю статьи не читали, но мнение имеете? :)

[AlexandrY 3]

Ну хватит уже фантазировать о том что не осилили. Это уже какое-то болезненное себялюбие - высасывание контраргументов из фантазий.

Ну и вы я так понимаю статьи не читали, но мнение имеете? :)

Вы сами-то докажите что что-то поняли?

От вас только ссылки. Такие мы и сами вам можем тонну отгрузить. :laughing:

[Kabdim 0]

Если бы вы прочитали первую ссылку, вас бы не пришлось отправлять в раздел 4.3. Но с учетом того что вы не осилил даже это, я в обсуждении с вами в серьезном ключе смысла не вижу. Вы ведь всё равно будете фантазировать любую фигню лишь бы сделать вид что это не вы "не ослили", а "авторы дураки".

[AlexandrY 3]

Если бы вы прочитали первую ссылку, вас бы не пришлось отправлять в раздел 4.3. Но с учетом того что вы не осилил даже это, я в обсуждении с вами в серьезном ключе смысла не вижу. Вы ведь всё равно будете фантазировать любую фигню лишь бы сделать вид что это не вы "не ослили", а "авторы дураки".

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

Скажем можете ли вы объяснить зачем нам вот такое доказательство - confidentiality and intransitive non-interference proofs?

Т.е. как его применить программисту embedded шлюза между Ethernet и SPI ?