package body Circle with SPARK_Mode => On Is
   procedure Burn_Circle(Radius : Unsigned_8; DAC : in out DAC_T) is
      Y : Unsigned_8;
   begin
      DAC.Channels(Beam_Channel).Voltage := Voltage_T'Last;
      High_Half:for X in X0 - Radius .. X0 + Radius loop
         Y := Compute_Y(X, Radius);
         --Y1 := 2*Radius - Y;
         DAC.Channels(X_Channel).Voltage := Voltage_T(X);
         DAC.Channels(Y_Channel).Voltage := Voltage_T(Y);
         Set_Voltages(DAC);
      end loop High_Half;

      Low_Half:for X in X0 - Radius .. X0 + Radius loop
         Y := Compute_Y(X, Radius);
         Y := 2*Radius - Y;
         DAC.Channels(X_Channel).Voltage := Voltage_T(X);
         DAC.Channels(Y_Channel).Voltage := Voltage_T(Y);
         Set_Voltages(DAC);
      end loop Low_Half;
      DAC.Channels(Beam_Channel).Voltage := 0;
      Set_Voltages(DAC);
   end Burn_Circle;

   function Compute_Y(X, Radius : Unsigned_8) return Unsigned_8 is
   begin
      return Sqrt_Lut.Sqrt(Radius * Radius - (X-X0) * (X-X0)) + Y0;
   end Compute_Y;
end Circle;