Новый для Spark и новый для Ada, поэтому этот вопрос может быть слишком широким.Тем не менее, это спрашивается добросовестно, как часть попытки понять Spark.Помимо прямых ответов на вопросы ниже, я приветствую критику стиля, рабочего процесса и т. Д.
В качестве моего первого набега на Spark я решил попытаться реализовать (легко) и доказать правильность (пока что безуспешно) функции
.
Вопрос: Как правильно реализовать и доказать правильность этой функции?
Я начал со следующего util.ads:
package Util is
function Floor_Log2(X : Positive) return Natural with
Post => 2**Floor_Log2'Result <= X and then X < 2**(Floor_Log2'Result + 1);
end Util;
У меня нет предварительных условий, потому что диапазоны ввода полностью выражают единственное интересное предварительное условие.Постусловие, которое я написал на основе математического определения;однако, у меня есть непосредственная проблема здесь.Если X равно Positive'Last, то 2**(Floor_Log2'Result + 1) превышает Positive'Last и Natural'Last.Здесь я уже сталкиваюсь с ограниченным знанием Ады, поэтому: Подвопрос 1: Какого типа подвыражение в условии post, и является ли это переполнением проблемой?Есть ли общий способ решить это?Чтобы избежать этой проблемы в данном конкретном случае, я изменил спецификацию на менее интуитивно понятную, но эквивалентную:
package Util is
function Floor_Log2(X : Positive) return Natural with
Post => 2**Floor_Log2'Result <= X and then X/2 < 2**Floor_Log2'Result;
end Util;
Существует много способов реализации этой функции, и меня это не особо беспокоитточка, так что я был бы счастлив с любым из них.Я бы посчитал, что «естественная» реализация (учитывая мой конкретный C-фон) выглядит примерно так: util.adb:
package body Util is
function Floor_Log2 (X : Positive) return Natural is
I : Natural := 0;
Remaining : Positive := X;
begin
while Remaining > 1 loop
I := I + 1;
Remaining := Remaining / 2;
end loop;
return I;
end Floor_Log2;
end Util;
Попытка доказать это без инвариантов цикла не удалась, как и ожидалось.Результаты (это и все результаты GNATprove уровня 4, вызванные из GPS как gnatprove -P%PP -j0 %X --ide-progress-bar -u %fp --level=4 --report=all):
util.adb:6:13: info: initialization of "Remaining" proved[#2]
util.adb:7:15: info: initialization of "I" proved[#0]
util.adb:7:17: medium: overflow check might fail[#5]
util.adb:8:23: info: initialization of "Remaining" proved[#1]
util.adb:8:33: info: range check proved[#4]
util.adb:8:33: info: division check proved[#8]
util.adb:10:14: info: initialization of "I" proved[#3]
util.ads:3:14: medium: postcondition might fail, cannot prove 2**Floor_Log2'Result <= X[#7]
util.ads:3:15: medium: overflow check might fail[#9]
util.ads:3:50: info: division check proved[#6]
util.ads:3:56: info: overflow check proved[#10]
Большинство ошибок здесь имеют для меня основной смысл.Начиная с первой проверки переполнения, GNATprove не может доказать, что цикл завершается менее чем за Natural'Last итераций (или вообще?), Поэтому он не может доказать, что I := I + 1 не переполняется.Мы знаем, что это не так, потому что Remaining уменьшается.Я попытался выразить это добавлением варианта цикла pragma Loop_Variant (Decreases => Remaining), и GNATprove смог доказать этот вариант цикла, но потенциальное переполнение I := I + 1 не изменилось, предположительно, потому что доказательство завершения цикла вообще не эквивалентно доказательству того, что он завершаетсяменее чем за Positive'Last итераций.Более жесткое ограничение показало бы, что цикл завершается не более чем Positive'Size итераций, но я не уверен, как это доказать.Вместо этого я «принудил это», добавив pragma Assume (I <= Remaining'Size);Я знаю, что это плохая практика, цель здесь состояла лишь в том, чтобы показать мне, как далеко я смогу продвинуться с этим первым выпуском, «скрытым под одеялом».Как и ожидалось, это предположение позволяет проверяющему доказать все проверки диапазона в файле реализации. Подвопрос 2: Как правильно доказать, что I не переполняется в этом цикле?
Однако мы до сих пор не достигли прогресса в доказательстве постусловия.Инвариант цикла явно необходим.Один инвариант цикла, который выполняется в верхней части цикла, состоит в том, что pragma Loop_Invariant (Remaining * 2**I <= X and then X/2 < Remaining * 2**I);Помимо того, что это истина, этот инвариант обладает хорошим свойством, что он явно эквивалентен постусловию, когда условие завершения цикла истинно.Однако, как и ожидалось, GNATprove не может доказать этот инвариант: medium: loop invariant might fail after first iteration, cannot prove Remaining * 2**I <= X[#20].Это имеет смысл, потому что индуктивный шаг здесь неочевиден.С делением на действительные числа можно представить простую лемму о том, что for all I, X * 2**I = (X/2) * 2**(I+1), но (а) я не ожидаю, что GNATprove узнает об этом без предоставления леммы, и (б) это сложнее с целочисленным делением.Итак, Подвопрос 3a: Является ли этот цикл подходящим инвариантом, который нужно использовать для доказательства этой реализации? Подвопрос 3b: Если да, то как правильно доказать это?Внешне доказать лемму и использовать это?Если это так, что именно это означает?
На этом этапе я подумал, что исследую совершенно другую реализацию, просто чтобы посмотреть, приведет ли она к чему-то другому:
package body Util is
function Floor_Log2 (X : Positive) return Natural is
begin
for I in 1 .. X'Size - 1 loop
if 2**I > X then
return I - 1;
end if;
end loop;
return X'Size - 1;
end Floor_Log2;
end Util;
Это менее интуитивная реализация для меня.Я не особо изучал эту вторую реализацию, но оставляю ее здесь, чтобы показать, что я пытался;дать потенциальные возможности для других решений основного вопроса;и поднять дополнительные подвопросы.
Идея состояла в том, чтобы обойти некоторые доказательства вокруг переполнения I и условий завершения, сделав окончание и диапазоны явными.К моему удивлению, испытатель сначала подавился переполнением, проверяя выражение 2**I.Я ожидал, что 2**(X'Size - 1) будет доказуемо в пределах X - но, опять же, я столкнулся с пределами моего знания Ады. Подвопрос 4: Является ли это выражение на самом деле свободным от переполнения в Аде, и как это можно доказать?
Это оказалось длинным вопросом ... но я думаю, чтоВопросы, которые я поднимаю, в контексте почти тривиального примера, являются относительно общими и, вероятно, будут полезны для других, которые, как и я, пытаются понять, относится ли Spark к ним и насколько они важны.