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

Так-то там ничего особенно принципиально нового нет.

(причина дафнячества простая - мне с этим и около надо разобраться более или менее подробно - потому разбираюсь - ну и что-то пощу - отчасти "для памяти", отчасти "для публики" и в видах народного просвещения).Из того же примера: захотелось посмотреть как решаются проблемы с алиасингом - ну соответственно инкремент массива выделился в функцию "о ( Read more... )

Раз уж пошло такое - иллюстрация к этому: 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
( Read more... )

Кажется не все въезжают, "о чем это":

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

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