team-worthwhile/worthwhile — Issue #14: Arrays are not considered in WP calculation
Author: bafain
Created: 2012-01-31 12:28:22+00:00
State: open

1. Implement array literals as functions (see `ArrayFunction`, which has already been added to the model)
2. Implement constant `ArrayFunction`s for implicit default values and insert them into declarations using the `ImplicitInitialValueInserter`
3. Ensure that several `ArrayFunction` instances can reference the same `ArrayFunction` in their `chainedFunction` attribute
4. Whenever an array assignment occurs, i. e. `WPStrategy::visit(Assignment)` is called:
1. Instantiate a new `ArrayFunction` that maps the assignment index to the assignment value and any other index to the assignment array's initial value
2. Instantiate a new array type `VariableDeclaration` whose initial value is the just instantiated `ArrayFunction`
3. Replace all variable references in the weakest precondition by a reference to the just instantiated `VariableDeclaration`
5. Do not forget to recurse into the `ArrayFunction` chains referenced in the weakest precondition to replace `VariableReferences` which can occur both in the index and the value `Expressions`