Changes between Version 1 and Version 2 of Language


Ignore:
Timestamp:
05/16/23 23:06:18 (3 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Language

    v1 v2  
    1 
    21= CIVL-C Language Manual
    32
    4 == Qualifiers
    5 
    6 === The `$input` and  `$output` type qualifiers
    7 
    8 The declaration of a variable in the root scope may include the type qualifier `$input`, e.g.,
    9 {{{
    10 $input int N;
    11 }}}
    12 This declares the variable to be an input variable, i.e., one which is considered to be an input to the program.
    13 Such a variable is initialized with an arbitrary (unconstrained) value of its type.
    14 When using symbolic execution to verify a program, such a variable will be assigned a unique symbolic constant of its type.
    15 In contrast, variables in the root scope which are not input variables will instead be initialized with the “undefined” value.
    16 Reading an undefined value is erroneous. [Note: the model checker attempts to catch such errors but currently
    17 does not do so for arrays, which are always initialized with unconstrained values.]
    18 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.
    19 
    20 Alternatively, it is possible to specify a particular concrete value for an input variable, either on the command line, e.g.,
    21 {{{
    22 civl verify -inputN=8 ...
    23 }}}
    24 or by including an initializer in the declaration, e.g.
    25 {{{
    26 $input int N=8;
    27 }}}
    28 The protocol for initializing an input variable is the following: if a command line value is specified, it is used.
    29 Otherwise, if an initializer is present, it is used.   Otherwise, the variable is assigned an arbitrary value of its type.
    30 
    31 A variable in the root scope may be declared with `$output` to declare it to be an output variable.
    32 Output variables may only be written to, never read.
    33 They are used primarily in functional equivalence checking.
    34 
    35 Input and output variables play a key role when determining whether two programs are functionally equivalent.
    36 Two programs are considered functionally equivalent if, whenever they are given the same inputs (i.e., corresponding $input
    37 variables are initialized with the same values) they will produce the same outputs (i.e., corresponding $output variables will
    38 end up with the same values at termination).
    39 
    40 === `$abstract`
    41 
    42 An abstract function declares a function without a body.  An abstract function is declared using a standard function prototype with the function qualifier `$abstract`, e.g.,
    43 {{{
    44   $abstract int f(int x);
    45 }}}
    46 An abstract function must have a non-void return type and take at least one parameter.   An invocation of an abstract function is an expression and can be used anywhere an expression is allowed.  The interpretation is an "uninterpreted function".    A unique symbolic constant of function type will be created, corresponding to the abstract function, and invocations are represented as applications of the uninterpreted function to the arguments. 
    47 
    48 === `$atomic_f`
    49 
    50 A function is declared atomic using the function qualifier `$atomic_f`, e.g.,
    51 {{{
    52 $atomic_f int f(int x) {
    53   ...
    54 }
    55 }}}
    56 A call to such a function executes as a single atomic step, i.e., without interleaving from other processes.   Hence, this is only relevant for concurrent programs.  Declaring a function to be atomic is almost equivalent to placing `$atomic{ ... }` around the function body.   The difference is that in the latter case, the call to the function and the execution of the body are executed in two atomic steps, i.e., after activation frame is pushed onto the call stack, another process could execute before the first process obtains the atomic lock and executes its body.   For an atomic function, the entire sequence of events happens in one atomic step.
    57 
    58 An atomic function must have a definition; in particular, neither a system function nor an abstract function may be declared using `$atomic_f`.
    59 
    60 === `$system`
    61 
    62 A system function is one in which the definition of the function is not provided in CIVL-C code, but is implemented instead in a certain Java class.  A system function is declared by adding the function qualifier `$system` to a function prototype.  Invocation of a system function always takes place in a single atomic step.
    63 
    64 A system function may have a guard, which is specified in the function contract using a `$executes_when` clause.  Unless constrained by its contract or other qualifiers, a system function may modify the stay in an arbitrary way.
    65 
    66 === `$pure`
    67 
    68 A system or atomic function may be declared to be `$pure`, e.g.,
    69 {{{
    70 $pure $system double sin(double x);
    71 $pure $atomic_f double mysin(double x) {
    72   return  x - x*x*x/6.;
    73 }
    74 }}}
    75 This means that the function is a mathematical function of its arguments only.    I.e., an invocation of the function has no side-effects and the return value depends on the arguments only (if called twice with the same arguments, it will return the same value, regardless of any differences in the state).   The user is responsible for ensuring that a function declared pure actually is pure.    If this is not the case, the model checker may produce incorrect results.
    76 
    773== Types
    784
    … …  
    806
    817The boolean type is denoted `_Bool`, as in C. Its values are 0 and 1, which are also denoted by `$false` and `$true`, respectively.
     8One may also include the standard C header `stdbool.h`, which defines `false` and `true` (also as 0 and 1), and defines the type
     9`bool` to be an alias for `_Bool`.
    8210
    8311=== The integer type
    … …  
    11846Ranges are typically used as a step in constructing domains.
    11947They can also be used in quantified expressions to specify the domain of a bound variable (see `$forall` and `$exists`).
     48
     49== Type qualifiers
     50
     51=== The `$input` and  `$output` type qualifiers
     52
     53The declaration of a variable in the root scope may include the type qualifier `$input`, e.g.,
     54{{{
     55$input int N;
     56}}}
     57This declares the variable to be an input variable, i.e., one which is considered to be an input to the program.
     58Such a variable is initialized with an arbitrary (unconstrained) value of its type.
     59When using symbolic execution to verify a program, such a variable will be assigned a unique symbolic constant of its type.
     60In contrast, variables in the root scope which are not input variables will instead be initialized with the “undefined” value.
     61Reading an undefined value is erroneous. [Note: the model checker attempts to catch such errors but currently
     62does not do so for arrays, which are always initialized with unconstrained values.]
     63In addition, input variables may only be read, never written to; an attempt to write to an input variable is also flagged as an error.
     64
     65Alternatively, it is possible to specify a particular concrete value for an input variable, either on the command line, e.g.,
     66{{{
     67civl verify -inputN=8 ...
     68}}}
     69or by including an initializer in the declaration, e.g.
     70{{{
     71$input int N=8;
     72}}}
     73The protocol for initializing an input variable is the following: if a command line value is specified, it is used.
     74Otherwise, if an initializer is present, it is used.   Otherwise, the variable is assigned an arbitrary value of its type.
     75
     76A variable in the root scope may be declared with `$output` to declare it to be an output variable.
     77Output variables may only be written to, never read.
     78They are used primarily in functional equivalence checking.
     79
     80Input and output variables play a key role when determining whether two programs are functionally equivalent.
     81Two programs are considered functionally equivalent if, whenever they are given the same inputs (i.e., corresponding $input
     82variables are initialized with the same values) they will produce the same outputs (i.e., corresponding $output variables will
     83end up with the same values at termination).
     84
     85===  Abstract (uninterpreted) functions
     86
     87An abstract function declares a function without a body.  An abstract function is declared using a standard function prototype with the function qualifier `$abstract`, e.g.,
     88{{{
     89  $abstract int f(int x);
     90}}}
     91An abstract function must have a non-void return type and take at least one parameter.   An invocation of an abstract function is an expression and can be used anywhere an expression is allowed.  The interpretation is an "uninterpreted function".    A unique symbolic constant of function type will be created, corresponding to the abstract function, and invocations are represented as applications of the uninterpreted function to the arguments. 
     92
     93=== Atomic functions
     94
     95A function is declared atomic using the function qualifier `$atomic_f`, e.g.,
     96{{{
     97$atomic_f int f(int x) {
     98  ...
     99}
     100}}}
     101A call to such a function executes as a single atomic step, i.e., without interleaving from other processes.   Hence, this is only relevant for concurrent programs.  Declaring a function to be atomic is almost equivalent to placing `$atomic{ ... }` around the function body.   The difference is that in the latter case, the call to the function and the execution of the body are executed in two atomic steps, i.e., after activation frame is pushed onto the call stack, another process could execute before the first process obtains the atomic lock and executes its body.   For an atomic function, the entire sequence of events happens in one atomic step.
     102
     103An atomic function must have a definition; in particular, neither a system function nor an abstract function may be declared using `$atomic_f`.
     104
     105=== System functions
     106
     107A system function is one in which the definition of the function is not provided in CIVL-C code, but is implemented instead in a certain Java class.  A system function is declared by adding the function qualifier `$system` to a function prototype.  Invocation of a system function always takes place in a single atomic step.
     108
     109A system function may have a guard, which is specified in the function contract using a `$executes_when` clause.  Unless constrained by its contract or other qualifiers, a system function may modify the stay in an arbitrary way.
     110
     111=== Pure functions
     112
     113A system or atomic function may be declared to be `$pure`, e.g.,
     114{{{
     115$pure $system double sin(double x);
     116$pure $atomic_f double mysin(double x) {
     117  return  x - x*x*x/6.;
     118}
     119}}}
     120This means that the function is a mathematical function of its arguments only.    I.e., an invocation of the function has no side-effects and the return value depends on the arguments only (if called twice with the same arguments, it will return the same value, regardless of any differences in the state).   The user is responsible for ensuring that a function declared pure actually is pure.    If this is not the case, the model checker may produce incorrect results.
    120121
    121122== Expressions
    … …  
    182183
    183184
    184 === `$here`
     185=== The `$here` scope expression
    185186Expression of type `$scope`, evaluating to the dynamic scope in which the evaluation takes place.
    186187
    187 === `$proc_null`
     188=== The null process reference
    188189The null process constant.  Similar to the NULL pointer, this gives an object of `$proc` type a defined value, and can be used in `==` and `!=` expressions.  It cannot be used as the argument to `$wait` or `$waitall`.
    189190
    190 === `$root`
     191=== The root scope constant
    191192Constant of type `$scope`, the root dynamic scope.
    192193
    … …  
    200201Precisely, the infinite sequence is intersected with the set of integers greater than or equal to `lo`.
    201202
    202 === `$scopeof`
     203=== The scope of an expression
    203204
    204205Given any left-hand-side expression ''expr'', the expression `$scopeof(`''expr''`)` evaluates to the dynamic scope containing the object specified by ''expr''.
    … …  
    237238Each of these expressions is erroneous if `s1` or `s2` is undefined.  This error is reported by the model checker.
    238239
    239 === `$self`
     240=== This process: `$self`
    240241
    241242This expression of `$proc` type returns a reference to the process which is evaluating this expression.  It provides a way for code to obtain the identity of the process executing the code.