gnatprove_13.2.1_28fc3583/share/examples/spark/spark_book/Chapter-07/led_display.adb

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
with System.Storage_Elements;
package body Led_Display
   with SPARK_Mode    => On,
        Refined_State => (LED_State => Value)
is
   type Octet is mod 2 ** 8;

   Value : Octet
      with
         Size => 8,  -- Use exactly 8 bits for this variable
         Volatile         => True,
         Async_Readers    => True,
         Effective_Writes => True,
         Address => System.Storage_Elements.To_Address(16#FFFF0000#);

   -- Segments 'a' through 'g' are in order from least to most ignificant bit.
   -- Active high.
   Patterns : constant array (Digit_Type) of Octet :=
              (2#0011_1111#, 2#0000_0110#, 2#0101_1011#, 2#0100_1111#,
               2#0110_0110#, 2#0110_1101#, 2#0111_1101#, 2#0000_0111#,
               2#0111_1111#, 2#0110_0111#);

   procedure Display_Digit (Digit : in Digit_Type)
      with Refined_Global => (Output => Value)
   is
   begin
      Value := Patterns (Digit);
   end Display_Digit;

end LED_Display;