定點類型不能正確乘積

Question

我是新來的Ada，並且一直在嘗試定點「delta」類型。具體來說，我創建了一個32位三角洲類型範圍0.0 .. 1.0。但是，當我嘗試平方某些值時，我得到一個CONSTRAINT_ERROR。據我所知，這不應該發生在我指定的範圍內。此錯誤的閾值似乎爲sqrt(1/2)。我使用的是MinGW-w64版本4.8.0中的GNAT。

測試代碼（所有的它編譯中的gnatmake <file>沒有警告/錯誤的形式）：

types.ads：

pragma Ada_2012; 

with Ada.Unchecked_Conversion; 
with Ada.Text_IO; 

package Types is 
    type Fixed_Type is delta 1.0/2**32 range 0.0 .. 1.0 
     with Size => 32; 
    type Modular_Type is mod 2**32 
     with Size => 32; 
    function Fixed_To_Mod is new Ada.Unchecked_Conversion(Fixed_Type, Modular_Type); 
    package MIO is new Ada.Text_IO.Modular_IO(Modular_Type); 
    package FIO is new Ada.Text_IO.Fixed_IO(Fixed_Type); 
end Types; 

specifics.adb：

pragma Ada_2012; 

with Ada.Text_IO; 

with Types; use Types; 

procedure Specifics is 
    package TIO renames Ada.Text_IO; 

    procedure TestValue(val: in Fixed_Type) is 
     square : Fixed_Type; 
    begin 
     square := val * val; 
     TIO.Put_Line("Value " & Fixed_Type'Image(val) & " squares properly."); 
     TIO.Put_Line("Square: " & Fixed_Type'Image(square)); 
     TIO.New_Line; 
    exception 
     when Constraint_Error => 
      TIO.Put_Line("Value " & Fixed_Type'Image(val) & " does not square properly."); 
      TIO.Put_Line("Square: " & Fixed_Type'Image(val * val)); 
      TIO.Put_Line("Not sure how that worked."); 
      TIO.New_Line; 
    end TestValue; 

    function ParseFixed(s: in String; last: in Natural; val: out Fixed_Type) return Boolean is 
     l : Natural; 
    begin 
     FIO.Get(s(s'First..last), val, l); 
     return TRUE; 
    exception 
     when others => 
      TIO.Put_Line("Parsing failed."); 
      return FALSE; 
    end ParseFixed; 

    buffer : String(1..20); 
    last : Natural; 
    f : Fixed_Type; 
begin 
    loop 
     TIO.Put(">>> "); 
     TIO.Get_Line(buffer, last); 
     exit when buffer(1..last) = "quit"; 
     if ParseFixed(buffer, last, f) then 
      TestValue(f); 
     end if; 
    end loop; 
end Specifics; 

輸出特定的.adb：

>>> 0.1 
Value 0.1000000001 squares properly. 
Square: 0.0100000000 

>>> 0.2 
Value 0.2000000000 squares properly. 
Square: 0.0399999998 

>>> 0.4 
Value 0.3999999999 squares properly. 
Square: 0.1599999999 

>>> 0.6 
Value 0.6000000001 squares properly. 
Square: 0.3600000001 

>>> 0.7 
Value 0.7000000000 squares properly. 
Square: 0.4899999998 

>>> 0.75 
Value 0.7500000000 does not square properly. 
Square: -0.4375000000 
Not sure how that worked. 

>>> quit 

不知何故，乘以val本身產生了一個負數，這解釋了CONSTRAINT_ERROR ...但是不用擔心，爲什麼我首先得到一個負數？

然後我決定來測試在該平方數開始失敗的地步，所以我寫了下面的代碼片段：

fixedpointtest.adb：

pragma Ada_2012; 

with Ada.Text_IO; 

with Types; use Types; 

procedure FixedPointTest is 
    package TIO renames Ada.Text_IO; 

    test, square : Fixed_Type := 0.0; 
begin 
    while test /= Fixed_Type'Last loop 
     square := test * test; 
     test := test + Fixed_Type'Delta; 
    end loop; 
exception 
    when Constraint_Error => 
     TIO.Put_Line("Last valid value: " & Fixed_Type'Image(test-Fixed_Type'Delta)); 
     TIO.Put("Hex value: "); 
     MIO.Put(Item => Fixed_To_Mod(test-Fixed_Type'Delta), Base => 16); 
     TIO.New_Line; 
     TIO.Put("Binary value: "); 
     MIO.Put(Item => Fixed_To_Mod(test-Fixed_Type'Delta), Base => 2); 
     TIO.New_Line; 
     TIO.New_Line; 
     TIO.Put_Line("First invalid value: " & Fixed_Type'Image(test)); 
     TIO.Put("Hex value: "); 
     MIO.Put(Item => Fixed_To_Mod(test), Base => 16); 
     TIO.New_Line; 
     TIO.Put("Binary value: "); 
     MIO.Put(Item => Fixed_To_Mod(test), Base => 2); 
     TIO.New_Line; 
     TIO.New_Line; 
end FixedPointTest; 

，並得到了以下的輸出：

Last valid value: 0.7071067810 
Hex value: 16#B504F333# 
Binary value: 2#10110101000001001111001100110011# 

First invalid value: 0.7071067812 
Hex value: 16#B504F334# 
Binary value: 2#10110101000001001111001100110100# 

那麼，sqrt(1/2)，我們再次見面。有人可以向我解釋爲什麼我的代碼是這樣做的嗎？有沒有辦法使它正確地繁殖？

Answer 1

我認爲你所要求的精確度比實際可用的「底層」還要多1位。

你的聲明

type Fixed_Type is delta 1.0/2**32 range 0.0 .. 1.0 
     with Size => 32; 

僅接受，因爲GNAT使用了一個偏置表示;沒有足夠的空間來放置符號。你可以看到這個，因爲0.7071067810被表示爲16#B504F333#，其中最重要的位被設置。因此，當您將0.71乘以0.71時，結果具有最高有效位集;而低級代碼認爲這必須是符號位，所以我們有一個溢出。

如果聲明Fixed_Type作爲

type Fixed_Type is delta 1.0/2**31 range 0.0 .. 1.0 
     with Size => 32; 

都應該很好。

還有一點：在您的報告中，輸入爲0的specifics的行爲。75，你引用的結果

>>> 0.75 
Value 0.7500000000 does not square properly. 
Square: -0.4375000000 
Not sure how that worked. 

我gnatmake specifics.adb -g -gnato -bargs -E重建，結果現在

>>> 0.75 
Value 0.7500000000 does not square properly. 

Execution terminated by unhandled exception 
Exception name: CONSTRAINT_ERROR 
Message: 64-bit arithmetic overflow 
Call stack traceback locations: 
0x100020b79 0x10000ea80 0x100003520 0x100003912 0x10000143e 

和回溯解碼爲

system__arith_64__raise_error (in specifics) (s-arit64.adb:364) 
__gnat_mulv64 (in specifics) (s-arit64.adb:318) 
specifics__testvalue.2581 (in specifics) (specifics.adb:20)  <<<<<<<<<< 
_ada_specifics (in specifics) (specifics.adb:45) 
main (in specifics) (b~specifics.adb:246) 

和specifics.adb:20是

 TIO.Put_Line("Square: " & Fixed_Type'Image(val * val)); 

在異常處理程序中，這又涉及有問題的方塊（在異常處理程序中不是一件好事）。您可以看到在上面的行中打印出的值0.75沒有任何問題：在fixedpointtest.adb中，添加導致最後一個有效值0.7071067810沒有問題。

我很驚訝地發現-gnato檢測到這個錯誤，因爲我以爲它只適用於整數算術;但實際上在GNAT User Guide中有一個討論，它指出它也適用於定點算法。事實證明，就可避免約束錯誤，並通過使用-gnato3得到正確的運算結果：

>>> 0.75 
Value 0.7500000000 squares properly. 
Square: 0.5625000000 

，但只在使用任意多精度算術的成本 - 而不是一個時間約束系統是個好主意！