| Thread Links | Date Links | ||||
|---|---|---|---|---|---|
| Thread Prev | Thread Next | Thread Index | Date Prev | Date Next | Date Index |
On 08/02/2011 06:06 PM, Nate Hayes wrote:
I mean, what is the purpose of having all the formalism for a FTDIA if a user's program can no longer be validated by it as soon as they include a single intersection or union operation? Intersection and union are very common operations in interval programs and algorithms...
Motion 26 has a concept of intersection and union, hence supports all such calculations. But for safety reasons it requires that the result is always a bare interval -- since the decoration it should get (if any) must depend on the context.
so perhaps the majority of programs will be beyond the reach of FTDIA to verify.
Traditional interval arithmetic without decorations has no FTIA for computations with intersection. Nevertheless, many verifying interval algorithms using intersection are in use.
Interval techniques usually validate things without decorations - otherwise they couldn't have thrived in the past.
For verification, decorations are only needed for checking the hypotheses of fixed point theorems.