Module 270: Changes to add more meaningful names, where appropriate, for single vars

courses/ada_essentials/270_introduction_to_contracts/01-introduction.rst

@@ -81,12 +81,12 @@ Defensive Programming
 
 .. code:: Ada
 
-   procedure Push (S : Stack) is
-      Entry_Length : constant Positive := Length (S);
+   procedure Push (Stack : Stack_Type) is
+      Entry_Length : constant Positive := Length (Stack);
    begin
-      pragma Assert (not Is_Full (S)); -- entry condition
+      pragma Assert (not Is_Full (Stack)); -- entry condition
       [...]
-      pragma Assert (Length (S) = Entry_Length + 1); -- exit condition
+      pragma Assert (Length (Stack) = Entry_Length + 1); -- exit condition
    end Push;
 
 * Subprogram contracts are an **assertion** mechanism
@@ -95,15 +95,15 @@ Defensive Programming
 
 .. code:: Ada
 
-   procedure Force_Acquire (P : Peripheral) is
+   procedure Force_Acquire (Resource : Shared_Resource) is
    begin
-      if not Available (P) then
+      if not Available (Resource) then
          -- Corrective action
-         Force_Release (P);
-         pragma Assert (Available (P));
+         Force_Release (Resource);
+         pragma Assert (Available (Resource));
       end if;
 
-      Acquire (P);
+      Acquire (Resource);
    end;
 
 ------

courses/ada_essentials/270_introduction_to_contracts/02-preconditions_and_postconditions.rst

@@ -148,10 +148,10 @@ Function result can be referenced by :ada:`'Result` on the function name
 
    .. code:: Ada
 
-      function Greatest_Common_Denominator (A, B : Integer)
+      function Greatest_Common_Denominator (Num1, Num2 : Integer)
         return Integer with
-          Pre  => A > 0 and B > 0,
-          Post => Is_GCD (A, B,
+          Pre  => Num1 > 0 and Num2 > 0,
+          Post => Is_GCD (Num1, Num2,
                           Greatest_Common_Denominator'Result);
 
 ------------------------------------------
@@ -173,16 +173,16 @@ Quiz
 
 .. code:: Ada
 
-   function Area (L : Positive; H : Positive) return Positive is
-      (L * H)
+   function Area (Length : Positive; Height : Positive) return Positive is
+      (Length * Height)
    with Pre => ?
 
 Which pre-condition is necessary for :ada:`Area` to calculate the correct result for
-all values :ada:`L` and :ada:`H`?
+all values :ada:`Length` and :ada:`Height`?
 
-   A. ``L > 0 and H > 0``
-   B. ``L < Positive'Last and H < Positive'Last``
-   C. ``L * H in Positive``
+   A. ``Length > 0 and Height > 0``
+   B. ``Length < Positive'Last and Height < Positive'Last``
+   C. ``Length * Height in Positive``
    D. :answer:`None of the above`
 
 .. container:: animate
@@ -195,7 +195,7 @@ all values :ada:`L` and :ada:`H`?
 
    The correct precondition would be
 
-         :ada:`Integer'Last / L <= H`
+         :ada:`Integer'Last / Length <= Height`
 
    to prevent overflow errors on the range check.
 
@@ -243,17 +243,17 @@ Separations of Concerns
 
 .. code:: Ada
 
-   function Val return Integer
-    with Post => F'Result /= 0
-   is (if Val_Raw > 0 then Val_Raw else 1);
+   function Validated_Value (Raw_Value : Integer) return Integer
+    with Post => Validated_Value'Result /= 0
+   is (if Raw_Value > 0 then Raw_Value else 1);
 
-   procedure Process (I : Integer)
-    with Pre => I /= 0
-   is (Set_Output (10 / I));
+   procedure Process (Input_Value : Integer)
+    with Pre => Input_Value /= 0
+   is (Set_Output (10 / Input_Value));
 
    [...]
 
-   Process (Val);
+   Process (Validated_Value);
 
 * Review of interface: guaranteed to work
 
@@ -281,12 +281,12 @@ No Secret Precondition Requirements
 
 .. code:: Ada
 
-   package P is
+   package Basic_Package is
      function Foo return Bar
        with Pre => Hidden; -- illegal private reference
    private
      function Hidden return Boolean;
-   end P;
+   end Basic_Package;
 
 ---------------------------------------
 Postconditions Are Good Documentation

courses/ada_essentials/270_introduction_to_contracts/03-type_invariants.rst

@@ -127,35 +127,38 @@ Quiz
 
    .. code:: Ada
 
-      package P is
-         type Some_T is private;
-         procedure Do_Something (X : in out Some_T);
+      package Counter_System is
+         type Counter_T is private;
+         procedure Increment (Val_To_Inc : 
+                              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 Is_Valid (Val_To_Check : Integer) 
+            return Boolean;
+         type Counter_T is new Integer with
+            Type_Invariant => Is_Valid (Integer (Counter_T));
+      end Counter_System;
+
+      package body Counter_System is
+         function Increment_Helper (Helper_Num : Counter_T)
+                                      return Counter_T is
+            New_Val : Counter_T := Helper_Num + 1;
          begin
-            return Z;
-         end Local_Do_Something;
-         procedure Do_Something (X : in out Some_T) is
+            return New_Val;
+         end Increment_Helper;
+         procedure Increment (Val_To_Inc : 
+                              in out Counter_T) is
          begin
-            X := X + 1;
-            X := Local_Do_Something (X);
-         end Do_Something;
-         function Counter (I : Integer)
+            Val_To_Inc := Val_To_Inc + 1;
+            Val_To_Inc := Increment_Helper (Val_To_Inc);
+         end Increment;
+         function Is_Valid (Val_To_Check : Integer)
                            return Boolean is
             (True);
-      end P;
+      end Counter_System;
 
  .. 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_System, how many times is `Is_Valid` called?
 
        A. 1
        B. :answer:`2`
@@ -165,7 +168,7 @@ 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
+       externally visible subprograms. So :ada:`Is_Valid` is called when
+       entering and exiting :ada:`Increment` - not :ada:`Increment_Helper`,
+       even though a new instance of :ada:`Counter_T` is created
 

courses/ada_essentials/270_introduction_to_contracts/04-subtype_predicates.rst

@@ -112,7 +112,7 @@ Predicate Expression Content
 
       subtype Even is Integer
         with Dynamic_Predicate => Even mod 2 = 0;
-      J, K : Even := 42;
+      Even_Num, Also_Even_Num : Even := 42;
 
 * Any visible object or function in scope
 
@@ -177,29 +177,29 @@ Beware Accidental Recursion in Predicate
 
    .. code:: Ada
 
-      type Sorted_Table is array (1 .. N) of Integer with
+      type Sorted_Table is array (1 .. Max_Size) of Integer with
          Dynamic_Predicate => Sorted (Sorted_Table);
       -- on call, predicate is checked!
-      function Sorted (T : Sorted_Table) return Boolean;
+      function Sorted (A_Table : Sorted_Table) return Boolean;
 
 * Non-recursive example
 
    .. code:: Ada
 
-      type Sorted_Table is array (1 .. N) of Integer with
+      type Sorted_Table is array (1 .. Max_Size) 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 Rows in Sorted_Table'Range =>
+            (Row = Sorted_Table'First
+             or else Sorted_Table (Row - 1) <= Sorted_Table (Row)));
 
 * Type-based example
 
    .. code:: Ada
 
-      type Table is array (1 .. N) of Integer;
-      subtype Sorted_Table is Table with
+      type Table_Type is array (1 .. Max_Size) of Integer;
+      subtype Sorted_Table is Table_Type with
            Dynamic_Predicate => Sorted (Sorted_Table);
-      function Sorted (T : Table) return Boolean;
+      function Sorted (A_Table : Table_Type) return Boolean;
 
 ------
 Quiz
@@ -208,20 +208,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 (The_Day : Days_T) return Boolean is
+      (The_Day /= Sun and then The_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 Wknd is Days_T with`
+   |    :answermono:`Static_Predicate => Wknd in Sun | Sat;`
+B. | ``subtype Wknd is Days_T with Static_Predicate =>``
+   |    ``(if Wknd = Sun or else Wknd = Sat then True else False);``
+C. | ``subtype Wknd is Days_T with``
+   |    ``Static_Predicate => not Is_Weekday (Wknd);``
+D. | ``subtype Wknd is Days_T with``
    |    ``Static_Predicate =>``
-   |       ``case T is when Sat | Sun => True,``
+   |       ``case Wknd is when Sat | Sun => True,``
    |                 ``when others => False;``
 
 .. container:: animate