diff --git a/content/courses/intro-to-spark/chapters/03_Proof_Of_Program_Integrity.rst b/content/courses/intro-to-spark/chapters/03_Proof_Of_Program_Integrity.rst index c202e2a22..aab52045e 100644 --- a/content/courses/intro-to-spark/chapters/03_Proof_Of_Program_Integrity.rst +++ b/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, diff --git a/content/courses/intro-to-spark/chapters/04_State_Abstraction.rst b/content/courses/intro-to-spark/chapters/04_State_Abstraction.rst index ae620de78..42f02521b 100644 --- a/content/courses/intro-to-spark/chapters/04_State_Abstraction.rst +++ b/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 diff --git a/content/courses/intro-to-spark/chapters/05_Proof_Of_Functional_Correctness.rst b/content/courses/intro-to-spark/chapters/05_Proof_Of_Functional_Correctness.rst index b35a813f3..7225e6a92 100644 --- a/content/courses/intro-to-spark/chapters/05_Proof_Of_Functional_Correctness.rst +++ b/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.