replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Updated language use in modeling-nondeterminism.md

This commit is contained in:
Ed Stenson 2018-12-06 14:39:06 +00:00
parent 9d5497df0d
commit 8c61e24bfe
1 changed files with 12 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
doc/cprover-manual/modeling-nondeterminism.md
View File

@ -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