Fix typos

Co-authored-by: Allan Blanchard <allan.blanchard0@gmail.com>

Author: AllanBlanchard

english/function-contract/contract.tex

@@ -652,11 +652,11 @@
 types, the logic type is \CodeInline{integer}, for C floating point types, the
 logic type is \CodeInline{real} (structures are kept as are until one really
 tries to compute something with its field and this case, the value of the field
-itself is promoted). When one tries to add an \CodeInline{integer} and a
+itself is promoted). When one tries to sum an \CodeInline{integer} and a
 \CodeInline{real}, the \CodeInline{integer} is promoted to a \CodeInline{real}.
 
 
-Thus, here even if \CodeInline{x+y} might overflow, we can safely compare the
+Thus, here, even if \CodeInline{x+y} might overflow, we can safely compare the
 resulting value to \CodeInline{INT\_MIN} and \CodeInline{INT\_MAX}. Note that
 it also means that for C types that have defined overflow, the behavior is the
 one from ACSL. For example:
@@ -680,7 +680,7 @@
 \image{addition-unsigned-fixed}
 
 
-However, there are still operations that may be undefined, for example, if one
+However, there are still operations that may be undefined. For example, if one
 writes the following ACSL properties, there are divisions by 0:
 
 
@@ -692,7 +692,7 @@
 
 Nevertheless, those annotations are well-defined in ACSL. Even if we are not
 able to \textit{compute} the values of these divisions, it is correct to write
-these assertions, the first one evaluates to true, the second is unknown: in the
+these assertions. The first one evaluates to true, the second is unknown: in the
 first assertion, even if we cannot compute the terms, they are indeed the same,
 thus equal ; in the second, we cannot say if they equal because even if they are
 different, nothing tells us what is the value that would eventually be

french/function-contract/contract.tex

@@ -682,7 +682,7 @@
 
 Nous voyons que l'expression qui peut provoquer un comportement indéterminé en
 C peut être utilisée de manière sure en ACSL. La raison de cela est que les
-valeurs C sont automatiquement promue vers de types logiques avant de faire des
+valeurs C sont automatiquement promues vers des types logiques avant de faire des
 calculs. Pour les entiers C, le type logique est \CodeInline{integer}, pour les
 valeurs flottantes, le type logique est \CodeInline{real} (les structures sont
 conservées telles quelles jusqu'à ce qu'un champ en particulier soit utilisé
@@ -716,7 +716,7 @@
 \image{addition-unsigned-fixed}
 
 
-Cependant, il reste d'autres opérations qui peuvent être indéfinie, par exemple,
+Cependant, il reste d'autres opérations qui peuvent être indéfinies, par exemple,
 si nous écrivons les propriétés ACSL suivante, il y a des divisions par 0 :
 
 
@@ -728,7 +728,7 @@
 
 Néanmoins, ces annotations sont parfaitement définies en ACSL. Même si nous ne
 sommes pas capables de \textit{calculer} les valeurs de ces divisions, il est
-correct d'écrire ces assertions, la première s'évalue à vrai, la seconde est
+correct d'écrire ces assertions. La première s'évalue à vrai, la seconde est
 inconnue : dans la première assertion, même, si nous ne pouvons pas calculer
 les termes, ils sont effectivement les mêmes, et donc égaux ; dans la seconde,
 nous ne pouvons pas dire s'ils sont égaux parce que même s'ils sont différents,