@@ -528,35 +528,48 @@ Quiz
528528
529529.. code :: Ada
530530
531- type Index_T is range 1 .. 100;
532- -- Database initialized such that value for element at I = I
533- Database : array (Index_T) of Integer;
534- -- Set the value for element Index to Value and
535- -- then increment Index by 1
536- function Set_And_Move (Value : Integer;
531+ Database : String (1 .. 10) := "ABCDEFGHIJ";
532+ -- Set the value for the element at position Index in
533+ -- array Database to Value and then increment Index by 1
534+ function Set_And_Move (Value : Character;
537535 Index : in out Index_T)
538536 return Boolean
539537 with Post => ...
540538
541539 Given the following expressions, what is their value if they are evaluated in the postcondition
542- of the call :ada: `Set_And_Move (-1, 10) `
540+ of the call :ada: `Set_And_Move ('X', 4) `?
543541
544- .. list-table ::
542+ .. container :: animate 2-
543+
544+ .. image :: subprogram_contracts_special_attributes-legend.svg
545+ :width: 60%
546+
547+ .. container :: animate 1-
548+
549+ * ``Database'Old (Index) ``
550+
551+ .. container :: animate 2-
552+
553+ .. image :: subprogram_contracts_special_attributes-answer1.svg
554+ :width: 60%
555+
556+ .. container :: animate 1-
557+
558+ * ``Database (Index'Old) ``
545559
546- * - `` Database'Old (Index) ``
560+ .. container :: animate 3-
547561
548- - :animate: ` 11 `
549- - :animate: ` Use new index in copy of original Database `
562+ .. image :: subprogram_contracts_special_attributes-answer2.svg
563+ :width: 60 %
550564
551- * - `` Database (Index'Old) ``
565+ .. container :: animate 1-
552566
553- - :animate: `-1 `
554- - :animate: `Use copy of original index in current Database `
567+ * ``Database (Index)'Old ``
555568
556- * - `` Database (Index)'Old ``
569+ .. container :: animate 4-
557570
558- - :animate: ` 10 `
559- - :animate: ` Evaluation of Database (Index) before call `
571+ .. image :: subprogram_contracts_special_attributes-answer3.svg
572+ :width: 60 %
560573
561574-------------------------------------
562575Stack Example (Spec with Contracts)
0 commit comments