From 9b6e337ea2b9083575cc49cf47151ad473cd0421 Mon Sep 17 00:00:00 2001 From: dana Date: Fri, 20 Dec 2024 16:50:54 -0500 Subject: [PATCH 1/3] Renaming single char vars where it makes sense to do so --- .../02-preconditions_and_postconditions.rst | 44 +++++++++---------- .../04-in_practice.rst | 44 +++++++++---------- 2 files changed, 44 insertions(+), 44 deletions(-) diff --git a/courses/fundamentals_of_ada/273_subprogram_contracts/02-preconditions_and_postconditions.rst b/courses/fundamentals_of_ada/273_subprogram_contracts/02-preconditions_and_postconditions.rst index f48efd358..533ebc271 100644 --- a/courses/fundamentals_of_ada/273_subprogram_contracts/02-preconditions_and_postconditions.rst +++ b/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 + procedure Print_Something is I : Integer := From_String (""); 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,16 +226,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` - 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 @@ -243,8 +243,8 @@ all values :ada:`L` and :ada:`H` 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` diff --git a/courses/fundamentals_of_ada/273_subprogram_contracts/04-in_practice.rst b/courses/fundamentals_of_ada/273_subprogram_contracts/04-in_practice.rst index af6bbfa37..0fcd96529 100644 --- a/courses/fundamentals_of_ada/273_subprogram_contracts/04-in_practice.rst +++ b/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 (Num_1, Num_2 : Natural) return Integer with - Post => Is_GCD (A, - B, + Post => Is_GCD (Num_1, + Num_2, Greatest_Common_Denominator'Result); - function Is_GCD (A, B, Candidate : Integer) + function Is_GCD (Num_1, Num_2, 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) + (Num_1 rem Candidate = 0 and + Num_2 rem Candidate = 0 and + (for all K in 1 .. Integer'Min (Num_1,Num_2) => + (if (Num_1 rem K = 0 and Num_2 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? From 825b3473e60ddf95ab23d900bf7a08ebadb1d9fa Mon Sep 17 00:00:00 2001 From: dana Date: Fri, 20 Dec 2024 17:10:54 -0500 Subject: [PATCH 2/3] Correcting text that was clipped from edge of slide --- .../273_subprogram_contracts/04-in_practice.rst | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/courses/fundamentals_of_ada/273_subprogram_contracts/04-in_practice.rst b/courses/fundamentals_of_ada/273_subprogram_contracts/04-in_practice.rst index 0fcd96529..93ac5cc88 100644 --- a/courses/fundamentals_of_ada/273_subprogram_contracts/04-in_practice.rst +++ b/courses/fundamentals_of_ada/273_subprogram_contracts/04-in_practice.rst @@ -92,18 +92,18 @@ Postcondition Compared to Their Body: Example .. code:: Ada - function Greatest_Common_Denominator (Num_1, Num_2 : Natural) + function Greatest_Common_Denominator (Num1, Num2 : Natural) return Integer with - Post => Is_GCD (Num_1, - Num_2, + Post => Is_GCD (Num1, + Num2, Greatest_Common_Denominator'Result); - function Is_GCD (Num_1, Num_2, Candidate : Integer) + function Is_GCD (Num1, Num2, Candidate : Integer) return Boolean is - (Num_1 rem Candidate = 0 and - Num_2 rem Candidate = 0 and - (for all K in 1 .. Integer'Min (Num_1,Num_2) => - (if (Num_1 rem K = 0 and Num_2 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))); ---------------------- From ef3b4e4544c40767097aeebc8e923c15ade93a67 Mon Sep 17 00:00:00 2001 From: Dana Binkley Date: Thu, 2 Jan 2025 14:45:30 +0000 Subject: [PATCH 3/3] Apply 1 suggestion(s) to 1 file(s) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Léo Germond --- .../02-preconditions_and_postconditions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/courses/fundamentals_of_ada/273_subprogram_contracts/02-preconditions_and_postconditions.rst b/courses/fundamentals_of_ada/273_subprogram_contracts/02-preconditions_and_postconditions.rst index 533ebc271..8f860bce5 100644 --- a/courses/fundamentals_of_ada/273_subprogram_contracts/02-preconditions_and_postconditions.rst +++ b/courses/fundamentals_of_ada/273_subprogram_contracts/02-preconditions_and_postconditions.rst @@ -200,7 +200,7 @@ Quiz with Pre => S'Length > 0; procedure Print_Something is - I : Integer := From_String (""); + I : Integer := To_Integer (""); begin Put_Line (I'Image); end Print_Something;