A Formal Proof of Square Root and Division Elimination in Embedded Programs
The use of real numbers in a program can introduce differences between the expected and the actual behavior of the program, due to the finite representation of these numbers. Therefore, one may want to define programs using real numbers such that this difference vanishes. This paper defines a progra...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
University of Bologna
2013-01-01
|
| Series: | Journal of Formalized Reasoning |
| Subjects: | |
| Online Access: | http://jfr.unibo.it/article/view/3887 |