Changes between Version 9 and Version 10 of OmnibusChanges


Ignore:
Timestamp:
08/03/13 15:26:48 (13 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • OmnibusChanges

    v9 v10  
    1111 * The type of this expression is `CIVLDynamicType`.  When evaluated, it returns the dynamic type determined by the current state and the given static type.  (This assumes extent expressions are stored in array types.)  For example, if `t` is the static type `struct foo { double a[n]; }` from the source code above, then `DynamicTypeOf(t)`, evaluated in the state that arises at that point in the source code, will yield the symbolic type which is a record type with one field which is an array of doubles of length 2.  Now you can store that dynamic type in a variable if you want to save it, e.g., insert a statement like this into the model:
    1212  * `CIVLDynamicType __struct_foo__ = DynamicTypeOf(struct foo { double a[n]; });`
    13 * add a new kind of CIVL expression: `InitialValue[variable, dynamicType]`. Here, `variable` is a (static) `Variable`, and `dynamicType` is an expression of type `CIVLDynamicType`.   The type of this expression is the type of the variable.  When evaluated, it returns a default initial value for a variable with the given dynamic type.  This can be used to initialize arrays and structs.
     13* add a new kind of CIVL expression: `InitialValue[variable]`. Here, `variable` is a (static) `Variable`.  The type of this expression is the type of the variable.  When evaluated, it returns a default initial value for a variable with the dynamic type determined by the current state and the static type of the variable.  This can be used to initialize arrays and structs.
    1414* add a new `CIVLType`: `CIVLScopeType`
    1515* add new subtype of `Variable`: `CIVLScopeVariable` with method
    … …  
    3838 * add the variable `v` to the current scope with the translated type `t` as usual
    3939 * add an assignment statement at the current location: `v=InitialValue[v, DynamicTypeOf(t)]`
    40 * Evaluation of `DynamicTypeOf(t)` in a state `s` is defined as follows:
    41  * if `t` is a struct type, say with tag `foo`, then the result is the result of evaluating the variable (in s) `__struct_foo__`
    42  * if `t` is an array type with element type `E` and length expression `l`, the result is obtained by evaluating `CIVLDynamicType(E)`, call the result `de`; evaluating `l`, call the result `dl`; and return `completeArrayType(de,dl)` (eliding the wrapping and unwrapping of the symbolic type into a symbolic expression value)
    43 * Evaluation of `InitialValue[v,d]` is as follows:
    44  * for a primitive dynamic type, some undefined value (null expression)?
    45  * define a method in the `Evaluator`, `SymbolicExpression computeInitialValue(LHSExpression expr, SymbolicType dynamicType);`
    46  * if `dynamicType` is a tuple type, create the concrete tuple of type of that type with each component obtained by evaluating `computeInitialValue(dotExpression(…), componentType)`
     40* define a method in the `Evaluator`, `SymbolicType getDynamicType(State s, Type t)`
     41 * if `t` is a primitive type, map to the corresponding symbolic type
     42 * if `t` is a struct type, say with tag `foo`, then the result is the result of evaluating the variable (in s) `__struct_foo__` and extracting the symbolic type from the result
     43 * if `t` is an array type with element type `E` and length expression `l`, the result is obtained by evaluating `getDynamicType(s, E)`, call the result `de`; evaluating `l`, call the result `dl`; and returning `completeArrayType(de,dl)` (eliding the wrapping and unwrapping of the symbolic type into a symbolic expression value)
     44* define a method in the `Evaluator`, `SymbolicType computeDynamicType(State s, Type t)`
     45 * if `t` is a struct type, return the symbolic tuple type obtained by invoking `computeDynamicType` recursively on the component types of `t`
     46 * if `t` is an array type or primitive type proceed analogously to `getDynamicType`
     47* define a method in the `Evaluator`, `SymbolicExpression computeInitialValue(State s, LHSExpression expr, SymbolicType dynamicType);`
     48 * if `dynamicType` is a tuple type, create the concrete tuple of that type with each component obtained by evaluating `computeInitialValue(s, dotExpression(…), componentType)`
    4749 * if `dynamicType` is an array type, create a unique symbolic constant name based on the LHS expression and a symbolic constant with that name and type `dynamicType` (no recursion in this case)
     50* Evaluation of `DynamicTypeOf(t)` in a state `s` is defined by `computeDynamicType(s,t)`
     51* Evaluation of `InitialValue[v]` is as follows:
     52 * let `t` be the (static) type of `v`
     53 * if `t` is primitive, return appropriate symbolic value (null expression, …)
     54 * else let `d` be `getDynamicType(s,t)`
     55 * return `computeInitialValue(s, v, d)`
    4856
    49 
     57