Minor fixes and suggestions for Intro to SPARK course

content/courses/intro-to-spark/chapters/03_Proof_Of_Program_Integrity.rst

@@ -10,7 +10,7 @@ performing proof of your program's integrity is to ensure the absence of
 runtime errors during its execution.
 
 The analysis steps discussed here are only sound if you've previously
-performed :ref:`Flow_Analysis`.  You shouldn't proceed further if there you
+performed :ref:`Flow_Analysis`.  You shouldn't proceed further if you
 still have unjustified flow analysis messages for your program.
 
 
@@ -317,7 +317,7 @@ testing easier.  Early failure detection also allows an easier recovery and
 facilitates debugging, so you may want to enable these checks at runtime to
 terminate execution before some damaging or hard-to-debug action occurs.
 
-GNATprove statically analyses preconditions and postcondition. It verifies
+GNATprove statically analyses preconditions and postconditions. It verifies
 preconditions every time a subprogram is called, which is the runtime
 semantics of contracts.  Postconditions, on the other hand, are verified
 once as part of the verification of the subprogram's body. For example,

content/courses/intro-to-spark/chapters/04_State_Abstraction.rst

@@ -615,7 +615,7 @@ contracts when their implementation is visible.
 You may often need a more constraining contract to verify the package's
 implementation but want to be less strict outside the abstraction.  You do
 this using the :ada:`Refined_Post` aspect. This aspect, when placed on a
-subprogram's body, provides stronger guaranties to internal callers of a
+subprogram's body, provides stronger guarantees to internal callers of a
 subprogram. If you provide one, the refined postcondition must imply the
 subprogram's postcondition. This is checked by GNATprove, which reports a
 failing postcondition if the refined postcondition is too weak, even if
@@ -681,6 +681,13 @@ As part of flow analysis, GNATprove checks for the proper initialization of
 variables. Therefore, flow analysis needs to know which variables are
 initialized during the package's elaboration.
 
+.. todo::
+
+   What is the target audience of this book? If its people who have no
+   Ada experience then they likely have no idea what elaboration is.
+   One option is to add the prerequisite knowledge for this book in the intro,
+   and link to the Introduction to Ada (which also does not discuss elaboration).
+
 You can use the :ada:`Initializes` aspect to specify the set of visible
 variables and state abstractions that are initialized during the
 elaboration of a package.  An :ada:`Initializes` aspect can't refer to a
@@ -911,8 +918,8 @@ This program doesn't read any uninitialized data, but GNATprove fails to
 verify that. This is because we provided a state abstraction for package
 :ada:`Counting`, so flow analysis computes the effects of subprograms in terms
 of this state abstraction and thus considers :ada:`State` to be an in-out
-global consisting of both :ada:`Reset_Black_Counter` and
-:ada:`Reset_Red_Counter`. So it issues the message requiring that :ada:`State` be
+global consisting of both :ada:`Black_Counter` and
+:ada:`Red_Counter`. So it issues the message requiring that :ada:`State` be
 initialized after elaboration as well as the warning that no procedure in
 package :ada:`Counting` can initialize its state.
 
@@ -1268,9 +1275,9 @@ body) from an external interface that reads the file system.
        end;
     end Data;
 
-This example isn't correct. The dependency between :ada:`Data_1`'s initial
-value and :ada:`File_System` must be listed in :ada:`Data`'s :ada:`Initializes`
-aspect.
+This example isn't correct. The dependency between :ada:`Data_1`'s, :ada:`Data_2`'s, and
+:ada:`Data_3`'s initial values and :ada:`File_System` must be listed in
+:ada:`Data`'s :ada:`Initializes` aspect.
 
 
 Example #10

content/courses/intro-to-spark/chapters/05_Proof_Of_Functional_Correctness.rst

@@ -542,6 +542,11 @@ the proof or strip it down to a small number of easily-reviewable
 assumptions. For this purpose, you can add assertions to break complex
 proofs into smaller steps.
 
+.. todo::
+
+    This might confuse people, what is the difference between the
+    first two assertions provided here?
+
 .. code-block:: ada
 
     pragma Assert (Assertion_Checked_By_The_Tool);
@@ -644,10 +649,19 @@ property.
 Ghost Procedures
 ~~~~~~~~~~~~~~~~
 
+.. todo::
+
+    This section still seems very abstract. Can a more concrete example be developed?
+
 Ghost procedures can't affect the value of normal variables, so they're
 mostly used to perform operations on ghost variables or to group together a
 set of intermediate assertions.
 
+.. todo::
+
+    Hard to understand what this first sentence is trying to express;
+    specifically the word "treatment".
+
 Abstracting away the treatment of assertions and ghost variables inside a
 ghost procedure has several advantages. First, you're allowed to use these
 variables in any way you choose in code inside ghost procedures.  This
@@ -687,6 +701,10 @@ isn't part of the functional behavior of the subprogram. Finally, it can
 help GNATprove by abstracting away assertions that would otherwise make its
 job more complex.
 
+.. todo::
+
+    What is a Proof Context? I don't think this is defined anywhere.
+
 In the example below, calling :ada:`Prove_P` with :ada:`X` as an operand only
 adds :ada:`P (X)` to the proof context instead of the larger set of assertions
 required to verify it. In addition, the proof of :ada:`P` need only be done
@@ -707,7 +725,7 @@ Handling of Loops
 
 When the program involves a loop, you're almost always required to provide
 additional annotations to allow GNATprove to complete a proof because the
-verification techniques used by GNATprove doesn't handle cycles in a
+verification techniques used by GNATprove don't handle cycles in a
 subprogram's control flow. Instead, loops are flattened by dividing them
 into several acyclic parts.
 
@@ -1036,6 +1054,10 @@ index :ada:`K` is stored at index :ada:`K-1`:
 
     end Show_Map;
 
+.. todo::
+
+    Uncommenting the code did not result in successful analysis.
+
 You need to uncomment the second loop invariant containing the frame condition
 in order to prove the assertion after the loop.