По поводу:
https://kouzdra.livejournal.com/4404809.html
https://kouzdra.livejournal.com/4410328.html

были демоны была бага - вчера вечером засабмитил - пофиксили (говорят - я пока не проверял).

Upd: проверил и правда пофиксили

Пара слов по тому примеруПосле того как стало понятно, что основа совинной методы - агрессивное разворачивание кода, в общем-то стало понятно и "как оно это доказывает":
( Read more... )

В общем - разобрался я "что это было и как это называется" (© Леонид Соболев). На деле оказалось не просто "тупо и просто", а "очень тупо и просто" - и довольно коряво, но для своего реального назначения вероятно самое то ( Read more... )

Разобрался с примерчиком про деление. Вкратце - как и ожидалось, просто ошибка в генерации промежуточного кода из-за которой не сходятся типы:
( Read more... )

Одна из причин моего к нему интереса - именно что "вроде бы на этом можно писать" (потому что на 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... )

Как я уже говорил, я поигрался со своими тестиками:

Для начала простейший: как известно знаковое деление на 2 нельзя "оптимизировать" арифметическим сдвигом: на отрицательных числах они округляют в разные стороны потому результат на нечетных отрицательных числах отличается на 1:

typedef int32_t my_int;

my_int ref (my_int n) {
return n/2 ( Read more... )