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

[kouzdra]

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

Comments

[anonymous]

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

Но зачем?

[kouzdra]

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

[vladicusmagnus]

Ну о чём и спич. Препроцессорные директивы воткнули в код. И? Крута, чо... В общем очередная свистоперделка, не без интересных идей, но это можно было теорией выдать, а не писать очередное мертворожденное.

[kouzdra]

Причем тут "препроцессор" вообще - если компилятор не сможет доказать что инвариант цикла (в данном случае - неизменность фрагмета массива) гарантировано выполняется - программа не откомпилируется.

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

Аналогом этого кода в С было бы что-то вроде:

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

[anonymous]

У вас есть препроцессор, который умеет проверять инварианты? Название в студию.

[anonymous]

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