Options
Algorithms for verified inclusions: theory and practice
Citation Link: https://doi.org/10.15480/882.316
Publikationstyp
Book Part
Date Issued
1988
Sprache
English
Author(s)
Institut
TORE-DOI
Start Page
109
End Page
126
Citation
Erstveröffentlichung in: Reliability in computing: the role of interval methods in scientific computing. Academic Press Professional, Inc. San Diego, 1988. S. 109-126
ISBN
978-1-4832-7784-4
978-0-12-505630-4
In the following basic principles of algorithms computing guaranteed bounds are developed from a theoretical and a practical point of view. Some fundamental theoretical facts are repeated where, for more detailed information, the reader is referred to the literature (...)
Furthermore practical aspects are discussed, especially how the process of computing a guaranteed result really works performed by means of checking assumptions of mathematical theorems. This checking process is performed automatically. The various steps from the mathematical theorem down to the practical verification are described in detail.
In contrast, standard floating-point algorithms usually deliver good approximations to the solution of a given numerical problem but there is neither a verification or a solution to the given problem actually exist. There are simple examples where the floating-point approximation is drstically wrong.
A programming environment has been developed which allows to specify commands to the computer in mathematical notation. Because the system (preliminary name CALCULUS) works interactively, no type specification is necessary at all allowing specifying algorithms like in a math book.
CALCULUS works right now on IBM System /370 machines under VM operating system. It is planned to have a C version for IBM System/2, SUN work stations and others available early next year. Some examples demonstrating the system are presented.
Furthermore practical aspects are discussed, especially how the process of computing a guaranteed result really works performed by means of checking assumptions of mathematical theorems. This checking process is performed automatically. The various steps from the mathematical theorem down to the practical verification are described in detail.
In contrast, standard floating-point algorithms usually deliver good approximations to the solution of a given numerical problem but there is neither a verification or a solution to the given problem actually exist. There are simple examples where the floating-point approximation is drstically wrong.
A programming environment has been developed which allows to specify commands to the computer in mathematical notation. Because the system (preliminary name CALCULUS) works interactively, no type specification is necessary at all allowing specifying algorithms like in a math book.
CALCULUS works right now on IBM System /370 machines under VM operating system. It is planned to have a C version for IBM System/2, SUN work stations and others available early next year. Some examples demonstrating the system are presented.
DDC Class
600: Technology
Loading...
Name
Ru88a.pdf
Size
530.64 KB
Format
Adobe PDF