Renaming single char vars where it makes sense to do so

courses/fundamentals_of_ada/273_subprogram_contracts/02-preconditions_and_postconditions.rst

@@ -71,12 +71,12 @@ Defensive Programming
 
 .. code:: Ada
 
-   procedure Push (S : Stack) is
-      Entry_Length : constant Positive := Length (S);
+   procedure Push (The_Stack : Stack) is
+      Entry_Length : constant Positive := Length (The_Stack);
    begin
-      pragma Assert (not Is_Full (S)); -- entry condition
+      pragma Assert (not Is_Full (The_Stack)); -- entry condition
       [...]
-      pragma Assert (Length (S) = Entry_Length + 1); -- exit condition
+      pragma Assert (Length (The_Stack) = Entry_Length + 1); -- exit condition
    end Push;
 
 * Subprogram contracts are an **assertion** mechanism
@@ -85,15 +85,15 @@ Defensive Programming
 
 .. code:: Ada
 
-   procedure Force_Acquire (P : Peripheral) is
+   procedure Force_Acquire (Resource : Peripheral) 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;
 
 -----------------------------
@@ -196,17 +196,17 @@ Quiz
 .. code:: Ada
 
    --  Convert string to Integer
-   function From_String ( S : String ) return Integer
+   function To_Integer ( S : String ) return Integer
       with Pre => S'Length > 0;
 
-   procedure Do_Something is
-      I : Integer := From_String ("");
+   procedure Print_Something is
+      I : Integer := To_Integer ("");
    begin
       Put_Line (I'Image);
-   end Do_Something;
+   end Print_Something;
 
-Assuming :ada:`From_String` is defined somewhere, what happens
-when :ada:`Do_Something` is run?
+Assuming :ada:`To_Integer` is defined somewhere, what happens
+when :ada:`Print_Something` is run?
 
    A. "0" is printed
    B. Constraint Error exception
@@ -217,7 +217,7 @@ when :ada:`Do_Something` is run?
 
    Explanations
 
-   The call to :ada:`From_String` will fail its precondition, which is considered
+   The call to :ada:`To_Integer` will fail its precondition, which is considered
    an :ada:`Assertion_Error` exception.
 
 ------
@@ -226,25 +226,25 @@ 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`
 
-   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
 
    Explanations
 
    A. Parameters are :ada:`Positive`, so this is unnecessary
-   B. :ada:`L = Positive'Last-1 and H = Positive'Last-1` will still cause an overflow
+   B. :ada:`Length = Positive'Last-1 and Height = Positive'Last-1` will still cause an overflow
    C. Classic trap: the check itself may cause an overflow!
 
-   Preventing an overflow requires using the expression :ada:`Integer'Last / L <= H`
+   Preventing an overflow requires using the expression :ada:`Integer'Last / Length <= Height`
 

courses/fundamentals_of_ada/273_subprogram_contracts/04-in_practice.rst

@@ -36,12 +36,12 @@ No Secret Precondition Requirements
 
 .. code:: Ada
 
-   package P is
+   package Some_Package is
      function Foo return Bar
        with Pre => Hidden; -- illegal private reference
    private
      function Hidden return Boolean;
-   end P;
+   end Some_Package;
 
 ---------------------------------------
 Postconditions Are Good Documentation
@@ -92,18 +92,18 @@ Postcondition Compared to Their Body: Example
 
 .. code:: Ada
 
-   function Greatest_Common_Denominator (A, B : Natural)
+   function Greatest_Common_Denominator (Num1, Num2 : Natural)
      return Integer with
-     Post =>  Is_GCD (A,
-                      B,
+     Post =>  Is_GCD (Num1,
+                      Num2,
                       Greatest_Common_Denominator'Result);
 
-   function Is_GCD (A, B, Candidate : Integer)
+   function Is_GCD (Num1, Num2, Candidate : Integer)
        return Boolean is
-     (A rem Candidate = 0 and
-      B rem Candidate = 0 and
-      (for all K in 1 .. Integer'Min (A,B) =>
-         (if (A rem K = 0 and B rem K = 0)
+     (Num1 rem Candidate = 0 and
+      Num2 rem Candidate = 0 and
+      (for all K in 1 .. Integer'Min (Num1,Num2) =>
+         (if (Num1 rem K = 0 and Num2 rem K = 0)
           then K <= Candidate)));
 
 ----------------------
@@ -145,24 +145,24 @@ Subprogram Contracts on Private Types
 
 .. code:: Ada
 
-   package P is
-     type T is private;
-     procedure Q (This : T) with
-       Pre => This.Total > 0; -- not legal
+   package Bank is
+     type Account is private;
+     procedure Process_Transaction (This : Account) with
+       Pre => This.Balance > 0; -- not legal
      ...
-     function Current_Total (This : T) return Integer;
+     function Current_Balance (This : Account) return Integer;
      ...
-     procedure R (This : T) with
-       Pre => Current_Total (This) > 0; -- legal
+     procedure R (This : Account) with
+       Pre => Current_Balance (This) > 0; -- legal
      ...
    private
-     type T is record
-       Total : Natural ;
+     type Account is record
+       Balance : Natural;
        ...
      end record;
-     function Current_Total (This : T) return Integer is
-         (This.Total);
-   end P;
+     function Current_Balance (This : Account) return Integer is
+         (This.Balance);
+   end Bank;
 
 -----------------------------------
 Preconditions or Explicit Checks?