Merge pull request #3537 from edstenson/review_nondeterminism

Updated language use in modeling-nondeterminism.md

Author: tautschnig

doc/cprover-manual/modeling-nondeterminism.md

@@ -5,7 +5,7 @@
 ### Rationale
 
 Programs typically read inputs from an environment. These inputs can
-take the form of data read from a file, keyboard or network socket, or
+take the form of data read from a file, keyboard, or network socket, or
 arguments passed on the command line. It is usually desirable to analyze
 the program for any choice of these inputs. In Model Checking, inputs
 are therefore modeled by means of *nondeterminism*, which means that the
@@ -16,13 +16,13 @@ computation that results from any choice of inputs.
 
 The CPROVER tools support the following sources of nondeterminism:
 
-- functions that read inputs from the environments;
-- the thread schedule in concurrent programs;
-- initial values of local-scoped variables and memory allocated with
-  `malloc`;
-- initial values of variables that are `extern` in all compilation
-  units;
-- explicit functions for generating nondeterminism.
+- Functions that read inputs from the environments.
+- The thread schedule in concurrent programs.
+- Initial values of local-scoped variables and memory allocated with
+  `malloc`.
+- Initial values of variables that are `extern` in all compilation
+  units.
+- Explicit functions for generating nondeterminism.
 
 The CPROVER tools are shipped with a number of stubs for the most
 commonly used library functions. When executing a statement such as
@@ -46,11 +46,13 @@ probabilistic (or random) choice.
 ### Uninterpreted Functions
 
 It may be necessary to check parts of a program independently.
-Nondeterminism can be used to over-approximate the behaviour of part of
+Nondeterminism can be used to over-approximate the behavior of a part of
 the system which is not being checked. Rather than calling a complex or
 unrelated function, a nondeterministic stub is used. However, separate
 calls to the function can return different results, even for the same
-inputs. If the function output only depends on its inputs then this can
+inputs.
+
+If the function output only depends on its inputs, this can
 introduce spurious errors. To avoid this problem, functions whose names
 begin with the prefix `__CPROVER_uninterpreted_` are treated as
 uninterpreted functions. Their value is non-deterministic but different