Typos in ACSL + Kernel

html/acsl.html

@@ -33,7 +33,7 @@ ACSL is a <em>formal</em> language.</p>
 
   assigns  a[0..n-1];
 
-  ensures<sidenote>As a formal language, ACSL enables a precise specification of function contracts. That makes the specification not only understandable by a human, but also manipulable by an analyzer. Furthermore, as a complete specification is not always useful, the contract can be partial, it depends on one wants to verify.</sidenote><point></point>
+  ensures<sidenote>As a formal language, ACSL enables a precise specification of function contracts. That makes the specification not only understandable by a human, but also manipulable by an analyzer. Furthermore, as a complete specification is not always useful, the contract can be partial, it depends on what one wants to verify.</sidenote><point></point>
   \forall integer i;
     0 <= i < n ==> a[i] == 0;
 */
@@ -58,13 +58,13 @@ void set_to_0(int* a, int n){
 <a href="../fc-plugins/jessie.html">Jessie</a>
 plug-ins use Hoare-style weakest precondition computations to
 formally prove ACSL properties. The process can be quite automatic,
-thanks to external theorem provers such as Alt-Ergo, Z3 or CVC4
+thanks to external theorem provers such as Alt-Ergo, Z3 or CVC4,
 or more interactive, with WP's built-in interactive prover
-or the use of the Coq proof-assistant. Other
+or the use of the Coq proof assistant. Other
 plug-ins, such as the <a href="../fc-plugins/eva.html">Eva</a>
 plug-in, may
 also contribute to the verification of ACSL properties. They may
-also report static analysis results in terms of asserted new ACSL
+also report static analysis results in terms of new asserted ACSL
 properties inside the source code.</p>
 
 <h2>More information</h2>

html/kernel.html

@@ -5,10 +5,10 @@ title: Kernel & Plugins - Frama-C
 active: 2
 ---
 
-<p>The Frama-C platform allows checking security, verifying requirement and
+<p>The Frama-C platform allows checking security, verifying requirements and
   guaranteeing trust in C programs, thanks to a collection of collaborative
   <a href="/html/kernel-plugin.html">plugins</a> that
-  perform static analysis, deductive verification, and testing, for safety- and
+  perform static and dynamic analysis, for safety- and
   security-critical software. Collaborative verification across cooperating
   plug-ins is enabled by their integration on top of a shared kernel and
   datastructures, and their compliance to
@@ -49,9 +49,9 @@ active: 2
   notion of project. A project consistently stores a program with all its
   required information, including results computed by analyzers and their
   parameters. Several projects may coexist in memory at the same time. The
-  projects are partitionned so that a modification on a particular projet does
-  not impact the other ones. The project mechanism may also be used for example
-  to perform different code transformation on the same original project, or to
+  projects are partitioned so that a modification on a particular projet does
+  not impact the others. The project mechanism may also be used for example
+  to perform different code transformations on the same original project, or to
   execute a particular analysis on the same project but with different
   parameters.
 </p>
@@ -73,7 +73,7 @@ active: 2
   the correctness of the entire verification process.
 </p>
 <p>The main correctness property of the Frama-C kernel can be stated as:
-  “if the consolidated status of a property is computed as valid [resp. invalid]
+  "if the consolidated status of a property is computed as valid [resp. invalid]
   by the kernel, then the property is valid [resp. invalid] with respect to ACSL
-  semantics”.
+  semantics".
 </p>