| Popis: |
Computing accurately with real numbers is always a challenge. This is particularly true in critical embedded systems since memory issues do not allow the use of dynamic data structures. This constraint imposes a finite representation of the real numbers, provoking uncertainties and rounding errors that might modify the actual behavior of a program from its ideal one. This article presents a solution to this problem with a program transformation that eliminates square roots and divisions in straight line programs without nested function calls. These two operations are the source of infinite sequences of digits in numerical representations, thus, eliminating these operations allows to compute exactly using for example a fixed-point number representation with a sufficient number of bits. In order to avoid an explosion of the size of the produced code this transformation relies on a particular anti-unification to realize a partial inlining of the variable and function definitions. This transformation targeting code for aeronautics certified in PVS, we want to prove the semantics preservation in this proof assistant. Thus we use both an OCaml implementation and the subtyping features of PVS to ensure the correctness of the transformation by defining a proof-producing (certifying) program transformation, providing a specific semantics preservation lemma for every definition in the transformed program. |
