June 20th, 2017

Gen.Turgidson

Что до павшего под корейским игом американского героя

Не хотел ничего писать, но попершее морализаторство несколько утомило:

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

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

PS: И к режиму какие претензии? Сам же парень полез на провода с высоким напряжением. Ну убило - бывает.

Штаты в этом смысле точно такие же - только там опасные места под напряжением другие - например нервные полицейские стреляющие почем зря - с которыми тоже надо технику безопасности (неочевидную кстати за пределами США соблюдать).
Gen.Turgidson

На тему "сделать мир безопасным":

Один из лучших текстов на эту тему:

В Москве любят запирать двери



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

Кто тот человек, который разрешит загадку кинематографов, театров и цирков?

Три тысячи человек должны за десять минут войти в цирк через одни-единственные, открытые только в одной своей половине двери. Остальные десять дверей, специально приспособленных для пропуска больших толп народа, -- закрыты. Кто знает, почему они закрыты? Возможно, что лет двадцать назад из цирковой конюшни украли ученого ослика, и с тех пор дирекция в страхе замуровывает удобные входы и выходы. А может быть, когда-то сквозняком прохватило знаменитого короля воздуха, и закрытые двери есть только отголосок учиненного королем скандала.
Collapse )
Там, где нельзя поставить барьера или рогатки, перевернуть скамейки или вывесить заградительную надпись,--там протягиваются веревки. Протягиваются они по вдохновению, в самых неожиданных местах. Если они протянуты на высоте человеческой груди, дело ограничивается легким испугом и несколько нервным смехом. Протянутая же на высоте лодыжки веревка может искалечить человека.

К черту двери! К черту очереди у театральных подъездов! Разрешите войти без доклада! Умоляем снять рогатку, поставленную нерадивым управдомом у своей развороченной панели! Вон перевернутые скамейки! Поставьте их на место! В сквере приятно сидеть именно ночью. Воздух чист, и в голову лезут умные мысли!
Dr.Strangelove

По поводу frama-c

# include <stdio.h>

/*@ requires n >= 0;
  @ ensures \result >= 1; 
 */
int fact (int n) {
  if (n == 0)
    return 1;
  return n * fact (n-1);
}

int main (int argv, char * argc []) {
  printf ("Hello: %d\n", fact (50));
  return 0;
}


Кажется подавляющее большинство народу вообще не понимает в чем на самом деле состоит тут неправильность:

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

И дальше при вызовах функции он будет полагаться на это.

По уму оно должно быть так:
Collapse )
Dr.Strangelove

По поводу верификационных тулов

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

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

Во-вторых - верификатор строго говоря не доказывает правильность программы - он доказывает соответствие кода некоторым формальным утверждениям о его свойствах.

Во-третьих - в остальном есть два опять же варианта:

1) максималистский - прописывается формально вся существенная семантика, и в случае если верификатор не справляется (а это в случае сложных условий довольно обычная ситуация), ему объясняют "что и как" вручную*

2) минималистский - всякие фичи типа приведеных выше используются по принципу "что удалось формализовать и проконтролировать - то и формализуем и контролируем". По мне тут удается формализовать довольно много и я бы очень бы непротив иметь подобную функциональность и в обычных приложениях. В частности потому что она неплохо подстраховывает от привнесения ошибок при модификации кода.

*) По поводу того что "все доказать невозможно - ибо Гедель и Тьюринг" - тут дело такое - автоматически - да - невозможно. Но вот проверить доказательство - не просто возможно - но и очень просто - и эти системы как правило и позволяют если автоматически не удалось доказать - просто выписать ключевые моменты доказательства вручную (что заметно более трудоемко - но и только) - после чего система без особых затруднений проверяет/доказывает его.

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