Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav07_lecture_4 [2007/03/27 16:28] leander.eyer |
sav07_lecture_4 [2007/03/27 16:33] leander.eyer |
||
---|---|---|---|
Line 139: | Line 139: | ||
and is represented by the function a[0->3][1->2][2->1]. Therefore, the last value of the array is expressed as a[0->3][1->2][2->1](2) = 1. | and is represented by the function a[0->3][1->2][2->1]. Therefore, the last value of the array is expressed as a[0->3][1->2][2->1](2) = 1. | ||
+ | |||
Line 168: | Line 169: | ||
===Avoiding exponential explosion using flattening=== | ===Avoiding exponential explosion using flattening=== | ||
- | Desugaring if-then-else expressions introduces a disjunction of two conjunction. If conditional expressions are embedded, the number of conjunction and conjunctions will explode. | + | Desugaring if-then-else expressions introduces a disjunction of two conjunctions. If conditional expressions are embedded, the number of conjunctions and disjunctions will explode. |
To avoid this explosion of terms, one may introduce additional //variables//. For instance, the expression: | To avoid this explosion of terms, one may introduce additional //variables//. For instance, the expression: | ||
Line 176: | Line 177: | ||
can be flattened as | can be flattened as | ||
- | y<sub>1</sub> = y + 5 | + | y<sub>1</sub> = y + 5\\ |
- | ∧ y<sub>2</sub> = 3y<sub>1</sub> | + | ∧ y<sub>2</sub> = 3y<sub>1</sub>\\ |
- | ∧ x < y<sub>2</sub> | + | ∧ x < y<sub>2</sub>\\ |
- | This gives a new grammar for //atomic formula//: | + | This gives a new grammar for //atomic formulas//: |
A := R(v,...,v) | v = f(v,...,v) | v = c | A := R(v,...,v) | v = f(v,...,v) | v = c | ||
Line 191: | Line 192: | ||
a = a [t<sub>1</sub>->t<sub>2</sub>]; | a = a [t<sub>1</sub>->t<sub>2</sub>]; | ||
- | The value of K is know for //global arrays// (statically defined). The case of dynamically allocated arrays (like the one in Java) will be dealt in a following section. | + | The value of K is known for //global arrays// (statically defined). The case of dynamically allocated arrays (like the one in Java) will be dealt in a further section. |