From c989353d5357cc3f783868b39de42356f3d5d88d Mon Sep 17 00:00:00 2001 From: Filip Gajowniczek Date: Wed, 7 Jul 2021 16:13:04 -0500 Subject: [PATCH 1/8] Minor fix in 02_Flow_analysis.rst --- content/courses/intro-to-spark/chapters/02_Flow_Analysis.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/courses/intro-to-spark/chapters/02_Flow_Analysis.rst b/content/courses/intro-to-spark/chapters/02_Flow_Analysis.rst index 1e3aebfc0..196441762 100644 --- a/content/courses/intro-to-spark/chapters/02_Flow_Analysis.rst +++ b/content/courses/intro-to-spark/chapters/02_Flow_Analysis.rst @@ -666,7 +666,7 @@ initialized on the path that falls through from the loop. Even though this program is correct, you shouldn't ignore the message: it means flow analysis cannot guarantee that :ada:`Result` is always initialized at the call site and so assumes any read of :ada:`Result` at the call site will read -initialized data. Therefore, you should either initialize :ada:`Result` when +uninitialized data. Therefore, you should either initialize :ada:`Result` when :ada:`Found` is false, which silences flow analysis, or verify this assumption at each call site by other means. From 74e08843dd87a233f4fe9cc3db2829adc708b1cd Mon Sep 17 00:00:00 2001 From: gusthoff Date: Fri, 15 Oct 2021 18:38:23 +0200 Subject: [PATCH 2/8] Addressing minor issues in 03_Proof_of_Program_Integrity.rst --- .../intro-to-spark/chapters/03_Proof_Of_Program_Integrity.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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, From 09f511489170eb0e75155740f358139eeba6e45c Mon Sep 17 00:00:00 2001 From: Filip Gajowniczek Date: Thu, 8 Jul 2021 13:02:47 -0500 Subject: [PATCH 3/8] 04_State_Abstraction.rst review --- .../chapters/04_State_Abstraction.rst | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) 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..102947b56 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 @@ -680,6 +680,11 @@ Initialization of Local Variables 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 @@ -911,8 +916,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 +1273,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 From ab4838afc64dc7dcdab7523d83758284edcb466b Mon Sep 17 00:00:00 2001 From: Filip Gajowniczek Date: Thu, 8 Jul 2021 14:55:25 -0500 Subject: [PATCH 4/8] Comments/fixes for 05_Proof_of_Functional_Correctness.rst --- .../05_Proof_Of_Functional_Correctness.rst | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) 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..52ad391f2 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,9 @@ 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); @@ -643,11 +646,16 @@ 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 +695,8 @@ 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 Prrof 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 +717,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 +1046,8 @@ 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. From 4ec2dbfa0970d0f817e1eacdf7b0871889d15759 Mon Sep 17 00:00:00 2001 From: filip-gajowniczek-adacore <75339569+filip-gajowniczek-adacore@users.noreply.github.com> Date: Fri, 9 Jul 2021 16:40:46 -0500 Subject: [PATCH 5/8] Update 04_State_Abstraction.rst Fix formatting of TODOs --- .../intro-to-spark/chapters/04_State_Abstraction.rst | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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 102947b56..42f02521b 100644 --- a/content/courses/intro-to-spark/chapters/04_State_Abstraction.rst +++ b/content/courses/intro-to-spark/chapters/04_State_Abstraction.rst @@ -680,8 +680,10 @@ Initialization of Local Variables 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 + +.. 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). From 57544df4033a56c501e54656f38cc93eb31efa95 Mon Sep 17 00:00:00 2001 From: filip-gajowniczek-adacore <75339569+filip-gajowniczek-adacore@users.noreply.github.com> Date: Fri, 9 Jul 2021 16:42:42 -0500 Subject: [PATCH 6/8] Update 05_Proof_Of_Functional_Correctness.rst Fixed TODO formatting --- .../05_Proof_Of_Functional_Correctness.rst | 33 ++++++++++++------- 1 file changed, 21 insertions(+), 12 deletions(-) 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 52ad391f2..4c99e8e6b 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,9 +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? +.. 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); @@ -646,16 +648,20 @@ property. Ghost Procedures ~~~~~~~~~~~~~~~~ -.. - TODO: This section still seems very abstract. Can a more concrete example be developed? + +.. 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". +.. 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 @@ -695,8 +701,9 @@ 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 Prrof Context? I don't think this is defined anywhere. +.. 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 @@ -1046,8 +1053,10 @@ index :ada:`K` is stored at index :ada:`K-1`: end Show_Map; -.. - TODO: Uncommenting the code did not result in successful analysis. +.. 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. From d9bcc7fccde0cad34662aaa33ce5f9bd23753c8e Mon Sep 17 00:00:00 2001 From: filip-gajowniczek-adacore <75339569+filip-gajowniczek-adacore@users.noreply.github.com> Date: Mon, 12 Jul 2021 12:51:48 -0500 Subject: [PATCH 7/8] Update content/courses/intro-to-spark/chapters/05_Proof_Of_Functional_Correctness.rst Co-authored-by: Gustavo A. Hoffmann --- .../chapters/05_Proof_Of_Functional_Correctness.rst | 1 + 1 file changed, 1 insertion(+) 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 4c99e8e6b..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 @@ -702,6 +702,7 @@ 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 From 3415f792710b0d430d1128cde3241deb53bb99aa Mon Sep 17 00:00:00 2001 From: "Gustavo A. Hoffmann" Date: Fri, 15 Oct 2021 18:31:17 +0200 Subject: [PATCH 8/8] Reverting change --- content/courses/intro-to-spark/chapters/02_Flow_Analysis.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/courses/intro-to-spark/chapters/02_Flow_Analysis.rst b/content/courses/intro-to-spark/chapters/02_Flow_Analysis.rst index 196441762..1e3aebfc0 100644 --- a/content/courses/intro-to-spark/chapters/02_Flow_Analysis.rst +++ b/content/courses/intro-to-spark/chapters/02_Flow_Analysis.rst @@ -666,7 +666,7 @@ initialized on the path that falls through from the loop. Even though this program is correct, you shouldn't ignore the message: it means flow analysis cannot guarantee that :ada:`Result` is always initialized at the call site and so assumes any read of :ada:`Result` at the call site will read -uninitialized data. Therefore, you should either initialize :ada:`Result` when +initialized data. Therefore, you should either initialize :ada:`Result` when :ada:`Found` is false, which silences flow analysis, or verify this assumption at each call site by other means.