December 1st, 2019

Gen.Turgidson

Ура! Зима официально началась!

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

Наши военныы мозги прошу прощения

Разразились на warhead.ru заметкой о американских околовоенных фантазиях на темы "звездных крейсеров бороздящих просторы театра метрополитен":
https://warhead.su/2019/11/30/bolshie-korabli-i-velikie-ambitsii-kakim-mog-byt-kosmicheskiy-flot-ssha

Сами прожекты любопытны, но еще любопытнее восприятие космических проблем аффтарами - как некоторая коллекция предрассудков о космосе: из комментов к:
https://youroker.livejournal.com/105868.html?thread=1910924#t1910924
Главным достоинством проекта называлась неуязвимость для превентивного удара. «Орион-бомбардировщик» на высокой орбите нельзя было внезапно атаковать ракетами с Земли, околоземной орбиты или даже Луны. Советским противокосмическим ракетам потребовались бы дни, чтобы до него добраться. За это время «Орион» успел бы нанести удар.

Ну нельзя же такую хрень писать. FYI - New Horizons пересек лунную орбиту через 15 часов после запуска. При том что задачи "сделать это побыстрее" ему не ставилось.

необычный проект позволял при необходимости «форсировать» каждый реактор с 75 МВт тепловой мощности до ошеломляющих 2500 МВт!

чего там "ошеломляюшего"-то - тепловая мощность ТЯРД по проекту NERVA - 5 гигаватт. Прототип двигателя был успешно вполне испытан в конце 60- на стенде (правда на 5GWt не вышли - ограничились 4-мя с копейками). Так что тут еще скромно весьма. Наверняка ориентировались не на "максимально достижиму мощность" (она по факту выше минимум в два раза), а на достаточную

На «форсаже», система охлаждения работала в открытом цикле (просто сбрасывая кипящий хладагент за борт).

Ой - вы хоть знаете как работает ТЯРД? - там собственно "охлаждение" обеспечивается как раз потоком разогреваемого рабочего тела (в кавычках - потому что нагрев рабочего тела и является основной функцией реактора в ТЯРД), Можно конечно называть рабочее тело "хладагентом" - но как бе оно там совсем не для этого греется.

Другое дело что идея "реактора-универсала" странна - теже двигатели от NERVA не так уж велики, чтобы пытаться скрестить ежа с ужом. Впрочем судя по упоминанию в качестве источника энергии для пушек реактора SP-100 - на деле никто и не планировал.
prog

На тему привидений

Тут еще ознакомился с плодом сумрачного мелкого и мягкого гения - язычком Dafny от них (собственно "москали в микрософте" именно оттуда). Язычок представляет собой что-то типа WhyML допиленного до того на чем вроде бы можно программировать (WhyML для этого и не предназначался - это утиля для опытов с доказательством правильности всяких алгоритмов).

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

По этой причине возможно буду постить кое-какие любопытные конь-цепть-уальные примерчики (бо наконец появился их источник в достаточно вменяемой форме не треюущей двухстраничного комментария на тему "что это было и как это называется"):
ghost var prevElements := a[..];
while // ...
  invariant a[lo..hi] == prevElements[lo..hi];
{
  // ...
}
Коньцепт тут "переменная-призрак". Смысл в том что они семантически ведут себя также как и "нормальные", только
1) на них нельзя ссылаться кроме как в "непризрачном" коде и в разного рода предикатах (в частности в инвариантах)
2) они не порождают никакого кода.

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

В данном случае - инвариант цикла утвержает что подмассив a[lo..hi] на протяжении всех итерации остается неизменным.
Gen.Turgidson

Мне тут напомнили что сегодня 140 лет был открыт сезон зимней охоты:

Хотел было отписаться сам, но это уже сделали лучше меня - так что:
https://maysuryan.livejournal.com/960428.html
в комментах корежит хрустобулочников



1 декабря (19 ноября) 1879 года. Взрыв свитского поезда


140 лет тому назад, 1 декабря (19 ноября) 1879 года под Москвой произошёл первый взрыв одного из царских поездов в их неуклонном следовании на станцию Дно (которое совершилось в Феврале 1917 года). Народовольцами был взорван поезд царской свиты. Несмотря на мощный взрыв, никто не погиб. Поезд свиты был взорван по ошибке, из-за перемены порядка следования основного императорского и свитского поездов.

Официальная печать о покушении:
Collapse )
Gen.Turgidson

На тему космического лифта:

https://kiri2ll.livejournal.com/1361679.html
Cобранная во время наблюдений бури информация позволила выявить неизвестные ранее особенности погодных процессов красной планеты. Оказалось, что во время подобных событий в атмосфере Марса формируются своеобразные «башни» — пылевые столбы, подымающиеся на десятки километров над поверхностью планеты.

Наблюдения показали, что марсианские пылевые «башни» могут достигать высоты 80 км, что намного выше атмосферного слоя, в котором обычно рассеяна пыль. На этой отметке их диаметр может достигать 500 км. Во время разрушения, башни формируют мощные пылевые облака на высоте 56 км, самые обширные из которых могли бы накрыть всю континентальную часть США.

По словам ученых, обычный срок жизни пылевых структур в марсианской атмосфере не превышает пары дней. Но во время глобальных бурь все меняется. Нижние слои «башен» получают постоянную «подпитку», что позволяет им существовать по 25 дней.

Обнаружение «башен» важно не только для понимания особенностей марсианских глобальных пылевых бурь. Оно также может объяснить причину потери Марсом значительной части воды. По мнению исследователей, пылевые структуры могут играть роль своеобразного космического лифта. Когда пыль нагревается, восходящие потоки уносят молекулы водяного пара в верхние слои атмосферы. Там под действием ультрафиолета они распадаются на водород и кислород, после чего безвозвратно улетучиваются в космос.
prog

По поводу призраков:

Кажется не все въезжают, "о чем это":
ghost var prevElements := a[..];
while // ...
  invariant a[lo..hi] == prevElements[lo..hi];
{
  // ...
}
ghost var нужны имено для задания инвариантов без порождения лишнего кода. С точки зрения компилятора они ведут так же как обычные и на общих правах участвую в процессе верификации "как если бы были настоящими" - но в код это не попадает.

Аналогом этого кода в С было бы что-то вроде:
  std::vector<int> a = ...
  ...
  auto const inv = std::vector<int> (a [lo], a [hi]);
  for (int i = 0; i != a.size(); ++ i) {
    assert (inv == std::vector<int> (a [lo], a [hi]));
    ...
  }
Только без оверхеда и с контролем условия во время компиляции
prog

Собственно пример на инварианты в dafny:

Раз уж пошло такое - иллюстрация к этому: https://kouzdra.livejournal.com/4407243.html
Вот такой код компилируется и работает:
var lo, hi := 2, 4;
var a := new int[6];
forall i | 0 <= i < a.Length {
  a [i] := (i + 1) * 10;
}
ghost var prevElements := a[..];
var i := 0;
while i < a.Length
  invariant a[lo..hi] == prevElements[lo..hi];
{
  if i < lo || i >= hi {
    a [i] := a [i] + 1;
  }
  i := i + 1;
}
А если заменитьCollapse )