diff --git a/courses/fundamentals_of_ada/273_subprogram_contracts.rst b/courses/fundamentals_of_ada/273_subprogram_contracts.rst index 7117eb2cf..e42084a36 100644 --- a/courses/fundamentals_of_ada/273_subprogram_contracts.rst +++ b/courses/fundamentals_of_ada/273_subprogram_contracts.rst @@ -528,35 +528,48 @@ Quiz .. code:: Ada - type Index_T is range 1 .. 100; - -- Database initialized such that value for element at I = I - Database : array (Index_T) of Integer; - -- Set the value for element Index to Value and - -- then increment Index by 1 - function Set_And_Move (Value : Integer; + Database : String (1 .. 10) := "ABCDEFGHIJ"; + -- Set the value for the element at position Index in + -- array Database to Value and then increment Index by 1 + function Set_And_Move (Value : Character; Index : in out Index_T) return Boolean with Post => ... Given the following expressions, what is their value if they are evaluated in the postcondition -of the call :ada:`Set_And_Move (-1, 10)` +of the call :ada:`Set_And_Move ('X', 4)`? -.. list-table:: +.. container:: animate 2- + + .. image:: subprogram_contracts_special_attributes-legend.svg + :width: 60% + +.. container:: animate 1- + + * ``Database'Old (Index)`` + +.. container:: animate 2- + + .. image:: subprogram_contracts_special_attributes-answer1.svg + :width: 60% + +.. container:: animate 1- + + * ``Database (Index'Old)`` - * - ``Database'Old (Index)`` +.. container:: animate 3- - - :animate:`11` - - :animate:`Use new index in copy of original Database` + .. image:: subprogram_contracts_special_attributes-answer2.svg + :width: 60% - * - ``Database (Index'Old)`` +.. container:: animate 1- - - :animate:`-1` - - :animate:`Use copy of original index in current Database` + * ``Database (Index)'Old`` - * - ``Database (Index)'Old`` +.. container:: animate 4- - - :animate:`10` - - :animate:`Evaluation of Database (Index) before call` + .. image:: subprogram_contracts_special_attributes-answer3.svg + :width: 60% ------------------------------------- Stack Example (Spec with Contracts) diff --git a/images/subprogram_contracts_special_attributes-answer1.svg b/images/subprogram_contracts_special_attributes-answer1.svg new file mode 100644 index 000000000..fdeb1ffb7 --- /dev/null +++ b/images/subprogram_contracts_special_attributes-answer1.svg @@ -0,0 +1,99 @@ + + + + + + + + + + + + + Database'Old (Index) +Database before the call: ABCDEFGHIJ +Index after the call : 5 +Value : E + + diff --git a/images/subprogram_contracts_special_attributes-answer2.svg b/images/subprogram_contracts_special_attributes-answer2.svg new file mode 100644 index 000000000..db3a3ebb3 --- /dev/null +++ b/images/subprogram_contracts_special_attributes-answer2.svg @@ -0,0 +1,97 @@ + + + + + + + + + + + + + Database (Index'Old) +Database after the call : ABCXEFGHIJ +Index before the call : 4 +Value : X + + diff --git a/images/subprogram_contracts_special_attributes-answer3.svg b/images/subprogram_contracts_special_attributes-answer3.svg new file mode 100644 index 000000000..b68467de7 --- /dev/null +++ b/images/subprogram_contracts_special_attributes-answer3.svg @@ -0,0 +1,95 @@ + + + + + + + + + + + + + Database (Index)'Old +Database before the call: ABCDEFGHIJ +Index before the call : 4 +Value : D + + diff --git a/images/subprogram_contracts_special_attributes-legend.svg b/images/subprogram_contracts_special_attributes-legend.svg new file mode 100644 index 000000000..8e431b615 --- /dev/null +++ b/images/subprogram_contracts_special_attributes-legend.svg @@ -0,0 +1,89 @@ + + + + + + + + + + + + + Legend +Value on call entry +Value on call return + + diff --git a/support_files/beamercolorthemeadacore.sty b/support_files/beamercolorthemeadacore.sty index 8a84c457d..f9cc6408e 100644 --- a/support_files/beamercolorthemeadacore.sty +++ b/support_files/beamercolorthemeadacore.sty @@ -14,6 +14,12 @@ \definecolor{adacore3}{RGB}{185,198,215} %% light blue \definecolor{lightyellow}{RGB}{240,230,160} +% For SVG, we need colors in hex notation, which would be +% lovelace blue #12284c +% orange #e07c00 +% light blue #b9c6d7 +% Note that the light blue doesn't show up well, so I've been using #55ddff + \setbeamercolor*{palette primary}{fg=adacore1,bg=adacore3} \setbeamercolor*{palette secondary}{fg=adacore2,bg=adacore3} \setbeamercolor*{palette tertiary}{fg=adacore3,bg=adacore1}