Испытание Floor_Log2 в Искре
Новичок в 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 будет знать, что без предоставления леммы, и (б) это сложнее с целочисленным делением. Итак, подвопрос 3а. Является ли этот цикл подходящим инвариантом, который нужно использовать для доказательства этой реализации? Подвопрос 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. Является ли это выражение на самом деле свободным от переполнения в Ada, и как это можно доказать?
Это оказалось длинным вопросом... но я думаю, что вопросы, которые я поднимаю, в контексте почти тривиального примера, являются относительно общими и, вероятно, будут полезны для других, которые, как и я, пытаются понять, если и как Spark имеет к ним отношение.
1 ответ
Я не могу помочь с вашими вопросами SPARK, но я могу ответить на некоторые ваши подвопросы.
Подвопрос 1: Поскольку вы используете "<" для Integer подвыражение также будет иметь тип Integer. За Positive'Last (2 ** 31 - 1 с GNAT), результат вашей функции должен быть 30, и подвыражение будет переполнено. (Это с точки зрения SPARK; компиляторам разрешается использовать более ранжированные типы при оценке выражений для получения математически / логически правильного результата, даже если подвыражение будет переполнено, и GNAT сделает это для некоторых значений -gnato.)
Подвопрос 4: 2 ** (X'Size - 1) может переполниться. Причина связана с 2 значениями 'Size: Positive'Size минимальное количество битов, необходимое для хранения значения подтипа Positive; X'Size фактическое количество бит, выделенных для X. Поскольку вы используете GNAT,
Integer'Last = Positive'Last = 2 ** 31 - 1, X'Size = 32, Positive'Size = 31,
Так, 2 ** (X'Size - 1) = 2 ** 31 > Positive'Last, Вы, вероятно, хотите использовать Positive'Size вместо X'Size,
(Опять же, с точки зрения SPARK; компиляторам разрешено получать логически правильный результат.)
В сторону: формы короткого замыкания and then а также or else следует использовать только тогда, когда они действительно необходимы. Современные процессоры выполняют все виды оптимизаций на уровне машинного кода, которые должны быть отключены для оценки короткого замыкания. Хотя они могут выглядеть как оптимизация, на практике они часто бывают противоположными.
НТН.
(Возможно, вы захотите пометить это с помощью [ada]. Я видел это только потому, что вы ссылались на него в clada.)
While this question is already over 6 months old I think it's still interesting so here's my (late) bet:-).
Preventing overflow in the post condition
Given the original function signature
function Floor_Log2 (X : Positive) return Natural with
Post => 2**Floor_Log2'Result <= X and then X < 2**(Floor_Log2'Result + 1);
I observe that I need to limit the domain of X in order to prevent overflow in the second term of the post condition. Given the definitions in Standard.ads, i.e.
type Integer is range -(2**31) .. +(2**31 - 1);
for Integer'Size use 32;
subtype Natural is Integer range 0 .. Integer'Last;
subtype Positive is Integer range 1 .. Integer'Last;
I conclude that, in order to prevent overflow,
X < 2**(Floor_Log2'Result + 1) <= 2**31 - 1
and therefore X <= 2**30 - 1. Hence, I changed the function signature to:
subtype Pos is Positive range 1 .. 2**30 - 1
function Floor_Log2 (X : Pos) return Natural with
Post => 2**Floor_Log2'Result <= X and then X < 2**(Floor_Log2'Result + 1);
First Approach
In principle, I could now proof the post condition as follows in GNAT CE 2019 (note that I use a different algorithm compared to the one stated in the question):
util.ads
package Util with SPARK_Mode is
subtype Pos is Positive range 1 .. 2**30 - 1
function Floor_Log2 (X : Pos) return Natural with
Post => 2**Floor_Log2'Result <= X and then X < 2**(Floor_Log2'Result + 1);
end Util;
util.adb
package body Util with SPARK_Mode is
----------------
-- Floor_Log2 --
----------------
function Floor_Log2 (X : Pos) return Natural is
L : Positive := 1;
H : Positive := L * 2;
I : Natural := 0;
begin
while not (L <= X and then X < H) loop
pragma Loop_Invariant
(L = 2 ** I and H = 2 ** (I+1));
pragma Loop_Invariant
(for all J in 0 .. I =>
not (2 ** J <= X and then X < 2 ** (J+1)));
L := H;
H := H * 2;
I := I + 1;
end loop;
return I;
end Floor_Log2;
end Util;
Unfortunately, however, the provers have difficulties with the non-linear arithmetic (i.e. exponentiation) and all proof sessions (on my computer) end with a timeout. In fact, if I run gnatprove with effort level 0, then I can only proof the post condition when I limit the upper bound of Pos to 2**7 - 1, i.e.
subtype Pos is Positive range 1 .. 2**7 - 1;
Increasing the effort level (or timeout) allows me to proof the post condition for larger values of Pos'Last.
Second Approach
In order to work around the limitation of the provers, I applied a little trick by redefining the exponentiation function. I could then use the following code to prove the post condition for the full range of Pos when I run gnatprove with effort level 1:
spark_exp.ads
generic
type Int is range <>;
Base : Int;
N_Max : Natural;
package SPARK_Exp with SPARK_Mode is
subtype Exp_T is Natural range 0 .. N_Max;
function Exp (N : Exp_T) return Int with Ghost;
private
type Seq_T is array (Exp_T range <>) of Int;
function Exp_Seq return Seq_T with
Ghost,
Post => (Exp_Seq'Result'First = 0)
and then (Exp_Seq'Result'Last = N_Max)
and then (Exp_Seq'Result (0) = 1)
and then (for all I in 1 .. N_Max =>
Exp_Seq'Result (I) = Base * Exp_Seq'Result (I - 1) and
Int'First < Exp_Seq'Result (I) and Exp_Seq'Result (I) < Int'Last);
function Exp (N : Exp_T) return Int is (Exp_Seq (N));
end SPARK_Exp;
spark_exp.adb
package body SPARK_Exp with SPARK_Mode is
-------------
-- Exp_Seq --
-------------
function Exp_Seq return Seq_T is
S : Seq_T (Exp_T'Range) := (others => 1);
begin
for I in 1 .. N_Max loop
pragma Loop_Invariant
(for all J in 1 .. I - 1 =>
S (J) = Base * S (J - 1) and
(Int'First / Base) < S (J) and S (J) < (Int'Last / Base));
S (I) := Base * S (I - 1);
end loop;
return S;
end Exp_Seq;
end SPARK_Exp;
util.ads
with SPARK_Exp;
package Util with SPARK_Mode is
subtype Pos is Positive range 1 .. 2**30 - 1;
package SPARK_Exp_2 is
new SPARK_Exp (Positive, 2, 30);
function Exp2 (N : SPARK_Exp_2.Exp_T) return Positive
renames SPARK_Exp_2.Exp;
function Floor_Log2 (X : Pos) return Natural with
Post => (Exp2 (Floor_Log2'Result) <= X) and then
(X < Exp2 (Floor_Log2'Result + 1));
end Util;
util.adb
package body Util with SPARK_Mode is
----------------
-- Floor_Log2 --
----------------
function Floor_Log2 (X : Pos) return Natural is
L : Positive := 1;
H : Positive := L * 2;
I : Natural := 0;
begin
while not (L <= X and then X < H) loop
pragma Loop_Invariant
(L = Exp2 (I) and H = Exp2 (I + 1));
pragma Loop_Invariant
(for all J in 0 .. I =>
not (Exp2 (J) <= X and then X < Exp2 (J + 1)));
L := H;
H := H * 2;
I := I + 1;
end loop;
return I;
end Floor_Log2;
end Util;
Эта реализация доказывает все проверки внутри тела, но предварительные условия все еще не доказаны:
package body Util is
pragma SPARK_Mode (On);
function Floor_Log2 (X : Positive) return Natural is
I : Natural := 30;
Prod : Natural := 2**30;
type Large_Natural is range 0 .. 2**31;
Prev_Prod : Large_Natural := Large_Natural'Last with Ghost;
begin
while I > 0 loop
if X >= Prod then
pragma Assert (Large_Natural (X) < Prev_Prod);
return I;
end if;
pragma Loop_Invariant (I > 0);
pragma Loop_Invariant (Prod >= X and Prev_Prod >= Large_Natural (X));
-- pragma Loop_Invariant (2**I > X);
Prod := Prod / 2;
I := I - 1;
end loop;
pragma Assert (I = 0);
return 0;
end Floor_Log2;
end Util;
Это дает следующий вывод с gnatprove:
gnatprove -P/Users/pnoffke/projects/ada/spark/floor_log2/floor_log2.gpr -j0 --ide-progress-bar -u util.adb --level=2 --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
util.adb:10:13: info: initialization of "I" proved
util.adb:11:18: info: initialization of "Prod" proved
util.adb:12:28: info: assertion proved
util.adb:12:48: info: initialization of "Prev_Prod" proved
util.adb:13:20: info: initialization of "I" proved
util.adb:15:33: info: initialization of "I" proved
util.adb:15:33: info: loop invariant preservation proved
util.adb:15:33: info: loop invariant initialization proved
util.adb:16:33: info: initialization of "Prod" proved
util.adb:16:33: info: loop invariant preservation proved
util.adb:16:33: info: loop invariant initialization proved
util.adb:16:47: info: initialization of "Prev_Prod" proved
util.adb:18:18: info: initialization of "Prod" proved
util.adb:18:23: info: division check proved
util.adb:19:15: info: initialization of "I" proved
util.adb:19:17: info: range check proved
util.adb:22:22: info: initialization of "I" proved
util.adb:22:22: info: assertion proved
util.ads:5:15: info: overflow check proved
util.ads:5:44: medium: postcondition might fail, cannot prove X / 2 < 2**Floor_Log2'result (e.g. when Floor_Log2'Result = 0 and X = 2)
util.ads:5:46: info: division check proved
util.ads:5:53: medium: overflow check might fail (e.g. when Floor_Log2'Result = 30)
Я не понимаю, почему gnatprove не может доказать комментарий Loop_Invariant, Если я попытаюсь это сделать, я получу следующий дополнительный вывод:
util.adb:17:33: medium: loop invariant might fail after first iteration, cannot prove 2**I > X (e.g. when I = 0 and X = 0)
util.adb:17:33: medium: loop invariant might fail in first iteration, cannot prove 2**I > X (e.g. when I = 30 and X = 1)
util.adb:17:34: medium: overflow check might fail (e.g. when I = 0)
В контрпримере сказано:when I = 0 and X = 0", но I не может быть 0 за первый Loop_Invariant,
Также если я инициализирую Prod в 2**I вместо 2**30, Я получил:
util.adb:6:26: medium: overflow check might fail (e.g. when I = 30 and Prod = 0)
Я подозреваю, что у gnatprove есть фундаментальная проблема с ** оператор. Я надеялся использовать Prev_Prod чтобы помочь доказать ваши предварительные условия, но я не понимаю, как добраться с вышеупомянутыми проблемами, которые у меня есть.