Changes between Version 11 and Version 12 of Language
- Timestamp:
- 05/18/23 12:14:38 (3 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
Language
v11 v12 83 83 end up with the same values at termination). 84 84 85 === Abstract (uninterpreted) functions 85 === Abstract (uninterpreted) functions: `$abstract` 86 86 87 87 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., … … 91 91 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. 92 92 93 === Atomic functions 93 === Atomic functions: `$atomic_f` 94 94 95 95 A function is declared atomic using the function qualifier `$atomic_f`, e.g., … … 103 103 An atomic function must have a definition; in particular, neither a system function nor an abstract function may be declared using `$atomic_f`. 104 104 105 === System functions 105 === System functions: `$system` 106 106 107 107 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. … … 109 109 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. 110 110 111 === Pure functions 111 === Pure functions: `$pure` 112 112 113 113 A system or atomic function may be declared to be `$pure`, e.g., … … 183 183 184 184 185 === Th e `$here` scope expression185 === This scope: the `$here` scope expression 186 186 Expression of type `$scope`, evaluating to the dynamic scope in which the evaluation takes place. 187 187 188 === The null process reference 188 === The null process reference: `$proc_null` 189 189 The 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`. 190 190 191 === The root scope constant 191 === The root scope constant: `$root` 192 192 Constant of type `$scope`, the root dynamic scope. 193 193 … … 425 425 == Functions 426 426 427 === `$assert`427 === Assertions: `$assert` 428 428 429 429 The system function `$assert` has the signature … … 443 443 If x=3 and B=2, the assertion is violated and CIVL prints the error message “x-coordinate 3 exceeds bound 2”. 444 444 445 === `$assume`445 === Assumptions: `$assume` 446 446 447 447 === `$assume_push`
