Changes between Version 13 and Version 14 of Fundamentals


Ignore:
Timestamp:
05/13/23 18:31:34 (3 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Fundamentals

    v13 v14  
    5656As usual, a translation unit consists of a sequence of variable declarations, function prototypes, and function definitions in file scope. In addition, assume statements may occur in the file scope.  These are used to state assumptions on the input values to a program.
    5757
    58 == Sequential Elements
    5958
    60 In this chapter we describe the main sequential elements of the language. For the most part these are the same as in C. Primitives dealing with concurrency are introduced in the next chapter.
     59== Qualifiers
    6160
    62 ===  Types
     61* `$input`
     62* `$output`
     63* `$abstract`
     64* `$atomic_f`
     65* `$system`
     66* `$pure`
    6367
    64 ==== Standard types inherited from C
     68== Types
    6569
    66 The `civlc.cvh` defines standard types inherited from C. The boolean type is denoted `_Bool`, as in C. Its values are 0 and 1, which are also denoted by `$false` and `$true`, respectively.
     70The boolean type is denoted `_Bool`, as in C. Its values are 0 and 1, which are also denoted by `$false` and `$true`, respectively.
    6771
    6872There is one integer type, corresponding to the mathematical integers. Currently, all of the C integer types `int`, `long`, `unsigned int`, `short`, etc., are mapped to the CIVL integer type.
    … …  
    7074There is one real type, corresponding to the mathematical real numbers. Currently, all of the C real types `double`, `float`, etc., are mapped to the CIVL real type.
    7175
    72 Array types, `struct` and `union` types, `char`, and pointer types (including pointers to functions) are all exactly as in C.
     76* `$proc`:  `$self`, `$proc_null`
     77* `$scope`: An object of type `$scope` is a reference to a dynamic scope. It may be thought of as a “dynamic scope ID, ” but it is not an integer and cannot be converted to an integer.
     78* `$domain`: A domain type is used to represent a set of tuples of integer values. Every tuple in a domain object has the same arity (i.e., number of components). The arity must be at least 1, and is called the dimension of the domain object.  For each integer constant expression n, there is a type `$domain(n)`, representing domains of dimension n. The universal domain type, denoted `$domain`, represents domains of all positive dimensions, i.e., it is the union over all n ≥ 1 of `$domain(n)`. In particular, each `$domain(n)` is a subtype of `$domain`.   There are expressions for specifying domain values.  Certain statements use domains, such as the “CIVL-for” loop `$for`
     79* `$range`: An object of this type represents an ordered set of integers. There are expressions for specifying range values;  Ranges are typically used as a step in constructing domains
    7380
    74 ==== The bundle type: `$bundle`
     81== Expressions
    7582
    76 CIVL-C includes a type named `$bundle`, declared in the CIVL-C standard header `bundle.cvh`. A bundle is basically a sequence of data, wrapped into an atomic package. A bundle is created using a function that specifies a region of memory. One can create a bundle from an array of integers, and another bundle from an array of reals. Both bundles have the same type, `$bundle`. They can therefore be entered into an array of `$bundle`, for example. Hence bundles are useful for mixing objects of different (even statically unknown) types into a single data structure. Later, the contents of a bundle can be extracted with another function that specifies a region of memory into which to unpack the bundle; if that memory does not have the right type to receive the contents of the bundle, a runtime error is generated. The bundle type and its functions are provided by the library `bundle.cvh`.
    77 The relevant functions for creating and manipulating bundles are given in ...
     83* `=>`
     84* `$true`
     85* `$false`
     86* `$forall`
     87* `$exists`
     88* `$pow(double, double)`
    7889
    79 ==== The `$scope` type
     90== Statements
    8091
    81 An object of type `$scope` is a reference to a dynamic scope. It may be thought of as a “dynamic
    82 scope ID, ” but it is not an integer and cannot be converted to an integer. Operations defined on scopes are discussed in Section ....
     92* `$assert`
     93* `$assume`
     94* `$atomic`
     95* `$choose`
     96* `$choose_int()`
     97* `$default_value()`
     98* `$elaborate`
     99* `$elaborate_domain()`
     100* `$exit`
     101* `$for`
     102* `$free`
     103* `$havoc()`
     104* `$hidden()`
     105* `$hide()`
     106* `$is_terminated($proc)`
     107* `$local_end()`
     108* `$local_start()`
     109* `$malloc`
     110* `$parfor`
     111* `$reveal()`
     112* `$spawn`
     113* `$wait`
     114* `$waitall`
     115* `$when`
     116* `$yield()`
    83117
    84 ==== The `$range` and `$domain` types
    85118
    86 CIVL-C provides certain abstract datatypes that are useful for representing iteration spaces of loops in an abstract way.
    87 First, there is a built-in type `$range`. An object of this type represents an ordered set of integers. There are expressions for specifying range values; these are described in Section .... Ranges are typically used as a step in constructing domains, described next.
     119== Contract Annotations
    88120
    89 A domain type is used to represent a set of tuples of integer values. Every tuple in a domain object has the same arity (i.e., number of components). The arity must be at least 1, and is called the dimension of the domain object.
     121clauses
    90122
    91 For each integer constant expression n, there is a type `$domain(n)`, representing domains of dimension n. The universal domain type, denoted `$domain`, represents domains of all positive dimensions, i.e., it is the union over all n ≥ 1 of `$domain(n)`. In particular, each `$domain(n)` is a subtype of `$domain`.
    92 There are expressions for specifying domain values; these are described in Section 6.2.3.2. There are also certains statements that use domains, such as the “CIVL-for” loop `$for`; see Section ...
     123* `depends_on`
     124* `executes_when`
     125* `\nothing`