Skip to content
Open
25 changes: 7 additions & 18 deletions courses/fundamentals_of_ada/273_subprogram_contracts.rst
Original file line number Diff line number Diff line change
Expand Up @@ -528,35 +528,24 @@ 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;
Database : String (1 .. 10) := "ABCDEFGHIJ";
-- Set the value for element Index to Value and
-- then increment Index by 1
function Set_And_Move (Value : Integer;
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::

* - ``Database'Old (Index)``

- :animate:`11`
- :animate:`Use new index in copy of original Database`

* - ``Database (Index'Old)``
.. container:: overlay 1

- :animate:`-1`
- :animate:`Use copy of original index in current Database`
.. image:: subprogram_contracts_special_attributes-quiz.svg}

* - ``Database (Index)'Old``
.. container:: overlay 2

- :animate:`10`
- :animate:`Evaluation of Database (Index) before call`
.. image:: subprogram_contracts_special_attributes-answer.svg}

-------------------------------------
Stack Example (Spec with Contracts)
Expand Down
216 changes: 216 additions & 0 deletions images/subprogram_contracts_special_attributes-answer.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Loading