證明從陣列讀取被初始化火花

Question

給出一個很簡單的SPARK功能可以概括整數數組：

function Add (X, Y : in Ints) return Ints is 
    Sum : Ints; 
begin 
    for i in Ints'Range loop 
     pragma Loop_Invariant (for all j in Ints'First .. i - 1 => Sum(j) = X(j) + Y(j)); -- line 7 
     Sum(i) := X(i) + Y(i); 
    end loop; 

    return Sum; -- line 11 
end Add; 

（其中type Ints is array (Integer range 0 .. 9) of Integer_32）

沒有循環不變編譯工作正常（因爲我有一個先決條件限制了X和Y的元素，使得溢出不會發生）。不過，我需要不變，以示的後置條件的某些屬性，但它會導致：

7:69: warning: "Sum" may be referenced before it has a value 
Phase 2 of 3: analysis and translation to intermediate language ... 
7:10: "Sum" is not initialized 
11:7: warning: "Sum" might not be initialized 

我不知道如何「被初始化」的概念，在證明中的語言表達，所以我不知道如何說服gnatprove沒有發生未初始化的讀取。

我可以通過在函數啓動時明確設置Sum的所有元素爲零來刪除警告，但我希望有更好的方法。

Answer 1

在SPARK中，數組被視爲整個對象，並且不允許像你一樣按組件進行組件初始化。但是，在gnatprove中有一個啓發式規則，它允許在數組範圍內進行簡單的循環操作，就像你一樣。這就是爲什麼沒有循環不變，你不會得到警告。這個啓發式規則隨循環不變而中斷，這就是爲什麼你再次得到警告。

你將不得不使用編譯警告接受警告，如下所述：

https://gcc.gnu.org/onlinedocs/gnat_rm/Pragma-Warnings.html

，避免錯誤你在第7行越來越，你可以以後移動循環不變分配（並相應地更改量化範圍）。