Address Claire's comments

courses/intro-to-spark/book/01_Overview.rst

@@ -85,7 +85,7 @@ environment <https://www.adacore.com/gnatpro/toolsuite/gps>`_.
 A trivial example
 ---------------------------------------------------------------------
 
-We will now look at a simple example of subprogram in Ada that has also used
+We will now look at a simple example of subprogram in Ada that also uses
 SPARK aspects to specify a verifiable subprogram contract. The subprogram
 called ``Increment`` adds 1 to the value of its parameter ``X``:
 
@@ -106,15 +106,15 @@ called ``Increment`` adds 1 to the value of its parameter ``X``:
      X := X + 1;
    end Increment;
 
-Several properties can be specified on this subprogram using the contracts
+Several properties are specified on this subprogram using the contracts
 shown:
 
 - The SPARK Global aspect specifies that ``Increment`` does not read
   and does not write any global variable.
 
-- The SPARK Depend aspect is especially interesting for the security of this
-  subprogram, as it specifies that the value of the parameter ``X`` after the
-  call only depends on the value of ``X`` before the call.
+- The SPARK Depend aspect is especially interesting for security, as it
+  specifies that the value of the parameter ``X`` after the call only depends
+  on the value of ``X`` before the call.
 
 - Functional properties of Increment are specified using the :ada:`Pre` and
   :ada:`Post` aspects of Ada.
@@ -140,7 +140,7 @@ between the SPARK and Ada languages. The aim while designing the SPARK
 subset of Ada was to create the biggest possible subset still amenable to
 easy specification and sound verification.
 
-The most notable exclusions include access type and allocators, as well as
+The most notable exclusions include access types and allocators, as well as
 handling of exceptions, which are both known to increase considerably the
 amount of required user-written annotations. Goto statements and
 controlled types are also not supported as they introduce non-trivial
@@ -251,24 +251,11 @@ while ``Incr_And_Log`` is not as it attempts to update the global variable
 
     end Side_Effects;
 
-However, ``Incr`` is valid SPARK while ``Incr_And_Log`` is not as it
-attempts to update the global variable ``Call_Count``.
-
 No aliasing of names
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Another restriction imposed in the SPARK subset concerns aliasing. We say that
-two names are aliased if they refer to the same object. Since access types
-(`pointers <https://en.m.wikipedia.org/wiki/Pointer_(computer_programming)>`_
-in Ada) are not allowed in SPARK, aliasing can only occur as part of the
-parameter passing in a subprogram call. As functions have no side-effects in
-SPARK, aliasing of parameters in function calls is not problematic, so we only
-need to consider procedure calls. When a procedure is called, SPARK makes sure
-that no :ada:`out` or :ada:`in out` parameter is aliased with either another
-parameter of the procedure or a global variable updated in the procedure's
-body.
-
-There are two reasons to forbid aliasing in SPARK:
+Another restriction imposed in the SPARK subset concerns aliasing. There are
+two reasons to forbid aliasing in SPARK:
 
 - First, it makes verification more difficult as it requires taking into
   account the fact that updates to two variables with different names may in
@@ -278,8 +265,18 @@ There are two reasons to forbid aliasing in SPARK:
   parameters are aliased, the results of a subprogram call may depend on
   compiler specific treatment, like parameter passing mechanisms.
 
-What is more, most of the time, possibility of aliasing was not even taken
-into account by the programmer. For example:
+We say that two names are aliased if they refer to the same object. Since
+access types (`pointers
+<https://en.m.wikipedia.org/wiki/Pointer_(computer_programming)>`_ in Ada) are
+not allowed in SPARK, aliasing can only occur as part of the parameter passing
+in a subprogram call. As functions have no side-effects in SPARK, aliasing of
+parameters in function calls is not problematic, so we only need to consider
+procedure calls. When a procedure is called, SPARK makes sure that no
+:ada:`out` or :ada:`in out` parameter is aliased with either another parameter
+of the procedure or a global variable updated in the procedure's body.
+
+Procedure ``Move_To_Total`` shows an example where the possibility of aliasing
+was not taken into account by the programmer:
 
 .. code:: ada run_button spark-flow
     :class: ada-run-expect-failure
@@ -316,8 +313,10 @@ check for non-aliasing on every call to ``Move_To_Total``. The final call to
 ``Move_To_Total`` in procedure ``No_Aliasing`` violates this property, which
 leads to both a message from GNATprove and a runtime error (assertion violation
 corresponding to the expected increase in ``Total`` from calling
-``Move_To_Total``) when compiling and running.
-
+``Move_To_Total``) when compiling and running. Note that the postcondition of
+``Move_To_Total`` is not violated on this second call, as integer parameters
+are passes by copy, and the postcondition is checked here before the copy-back
+from formal parameters to actual arguments.
 
 Identifying SPARK Code
 ---------------------------------------------------------------------

courses/intro-to-spark/book/02_Flow_Analysis.rst

@@ -297,7 +297,7 @@ the initial value of the other parameter. If the subprogram is a function,
 its result must be listed as an output, as we did for ``Get_Value_Of_X``
 using the :ada:`Result` attribute.
 
-.. code:: ada
+.. code:: ada spark-flow
 
     package Show_Depends_Contracts is
 
@@ -343,7 +343,7 @@ on each other.
 It can also be the case that an input is not used to compute the final
 value of any output. This can be expressed by putting :ada:`null` at the
 left of the dependency relation, like we have for the ``Do_Nothing``
-subprogram shown here. Note that there can only be one such dependency
+subprogram shown above. Note that there can only be one such dependency
 relation, listing all the unused inputs of the subprogram, and that it
 must be declared last. Also note that such an annotation will silence flow
 analysis' warning about unused parameters. Finally, :ada:`null` can also

courses/intro-to-spark/book/04_State_Abstraction.rst

@@ -167,12 +167,12 @@ cannot be used inside expressions. For example:
 Refining an Abstract State
 ---------------------------------------------------------------------
 
-Once an abstract state has been declared in a package, it must be refined
-into its constituents using a :ada:`Refined_State` aspect. The
-:ada:`Refined_State` aspect must be placed on the package's body even if
-the package previously did not require a body. For each state abstraction
-declared for the package, the refined state lists the set of variables
-which are represented by this state abstraction.
+Once an abstract state has been declared in a package, it must be refined into
+its constituents using a :ada:`Refined_State` aspect. The :ada:`Refined_State`
+aspect must be placed on the package's body even if the package previously did
+not require a body before the addition of :ada:`Abstract_State`. For each state
+abstraction declared for the package, the refined state lists the set of
+variables which are represented by this state abstraction.
 
 If an abstract state is specified for a package, then it must be complete,
 in the sense that every hidden variable must be part of a state
@@ -976,12 +976,11 @@ providing a procedure ``Reset_All`` calling the initialization procedures
        end Reset_All;
     end Counting;
 
-This example is correct. Flow analysis uses the refined version of
-:ada:`Global` contracts for internal calls and thus can verify that
+This example is correct.  Flow analysis computes refined versions of
+:ada:`Global` contracts for internal calls which are used to verify that
 ``Reset_All`` indeed properly initializes ``State``. Note that
-:ada:`Refined_Global` and :ada:`Global` annotations are not mandatory,
-they can also be computed by the tool.
-
+:ada:`Refined_Global` and :ada:`Global` annotations are not mandatory, they can
+also be computed by the tool.
 
 Example #6
 ~~~~~~~~~~
@@ -1038,11 +1037,11 @@ Example #7
 ~~~~~~~~~~
 
 In this version of our abstract stack unit, a model of the stack is returned by
-function ``Get_Model``, which can be called from the postcondition of ``Push``
+function ``Get_Stack``, which can be called from the postcondition of ``Push``
 to specify that the stack should not be modified if it is full. Then, we can
 assert in ``Use_Stack`` that after pushing an element on the stack, either the
-top of the stack is unchanged (if the stack was full already) or it is equal to
-the element just pushed.
+stack is unchanged (if the stack was full already) or its top element is equal
+to the element just pushed.
 
 .. code:: ada
 

courses/intro-to-spark/book/05_Proof_Of_Functional_Correctness.rst

@@ -485,13 +485,13 @@ write this kind of specification more easily, global ghost variables may be
 used to store intermediate values of variables in the program.
 
 For example, we specify below the subprogram ``Do_Two_Things`` in two steps
-using the global variable ``V_Interm`` to store the intermediate value of
-``V`` between the two things to be done. Note that, conceptually, this
-usage could be expressed using an existential quantification on the
-variable ``V_Interm``. This cannot always be done in SPARK as
-quantification in Ada is restricted to :ada:`for ... loop` patterns. What
-is more, supplying the value of the variable may help the prover to
-effectively verify the contracts.
+using the global variable ``V_Interm`` to store the intermediate value of ``V``
+between the two things to be done. Note that this usage could be expressed
+using an existential quantification on the variable ``V_Interm``, although this
+would be very inefficient at runtime to iterate over all integers. Besides,
+this cannot always be done in SPARK as quantification in Ada is restricted to
+:ada:`for ... loop` patterns. What is more, supplying the value of the variable
+may help the prover to effectively verify the contracts.
 
 .. code:: ada