Slides/157 break 273 subprogram contracts into chapters

courses/fundamentals_of_ada/273_subprogram_contracts/01-introduction.rst

@@ -0,0 +1,134 @@
+==============
+Introduction
+==============
+
+--------------------------
+:dfn:`Design-By-Contract`
+--------------------------
+
+* Source code acting in roles of **client** and **supplier** under a binding **contract**
+
+   - :dfn:`Contract` specifies *requirements* or *guarantees*
+
+      - *"A specification of a software element that affects its use by potential clients."* (Bertrand Meyer)
+
+   - :dfn:`Supplier` provides services
+
+       - Guarantees specific functional behavior
+       - Has requirements for guarantees to hold
+
+   - :dfn:`Client` utilizes services
+
+       - Guarantees supplier's conditions are met
+       - Requires result to follow the subprogram's guarantees
+
+---------------
+Ada Contracts
+---------------
+
+* Ada contracts include enforcement
+
+   - At compile-time: specific constructs, features, and rules
+   - At run-time: language-defined and user-defined exceptions
+
+* Facilities as part of the language definition
+
+   - Range specifications
+   - Parameter modes
+   - Generic contracts
+   - OOP :ada:`interface` types
+   - Work well, but on a restricted set of use-cases
+
+* Contract aspects to be more expressive
+
+   - Carried by subprograms
+   - ... or by types (seen later)
+   - Can have **arbitrary** conditions, more **versatile**
+
+------------------
+:dfn:`Assertion`
+------------------
+
+* Boolean expression expected to be :ada:`True`
+* Said *to hold* when :ada:`True`
+* Language-defined :ada:`pragma`
+
+.. code:: Ada
+
+   pragma Assert (not Full (Stack));
+   -- stack is not full
+   pragma Assert (Stack_Length = 0,
+                  Message => "stack was not empty");
+   -- stack is empty
+
+* Raises language-defined :ada:`Assertion_Error` exception if expression does not hold
+* The :ada:`Ada.Assertions.Assert` subprogram wraps it
+
+.. code:: Ada
+
+   package Ada.Assertions is
+     Assertion_Error : exception;
+     procedure Assert (Check : in Boolean);
+     procedure Assert (Check : in Boolean; Message : in String);
+   end Ada.Assertions;
+
+------
+Quiz
+------
+
+Which of the following statements is (are) correct?
+
+    A. Contract principles apply only to newer versions of the language
+    B. :answer:`Contract should hold even for unique conditions and corner cases`
+    C. Contract principles were first implemented in Ada
+    D. You cannot be both supplier and client
+
+.. container:: animate
+
+    Explanations
+
+    A. No, but design-by-contract **aspects** were fully integrated into Ada 2012
+    B. Yes, special case should be included in the contract
+    C. No, in eiffel, in 1986!
+    D. No, in fact you are always **both**, even the :ada:`Main` has a caller!
+
+------
+Quiz
+------
+
+Which of the following statements is (are) correct?
+
+    A. :answer:`Assertions can be used in declarations`
+    B. Assertions can be used in expressions
+    C. :answer:`Any corrective action should happen before contract checks`
+    D. Assertions must be checked using :ada:`pragma Assert`
+
+.. container:: animate
+
+    Explanations
+
+    A. Will be checked at elaboration
+    B. No assertion expression, but :ada:`raise` expression exists
+    C. Exceptions as flow-control adds complexity, prefer a proactive :ada:`if` to a (reactive) :ada:`exception` handler
+    D. You can call :ada:`Ada.Assertions.Assert`, or even directly :ada:`raise Assertion_Error`
+
+------
+Quiz
+------
+
+Which of the following statements is (are) correct?
+
+    A. :answer:`Defensive coding is a good practice`
+    B. Contracts can replace all defensive code
+    C. Contracts are executable constructs
+    D. Having exhaustive contracts will prevent run-time errors
+
+.. container:: animate
+
+    Explanations
+
+    A. Principles are sane, contracts extend those
+    B. See previous slide example
+    C. e.g. generic contracts are resolved at compile-time
+    D. A failing contract **will cause** a run-time error, only extensive (dynamic / static) analysis of contracted code may provide confidence in the absence of runtime errors (AoRTE)
+

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

@@ -0,0 +1,250 @@
+===================================
+Preconditions and Postconditions
+===================================
+
+-----------------------------
+Subprogram-based Assertions
+-----------------------------
+
+* **Explicit** part of a subprogram's **specification**
+
+    - Unlike defensive code
+
+* :dfn:`Precondition`
+
+   - Assertion expected to hold **prior to** subprogram call
+
+* :dfn:`Postcondition`
+
+   - Assertion expected to hold **after** subprogram return
+
+* Requirements and guarantees on both supplier and client
+* Syntax uses **aspects**
+
+   .. code:: Ada
+
+      procedure Push (This : in out Stack_T;
+                      Value : Content_T)
+        with Pre  => not Full (This),
+             Post => not Empty (This)
+                     and Top (This) = Value;
+
+---------------------------------
+Requirements / Guarantees: Quiz
+---------------------------------
+
+* Given the following piece of code
+
+    .. code:: Ada
+
+       procedure Start is
+       begin
+           ...
+           Turn_On;
+           ...
+
+       procedure Turn_On
+        with Pre => Has_Power,
+             Post => Is_On;
+
+* Complete the table in terms of requirements and guarantees
+
+.. list-table::
+
+   * - 
+     - Client (:ada:`Start`)
+     - Supplier (:ada:`Turn_On`)
+
+   * - Pre (:ada:`Has_Power`)
+     - :animate:`Requirement`
+     - :animate:`Guarantee`
+
+   * - Post (:ada:`Is_On`)
+     - :animate:`Guarantee`
+     - :animate:`Requirement`
+
+-----------------------
+Defensive Programming
+-----------------------
+
+* Should be replaced by subprogram contracts when possible
+
+.. code:: Ada
+
+   procedure Push (S : Stack) is
+      Entry_Length : constant Positive := Length (S);
+   begin
+      pragma Assert (not Is_Full (S)); -- entry condition
+      [...]
+      pragma Assert (Length (S) = Entry_Length + 1); -- exit condition
+   end Push;
+
+* Subprogram contracts are an **assertion** mechanism
+
+   - **Not** a drop-in replacement for all defensive code
+
+.. code:: Ada
+
+   procedure Force_Acquire (P : Peripheral) is
+   begin
+      if not Available (P) then
+         -- Corrective action
+         Force_Release (P);
+         pragma Assert (Available (P));
+      end if;
+
+      Acquire (P);
+   end;
+
+-----------------------------
+Pre/Postcondition Semantics
+-----------------------------
+
+* Calls inserted automatically by compiler
+
+|
+
+.. image:: pre_and_post_insertion_flow.svg
+   :width: 90%
+
+-------------------------------------
+Contract with Quantified Expression
+-------------------------------------
+
+* Pre- and post-conditions can be **arbitrary** :ada:`Boolean` expressions 
+
+.. code:: Ada
+
+   type Status_Flag is (Power, Locked, Running);
+
+   procedure Clear_All_Status (
+       Unit : in out Controller)
+     -- guarantees no flags remain set after call
+     with Post => (for all Flag in Status_Flag =>
+       not Status_Indicated (Unit, Flag));
+
+   function Status_Indicated (
+       Unit : Controller;
+       Flag : Status_Flag)
+       return Boolean;
+
+-------------------------------------
+Visibility for Subprogram Contracts
+-------------------------------------
+
+* **Any** visible name
+
+   - All of the subprogram's **parameters**
+   - Can refer to functions **not yet specified**
+
+      - Must be declared in same scope
+      - Different elaboration rules for expression functions
+
+  .. code:: Ada
+
+     function Top (This : Stack) return Content
+       with Pre => not Empty (This);
+     function Empty (This : Stack) return Boolean;
+
+* :ada:`Post` has access to special attributes
+
+    - See later
+
+------------------------------------------
+Preconditions and Postconditions Example
+------------------------------------------
+
+* Multiple aspects separated by commas
+
+.. code:: Ada
+
+     procedure Push (This : in out Stack;
+                     Value : Content)
+       with Pre  => not Full (This),
+            Post => not Empty (This) and Top (This) = Value;
+
+------------------------------------
+(Sub)Types Allow Simpler Contracts
+------------------------------------
+
+* Pre-condition
+
+   .. code:: Ada
+
+      procedure Compute_Square_Root (Input : Integer;
+                                     Result : out Natural)
+        with Pre  => Input >= 0,
+             Post => (Result * Result) <= Input and
+                     (Result + 1) * (Result + 1) > Input;
+
+* Subtype
+
+   .. code:: Ada
+
+      procedure Compute_Square_Root (Input  : Natural;
+                                     Result : out Natural)
+         with
+             -- "Pre => Input >= 0" not needed
+             -- (Input can't be < 0)
+             Post => (Result * Result) <= Input and
+                     (Result + 1) * (Result + 1) > Input;
+
+------
+Quiz
+------
+
+.. code:: Ada
+
+   --  Convert string to Integer
+   function From_String ( S : String ) return Integer
+      with Pre => S'Length > 0;
+
+   procedure Do_Something is
+      I : Integer := From_String ("");
+   begin
+      Put_Line (I'Image);
+   end Do_Something;
+
+Assuming :ada:`From_String` is defined somewhere, what happens
+when :ada:`Do_Something` is run?
+
+   A. "0" is printed
+   B. Constraint Error exception
+   C. :answer:`Assertion Error exception`
+   D. Undefined behavior
+
+.. container:: animate
+
+   Explanations
+
+   The call to :ada:`From_String` will fail its precondition, which is considered
+   an :ada:`Assertion_Error` exception.
+
+------
+Quiz
+------
+
+.. code:: Ada
+
+   function Area (L : Positive; H : Positive) return Positive is
+      (L * H)
+   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``
+   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
+   C. Classic trap: the check itself may cause an overflow!
+
+   Preventing an overflow requires using the expression :ada:`Integer'Last / L <= H`
+