An approach for implementing TUNES
12 Apr 1999 01:47:38 +0200
>>>>> "Faré" == Francois-Rene Rideau <firstname.lastname@example.org> writes:
>>> Proving the correctness of drawing routines requires a model of
>>> the video (beware that things are often not exactly the same
>>> when done by the video hardware, and that discrepancies should
>>> "leak" into a security breach when misspecifying what happens
>>> with video or other inexact I/O).
>> That is true... If we specify that operation FOO only puts a
>> pixel on the screen, when it actually makes the monitor blow up,
>> then anyone who the security privilege to put a pixel on the
>> screen will be able to perform operation FOO and thus make the
>> monitor blow up.
Faré> The problem is much more subtle: if you formally define
Faré> "drawing a line" by a given routine, but the actual hardware
Faré> or library routine will draw the line in a different way
Faré> (displacing a few pixels, doing anti-aliasing in a different
Faré> way, etc), then there will be a discrepancy between your
Faré> assumptions and the reality, and an ill-intentionned user or a
Faré> ill-driven program might use this discrepancy to prove an
Faré> absurdity in your system, whence to be able to have the system
Faré> admit any inconsistent axiom.
Faré> Specifying operations as conceptually "simple" as "drawing a
Faré> line" in a way that be both correct and useful is _quite_
Faré> challenging! The same could be said of "real number"
Faré> arithmetics, all the more when you want to relate your "real"
Faré> arithmetics implementation (IEEE or not) to approximations of
Faré> actual mathematical numbers. Again, this does NOT mean that
Faré> the task is unfeasible: when people design programs so as to
Faré> be correct, they do, in their right mind, do this work of
Faré> relating implementations to specifications, so that, when
Faré> programs are actually correct, there _is_ a way that could be
Faré> found to prove it. But this is nonetheless a very complex
Faré> task for which tools are currently lacking.
I tend to think that there should be several specifications of
"drawing a line". Because, sometimes you just don't care if
antialiasing is done an how it is done, and sometimes you really care
about the precise value of each pixel (if are implementing
antialiasing for instance). Given the context, one level of
abstraction is better than others.