diff --git a/content/courses/intro-to-spark/chapters/01_Overview.rst b/content/courses/intro-to-spark/chapters/01_Overview.rst index 23d964371..a1e7f2e58 100644 --- a/content/courses/intro-to-spark/chapters/01_Overview.rst +++ b/content/courses/intro-to-spark/chapters/01_Overview.rst @@ -62,9 +62,10 @@ verification of the source code performed without compiling or executing it. Verification uses tools that perform static analysis. These can take various forms. They include tools that check types and enforce visibility rules, such as the compiler, in addition to those that perform more complex -reasoning, such as abstract interpretation, as done by a tool like -`CodePeer `_ from AdaCore. The tools that -come with SPARK perform two different forms of static analysis: +reasoning, such as abstract interpretation, as done by a tool like the +`GNAT Static Analysis Suite `_ +from AdaCore. The tools that come with SPARK perform two different forms +of static analysis: - `flow analysis` is the fastest form of analysis. It checks initializations of variables and looks at data dependencies between