Using PVS to validate the algorithms of an exact arithmetic

David Lester; Paul Gowland

doi:10.1016/S0304-3975(02)00226-8

Using PVS to validate the algorithms of an exact arithmetic

David Lester, Paul Gowland

Research output: Contribution to journal › Article › peer-review

Abstract

The whole point of exact arithmetic is to generate answers to numeric problems, within some user-specified error. An implementation of exact arithmetic is therefore of questionable value, if it cannot be shown that it is generating correct answers. In this paper, we show that the algorithms used in an exact real arithmetic are correct. A program using the functions defined in this paper has been implemented in 'C' (a HASKELL version of which we provide as an appendix), and we are now convinced of its correctness. The table presented at the end of the paper shows that performing these proofs found three logical errors which had not been discovered by testing. One of these errors was only detected when the theorems were validated with PVS. © 2002 Elsevier Science B.V. All rights reserved.

Original language	English
Pages (from-to)	203-218
Number of pages	15
Journal	Theoretical Computer Science
Volume	291
Issue number	2
DOIs	https://doi.org/10.1016/S0304-3975(02)00226-8
Publication status	Published - 5 Jan 2003

Keywords

Cauchy sequences
Computable reals
Correctness
Exact arithmetic
PVS

Access to Document

10.1016/S0304-3975(02)00226-8

Cite this

@article{e0af96682da74d36993221f28dbd3c14,

title = "Using PVS to validate the algorithms of an exact arithmetic",

abstract = "The whole point of exact arithmetic is to generate answers to numeric problems, within some user-specified error. An implementation of exact arithmetic is therefore of questionable value, if it cannot be shown that it is generating correct answers. In this paper, we show that the algorithms used in an exact real arithmetic are correct. A program using the functions defined in this paper has been implemented in 'C' (a HASKELL version of which we provide as an appendix), and we are now convinced of its correctness. The table presented at the end of the paper shows that performing these proofs found three logical errors which had not been discovered by testing. One of these errors was only detected when the theorems were validated with PVS. {\textcopyright} 2002 Elsevier Science B.V. All rights reserved.",

keywords = "Cauchy sequences, Computable reals, Correctness, Exact arithmetic, PVS",

author = "David Lester and Paul Gowland",

year = "2003",

month = jan,

day = "5",

doi = "10.1016/S0304-3975(02)00226-8",

language = "English",

volume = "291",

pages = "203--218",

journal = "Theoretical Computer Science",

publisher = "Elsevier BV",

number = "2",

}

TY - JOUR

T1 - Using PVS to validate the algorithms of an exact arithmetic

AU - Lester, David

AU - Gowland, Paul

PY - 2003/1/5

Y1 - 2003/1/5

N2 - The whole point of exact arithmetic is to generate answers to numeric problems, within some user-specified error. An implementation of exact arithmetic is therefore of questionable value, if it cannot be shown that it is generating correct answers. In this paper, we show that the algorithms used in an exact real arithmetic are correct. A program using the functions defined in this paper has been implemented in 'C' (a HASKELL version of which we provide as an appendix), and we are now convinced of its correctness. The table presented at the end of the paper shows that performing these proofs found three logical errors which had not been discovered by testing. One of these errors was only detected when the theorems were validated with PVS. © 2002 Elsevier Science B.V. All rights reserved.

AB - The whole point of exact arithmetic is to generate answers to numeric problems, within some user-specified error. An implementation of exact arithmetic is therefore of questionable value, if it cannot be shown that it is generating correct answers. In this paper, we show that the algorithms used in an exact real arithmetic are correct. A program using the functions defined in this paper has been implemented in 'C' (a HASKELL version of which we provide as an appendix), and we are now convinced of its correctness. The table presented at the end of the paper shows that performing these proofs found three logical errors which had not been discovered by testing. One of these errors was only detected when the theorems were validated with PVS. © 2002 Elsevier Science B.V. All rights reserved.

KW - Cauchy sequences

KW - Computable reals

KW - Correctness

KW - Exact arithmetic

KW - PVS

U2 - 10.1016/S0304-3975(02)00226-8

DO - 10.1016/S0304-3975(02)00226-8

M3 - Article

VL - 291

SP - 203

EP - 218

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 2

ER -

Using PVS to validate the algorithms of an exact arithmetic

Abstract

Keywords

Access to Document

Fingerprint

Cite this