Changes between Version 15 and Version 16 of Fundamentals

Timestamp:

05/14/23 10:26:02 (3 years ago)

Author:

siegel

Comment:

--

Fundamentals

@@ -59 +59 @@
 == Qualifiers
 
-* `$input`
-* `$output`
-* `$abstract`
-* `$atomic_f`
-* `$system`
-* `$pure`
+=== The `$input` and  `$output` type qualifiers
+
+The declaration of a variable in the root scope may include the type qualifier `$input`, e.g.,
+{{{
+$input int N;
+}}}
+This declares the variable to be an input variable, i.e., one which is considered to be an input to the program.
+Such a variable is initialized with an arbitrary (unconstrained) value of its type.
+When using symbolic execution to verify a program, such a variable will be assigned a unique symbolic constant of its type.
+In contrast, variables in the root scope which are not input variables will instead be initialized with the “undefined” value.
+Reading an undefined value is erroneous. [Note: the model checker attempts to catch such errors but currently
+does not do so for arrays, which are always initialized with unconstrained values.]
+In addition, input variables may only be read, never written to; an attempt to write to an input variable is also flagged as an error.
+
+Alternatively, it is possible to specify a particular concrete value for an input variable, either on the command line, e.g.,
+{{{
+civl verify -inputN=8 ...
+}}}
+or by including an initializer in the declaration, e.g.
+{{{
+$input int N=8;
+}}}
+The protocol for initializing an input variable is the following: if a command line value is specified, it is used.
+Otherwise, if an initializer is present, it is used.   Otherwise, the variable is assigned an arbitrary value of its type.
+
+A variable in the root scope may be declared with `$output` to declare it to be an output variable.
+Output variables may only be written to, never read.
+They are used primarily in functional equivalence checking.
+
+Input and output variables play a key role when determining whether two programs are functionally equivalent.
+Two programs are considered functionally equivalent if, whenever they are given the same inputs (i.e., corresponding $input
+variables are initialized with the same values) they will produce the same outputs (i.e., corresponding $output variables will 
+end up with the same values at termination).
+
+=== `$abstract`
+
+=== `$atomic_f`
+
+=== `$system`
+
+=== `$pure`
 
 == Types