Merge branch 'slides/276_type_contracts-code-snippets-should-use-better-names-than-single-characters' into 'master'

dm-at-ada · dm-at-ada · commit beb7d1ac89a2 · 2025-01-09T17:30:29.000Z
276_type_contracts: Renaming single var names to something a little more meaningful

See merge request feng/training/material!263
diff --git a/courses/fundamentals_of_ada/276_type_contracts/02-type_invariants.rst b/courses/fundamentals_of_ada/276_type_contracts/02-type_invariants.rst
@@ -135,20 +135,20 @@ Default Type Initialization for Invariants
 
 .. code:: Ada
 
-   package P is
+   package Operations is
      -- Type is private, so we can't use Default_Value here
-     type T is private with Type_Invariant => Zero (T);
-     procedure Op (This : in out T);
-     function Zero (This : T) return Boolean;
+     type Private_T is private with Type_Invariant => Zero (Private_T);
+     procedure Op (This : in out Private_T);
+     function Zero (This : Private_T) return Boolean;
    private
      -- Type is not a record, so we need to use aspect
      -- (A record could use default values for its components)
-     type T is new Integer with Default_Value => 0;
-     function Zero (This : T) return Boolean is
+     type Private_T is new Integer with Default_Value => 0;
+     function Zero (This : Private_T) return Boolean is
      begin
         return (This = 0);
      end Zero;
-   end P;
+   end Operations;
 
 ---------------------------------
 Type Invariant Clause Placement
@@ -158,14 +158,14 @@ Type Invariant Clause Placement
 
    .. code:: Ada
 
-      package P is
-        type T is private;
-        procedure Op (This : in out T);
+      package Operations is
+        type Private_T is private;
+        procedure Op (This : in out Private_T);
       private
-        type T is new Integer with
-          Type_Invariant => T = 0,
+        type Private_T is new Integer with
+          Type_Invariant => Private_T = 0,
           Default_Value => 0;
-      end P;
+      end Operations;
 
 * It is really an implementation aspect
 
@@ -197,35 +197,37 @@ Quiz
 
    .. code:: Ada
 
-      package P is
-         type Some_T is private;
-         procedure Do_Something (X : in out Some_T);
+      package Counter_Package is
+         type Counter_T is private;
+         procedure Increment (Val : in out Counter_T);
       private
-         function Counter (I : Integer) return Boolean;
-         type Some_T is new Integer with
-            Type_Invariant => Counter (Integer (Some_T));
-      end P;
-
-      package body P is
-         function Local_Do_Something (X : Some_T)
-                                      return Some_T is
-            Z : Some_T := X + 1;
+         function Check_Threshold (Value : Integer) 
+                                       return Boolean;
+         type Counter_T is new Integer with
+            Type_Invariant => Check_Threshold 
+                              (Integer (Counter_T));
+      end Counter_Package;
+
+      package body Counter_Package is
+         function Increment_Helper (Helper_Val : Counter_T)
+                                      return Counter_T is
+            Next_Value : Counter_T := Helper_Val + 1;
          begin
-            return Z;
-         end Local_Do_Something;
-         procedure Do_Something (X : in out Some_T) is
+            return Next_Value;
+         end Increment_Helper;
+         procedure Increment (Val : in out Counter_T) is
          begin
-            X := X + 1;
-            X := Local_Do_Something (X);
-         end Do_Something;
-         function Counter (I : Integer)
-                           return Boolean is
-            (True);
-      end P;
+            Val := Val + 1;
+            Val := Increment_Helper (Val);
+         end Increment;
+         function Check_Threshold (Value : Integer)
+                                          return Boolean is
+            (Value <= 100); --  check against constraint
+      end Counter_Package;
 
  .. container:: column
 
-    If `Do_Something` is called from outside of P, how many times is `Counter` called?
+    If `Increment` is called from outside of Counter_Package, how many times is `Check_Threshold` called?
 
        A. 1
        B. :answer:`2`
@@ -234,8 +236,6 @@ Quiz
 
     .. container:: animate
 
-       Type Invariants are only evaluated on entry into and exit from
-       externally visible subprograms. So :ada:`Counter` is called when
-       entering and exiting :ada:`Do_Something` - not :ada:`Local_Do_Something`,
-       even though a new instance of :ada:`Some_T` is created
-
+       Type Invariants are only evaluated on entry into/exit from
+       externally visible subprograms. So :ada:`Check_Threshold` is called when
+       entering/exiting :ada:`Increment` - not :ada:`Increment_Helper`
diff --git a/courses/fundamentals_of_ada/276_type_contracts/03-subtype_predicates.rst b/courses/fundamentals_of_ada/276_type_contracts/03-subtype_predicates.rst
@@ -156,28 +156,28 @@ References Are Not Checked
 .. code:: Ada
 
    with Ada.Text_IO;   use Ada.Text_IO;
-   procedure Test is
+   procedure Even_Number_Test is
      subtype Even is Integer with Dynamic_Predicate => Even mod 2 = 0;
-     J, K : Even;
+     Current_Value, Next_Value : Even;
    begin
      -- predicates are not checked here
-     Put_Line ("K is" & K'Image);
-     Put_Line ("J is" & J'Image);
+     Put_Line ("Current_Value is" & Current_Value'Image);
+     Put_Line ("Next_Value is" & Next_Value'Image);
      -- predicate is checked here
-     K := J; -- assertion failure here
-     Put_Line ("K is" & K'Image);
-     Put_Line ("J is" & J'Image);
-   end Test;
+     Current_Value := Next_Value; -- assertion failure here
+     Put_Line ("Current_Value is" & Current_Value'Image);
+     Put_Line ("Next_Value is" & Next_Value'Image);
+   end Even_Number_Test;
 
 * Output would look like
 
     .. code:: Ada
 
-       K is 1969492223
-       J is 4220029
+       Current_Value is 1969492223
+       Next_Value is 4220029
 
        raised SYSTEM.ASSERTIONS.ASSERT_FAILURE:
-       Dynamic_Predicate failed at test.adb:9
+       Dynamic_Predicate failed at even_number_test.adb:9
 
 ------------------------------
 Predicate Expression Content
@@ -189,7 +189,7 @@ Predicate Expression Content
 
       subtype Even is Integer
         with Dynamic_Predicate => Even mod 2 = 0;
-      J, K : Even := 42;
+      Current_Value, Next_Value : Even := 42;
 
 * Any visible object or function in scope
 
@@ -309,7 +309,7 @@ Types Controlling For-Loops
            with Dynamic_Predicate => Even mod 2 = 0;
          ...
          -- not legal - how many iterations?
-         for K in Even loop
+         for A_Number in Even loop
            ...
          end loop;
 
@@ -321,8 +321,8 @@ Types Controlling For-Loops
       subtype Weekend is Days
         with Static_Predicate => Weekend in Sat | Sun;
       -- Loop uses "Days", and only enters loop when in Weekend
-      -- So "Sun" is first value for K
-      for K in Weekend loop
+      -- So "Sun" is first value for A_Day
+      for A_Day in Weekend loop
          ...
       end loop;
 
@@ -337,26 +337,26 @@ Why Allow Types with Static Predicates?
       type Days is (Sun, Mon, Tues, We, Thu, Fri, Sat);
       subtype Weekend is Days with Static_Predicate => Weekend in Sat | Sun;
       ...
-      for W in Weekend loop
-        GNAT.IO.Put_Line (W'Image);
+      for A_Day in Weekend loop
+        GNAT.IO.Put_Line (A_Day'Image);
       end loop;
 
 * :ada:`for` loop generates code like
 
    .. code:: Ada
 
       declare
-        w : weekend := sun;
+        a_day : weekend := sun;
       begin
         loop
-          gnat__io__put_line__2 (w'Image);
-          case w is
+          gnat__io__put_line__2 (a_day'Image);
+          case a_day is
             when sun =>
-              w := sat;
+              a_day := sat;
             when sat =>
               exit;
             when others =>
-              w := weekend'succ (w);
+              a_day := weekend'succ (a_day);
           end case;
         end loop;
       end;
@@ -375,7 +375,7 @@ In Some Cases Neither Kind Is Allowed
 
    type Play is array (Weekend) of Integer; -- illegal
    type Vector is array (Days range <>) of Integer;
-   L : Vector (Weekend); -- not legal
+   Not_Legal : Vector (Weekend); -- not legal
 
 -----------------------------------------
 Special Attributes for Predicated Types
@@ -409,7 +409,7 @@ Initial Values Can Be Problematic
 
          subtype Even is Integer
            with Dynamic_Predicate => Even mod 2 = 0;
-         K : Even;  -- unknown (invalid?) initial value
+         Some_Number : Even;  -- unknown (invalid?) initial value
 
 * The predicate is not checked on a declaration when no initial value is given
 * So can reference such junk values before assigned
@@ -428,8 +428,8 @@ Subtype Predicates Aren't Bullet-Proof
      type Table is array (1 .. 5) of Integer
        -- array should always be sorted
        with Dynamic_Predicate =>
-         (for all K in Table'Range =>
-           (K = Table'First or else Table (K-1) <= Table (K)));
+         (for all Idx in Table'Range =>
+           (Idx = Table'First or else Table (Idx-1) <= Table (Idx)));
      Values : Table := (1, 3, 5, 7, 9);
    begin
      ...
@@ -460,9 +460,9 @@ Beware Accidental Recursion in Predicate
 
       type Sorted_Table is array (1 .. N) of Integer with
          Dynamic_Predicate =>
-         (for all K in Sorted_Table'Range =>
-            (K = Sorted_Table'First
-             or else Sorted_Table (K - 1) <= Sorted_Table (K)));
+         (for all Index in Sorted_Table'Range =>
+            (Index = Sorted_Table'First
+             or else Sorted_Table (Index - 1) <= Sorted_Table (Index)));
 
 * Type-based example
 
@@ -526,20 +526,20 @@ Quiz
 .. code:: Ada
 
    type Days_T is (Sun, Mon, Tue, Wed, Thu, Fri, Sat);
-   function Is_Weekday (D : Days_T) return Boolean is
-      (D /= Sun and then D /= Sat);
+   function Is_Weekday (Day : Days_T) return Boolean is
+      (Day /= Sun and then Day /= Sat);
 
 Which of the following is a valid subtype predicate?
 
-A. | :answermono:`subtype T is Days_T with`
-   |    :answermono:`Static_Predicate => T in Sun | Sat;`
-B. | ``subtype T is Days_T with Static_Predicate =>``
-   |    ``(if T = Sun or else T = Sat then True else False);``
-C. | ``subtype T is Days_T with``
-   |    ``Static_Predicate => not Is_Weekday (T);``
-D. | ``subtype T is Days_T with``
+A. | :answermono:`subtype Sub_Day is Days_T with`
+   |    :answermono:`Static_Predicate => Sub_Day in Sun | Sat;`
+B. | ``subtype Sub_Day is Days_T with Static_Predicate =>``
+   |    ``(if Sub_Day = Sun or else Sub_Day = Sat then True else False);``
+C. | ``subtype Sub_Day is Days_T with``
+   |    ``Static_Predicate => not Is_Weekday (Sub_Day);``
+D. | ``subtype Sub_Day is Days_T with``
    |    ``Static_Predicate =>``
-   |       ``case T is when Sat | Sun => True,``
+   |       ``case Sub_Day is when Sat | Sun => True,``
    |                 ``when others => False;``
 
 .. container:: animate
