From b928bf26674a1b54567f8210d0fa6f0f2fe65bf1 Mon Sep 17 00:00:00 2001 From: dana Date: Thu, 2 Jan 2025 14:31:17 -0500 Subject: [PATCH 1/6] Changes to add more meaningful names, where appropriate, for single vars --- .../01-introduction.rst | 18 ++++---- .../02-preconditions_and_postconditions.rst | 36 +++++++-------- .../03-type_invariants.rst | 44 +++++++++---------- .../04-subtype_predicates.rst | 36 +++++++-------- 4 files changed, 67 insertions(+), 67 deletions(-) diff --git a/courses/fundamentals_of_ada/270_introduction_to_contracts/01-introduction.rst b/courses/fundamentals_of_ada/270_introduction_to_contracts/01-introduction.rst index 8960d29be..ab6299c3a 100644 --- a/courses/fundamentals_of_ada/270_introduction_to_contracts/01-introduction.rst +++ b/courses/fundamentals_of_ada/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; ------ diff --git a/courses/fundamentals_of_ada/270_introduction_to_contracts/02-preconditions_and_postconditions.rst b/courses/fundamentals_of_ada/270_introduction_to_contracts/02-preconditions_and_postconditions.rst index 31f5c1507..d271b5bc5 100644 --- a/courses/fundamentals_of_ada/270_introduction_to_contracts/02-preconditions_and_postconditions.rst +++ b/courses/fundamentals_of_ada/270_introduction_to_contracts/02-preconditions_and_postconditions.rst @@ -147,10 +147,10 @@ Function Postcondition :ada:`'Result` Attribute * :ada:`function` result can be manipulated with :ada:`'Result` .. 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); ------------------------------------------ @@ -172,16 +172,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 @@ -194,7 +194,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. @@ -242,13 +242,13 @@ 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 Get_Validated_Value return Integer + with Post => Get_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)); [...] @@ -280,12 +280,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 diff --git a/courses/fundamentals_of_ada/270_introduction_to_contracts/03-type_invariants.rst b/courses/fundamentals_of_ada/270_introduction_to_contracts/03-type_invariants.rst index 0e84fc0b4..c86222d28 100644 --- a/courses/fundamentals_of_ada/270_introduction_to_contracts/03-type_invariants.rst +++ b/courses/fundamentals_of_ada/270_introduction_to_contracts/03-type_invariants.rst @@ -127,35 +127,35 @@ 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 (X : 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 (I : 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 (X : Counter_T) + return Counter_T is + Z : Counter_T := X + 1; begin return Z; - end Local_Do_Something; - procedure Do_Something (X : in out Some_T) is + end Increment_Helper; + procedure Increment (X : in out Counter_T) is begin X := X + 1; - X := Local_Do_Something (X); - end Do_Something; - function Counter (I : Integer) + X := Increment_Helper (X); + end Increment; + function Is_Valid (I : 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 +165,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 diff --git a/courses/fundamentals_of_ada/270_introduction_to_contracts/04-subtype_predicates.rst b/courses/fundamentals_of_ada/270_introduction_to_contracts/04-subtype_predicates.rst index 390f91961..26afde12f 100644 --- a/courses/fundamentals_of_ada/270_introduction_to_contracts/04-subtype_predicates.rst +++ b/courses/fundamentals_of_ada/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 @@ -180,7 +180,7 @@ Beware Accidental Recursion in Predicate type Sorted_Table is array (1 .. N) 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 @@ -188,18 +188,18 @@ 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 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 .. N) 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 From 98932497d606483a75e4bcef15df06feb2ff7e28 Mon Sep 17 00:00:00 2001 From: dana Date: Thu, 2 Jan 2025 14:59:57 -0500 Subject: [PATCH 2/6] Minor name fix --- .../02-preconditions_and_postconditions.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/courses/fundamentals_of_ada/270_introduction_to_contracts/02-preconditions_and_postconditions.rst b/courses/fundamentals_of_ada/270_introduction_to_contracts/02-preconditions_and_postconditions.rst index d271b5bc5..df79b8d09 100644 --- a/courses/fundamentals_of_ada/270_introduction_to_contracts/02-preconditions_and_postconditions.rst +++ b/courses/fundamentals_of_ada/270_introduction_to_contracts/02-preconditions_and_postconditions.rst @@ -242,8 +242,8 @@ Separations of Concerns .. code:: Ada - function Get_Validated_Value return Integer - with Post => Get_Validated_Value'Result /= 0 + function Validated_Value return Integer + with Post => Validated_Value'Result /= 0 is (if Raw_Value > 0 then Raw_Value else 1); procedure Process (Input_Value : Integer) @@ -252,7 +252,7 @@ Separations of Concerns [...] - Process (Val); + Process (Validated_Value); * Review of interface: guaranteed to work From 693192bf93b9f399e84a5597e03a09f7c3edd529 Mon Sep 17 00:00:00 2001 From: Dana Binkley Date: Wed, 6 Aug 2025 17:04:43 -0400 Subject: [PATCH 3/6] [!] Fix per comment on MR --- .../02-preconditions_and_postconditions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/courses/ada_essentials/270_introduction_to_contracts/02-preconditions_and_postconditions.rst b/courses/ada_essentials/270_introduction_to_contracts/02-preconditions_and_postconditions.rst index afe640d68..421a93874 100644 --- a/courses/ada_essentials/270_introduction_to_contracts/02-preconditions_and_postconditions.rst +++ b/courses/ada_essentials/270_introduction_to_contracts/02-preconditions_and_postconditions.rst @@ -243,7 +243,7 @@ Separations of Concerns .. code:: Ada - function Validated_Value return Integer + function Validated_Value (Raw_Value : Integer) return Integer with Post => Validated_Value'Result /= 0 is (if Raw_Value > 0 then Raw_Value else 1); From 753e49cbb7649557aed73a4184084e4082c7dd07 Mon Sep 17 00:00:00 2001 From: Dana Binkley Date: Wed, 6 Aug 2025 17:09:20 -0400 Subject: [PATCH 4/6] [+] Adding robust names, hopefully for clarity (?) --- .../03-type_invariants.rst | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/courses/ada_essentials/270_introduction_to_contracts/03-type_invariants.rst b/courses/ada_essentials/270_introduction_to_contracts/03-type_invariants.rst index 26e31b092..22f05d1f5 100644 --- a/courses/ada_essentials/270_introduction_to_contracts/03-type_invariants.rst +++ b/courses/ada_essentials/270_introduction_to_contracts/03-type_invariants.rst @@ -129,26 +129,26 @@ Quiz package Counter_System is type Counter_T is private; - procedure Increment (X : in out Counter_T); + procedure Increment (Val_To_Inc : in out Counter_T); private - function Is_Valid (I : Integer) return Boolean; + 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 (X : Counter_T) + function Increment_Helper (Helper_Num : Counter_T) return Counter_T is - Z : Counter_T := X + 1; + New_Val : Counter_T := Helper_Num + 1; begin - return Z; + return New_Val; end Increment_Helper; - procedure Increment (X : in out Counter_T) is + procedure Increment (Val_To_Inc : in out Counter_T) is begin - X := X + 1; - X := Increment_Helper (X); + Val_To_Inc := Val_To_Inc + 1; + Val_To_Inc := Increment_Helper (Val_To_Inc); end Increment; - function Is_Valid (I : Integer) + function Is_Valid (Val_To_Check : Integer) return Boolean is (True); end Counter_System; From 967ed29d52267f7d2fc2cc08502cfec8addd1fca Mon Sep 17 00:00:00 2001 From: Dana Binkley Date: Wed, 6 Aug 2025 17:10:26 -0400 Subject: [PATCH 5/6] [!] Changing to align with review comments --- .../270_introduction_to_contracts/04-subtype_predicates.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/courses/ada_essentials/270_introduction_to_contracts/04-subtype_predicates.rst b/courses/ada_essentials/270_introduction_to_contracts/04-subtype_predicates.rst index 26afde12f..cb28001d6 100644 --- a/courses/ada_essentials/270_introduction_to_contracts/04-subtype_predicates.rst +++ b/courses/ada_essentials/270_introduction_to_contracts/04-subtype_predicates.rst @@ -177,7 +177,7 @@ 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 (A_Table : Sorted_Table) return Boolean; @@ -186,7 +186,7 @@ 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 => (for all Rows in Sorted_Table'Range => (Row = Sorted_Table'First @@ -196,7 +196,7 @@ Beware Accidental Recursion in Predicate .. code:: Ada - type Table_Type is array (1 .. N) of Integer; + type Table_Type is array (1 .. Max_Size) of Integer; subtype Sorted_Table is Table_Type with Dynamic_Predicate => Sorted (Sorted_Table); function Sorted (A_Table : Table_Type) return Boolean; From 01bf6e415212a519f609a3b331024a03b2bc591e Mon Sep 17 00:00:00 2001 From: Dana Binkley Date: Wed, 6 Aug 2025 17:37:03 -0400 Subject: [PATCH 6/6] [!] Trying to fit text on the page --- .../270_introduction_to_contracts/03-type_invariants.rst | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/courses/ada_essentials/270_introduction_to_contracts/03-type_invariants.rst b/courses/ada_essentials/270_introduction_to_contracts/03-type_invariants.rst index 22f05d1f5..76b532099 100644 --- a/courses/ada_essentials/270_introduction_to_contracts/03-type_invariants.rst +++ b/courses/ada_essentials/270_introduction_to_contracts/03-type_invariants.rst @@ -129,9 +129,11 @@ Quiz package Counter_System is type Counter_T is private; - procedure Increment (Val_To_Inc : in out Counter_T); + procedure Increment (Val_To_Inc : + in out Counter_T); private - function Is_Valid (Val_To_Check : Integer) return Boolean; + 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; @@ -143,7 +145,8 @@ Quiz begin return New_Val; end Increment_Helper; - procedure Increment (Val_To_Inc : in out Counter_T) is + procedure Increment (Val_To_Inc : + in out Counter_T) is begin Val_To_Inc := Val_To_Inc + 1; Val_To_Inc := Increment_Helper (Val_To_Inc);