Fix typos (#23)

Signed-off-by: Samuel Tyler <samuel@samuelt.me>

Author: fosslinux

src/language-top.md

@@ -85,7 +85,7 @@ domain Pair[A, B] {
 * Declared by keyword `domain`
 * Have a name, which is introduced as an additional _type_ in the Viper program
 * Domains may have type parameters (e.g. `A` and `B` above)
-* A domain's body (delimited by braces) consists of a number function declarations, followed by a number of axioms
+* A domain's body (delimited by braces) consists of a number of function declarations, followed by a number of axioms
   * Domain functions (functions declared inside a `domain`) may have neither a body nor a specification; these are uninterpreted total mathematical functions
   * Domain axioms consist of name (following the `axiom` keyword), and a definition enclosed within braces (which is a boolean expression which may not read the program state in any way)
 * Useful for specifying custom mathematical theories
@@ -106,7 +106,7 @@ define link(x, y) {
   * Macros are not type-checked until after expansion
   * However, macro bodies must be well-formed assertions / statements
 * May have any number of (untyped) parameter names (e.g. `a` and `b` above)
-* The are two kinds of macros
+* There are two kinds of macros
   * Macros defining assertions (or expressions) include the macro definition whitespace-separated afterwards (e.g. `plus` above)
   * Macros defining _statements_ include their definitions within braces (e.g. `link` above)
 * See the [array domain encoding](./domains-array.md) for an example

src/termination-measures.md

@@ -27,7 +27,7 @@ Viper successfully verifies that `factorial` terminates: at each recursive invoc
 
 Viper's standard library provides definitions of well-founded orders for most types built into Viper, all of which can be imported from the `decreases` folder. The following table lists all provided orders; we write `s1 <_ s2` if `s1` is less than `s2` with respect to the order.
 
-| Build-In Type<br>(file name) | Provided Well-Founded Order |
+| Built-In Type<br>(file name) | Provided Well-Founded Order |
 | ---- | ---- |
 |`Ref`<br>(`ref.vpr`)| `r1 <_ r2 <==> r1 == null && r2 != null`
 |`Bool`<br>(`bool.vpr`)| `b1 <_ b2 <==> b1 == false && b2 == true`