  Test instability in a floating-point program occurs when the control flow of
the program diverges from its ideal execution assuming real arithmetic. This
phenomenon is caused by the presence of round-off errors that affect the
evaluation of arithmetic expressions occurring in conditional statements.
Unstable tests may lead to significant errors in safety-critical applications
that depend on numerical computations. Writing programs that take into
consideration test instability is a difficult task that requires expertise on
finite precision computations and rounding errors. This paper presents a
toolchain to automatically generate and verify a provably correct test-stable
floating-point program from a functional specification in real arithmetic. The
input is a real-valued program written in the Prototype Verification System
(PVS) specification language and the output is a transformed floating-point C
program annotated with ANSI/ISO C Specification Language (ACSL) contracts.
These contracts relate the floating-point program to its functional
specification in real arithmetic. The transformed program detects if unstable
tests may occur and, in these cases, issues a warning and terminate. An
approach that combines the Frama-C analyzer, the PRECiSA round-off error
estimator, and PVS is proposed to automatically verify that the generated
program code is correct in the sense that, if the program terminates without a
warning, it follows the same computational path as its real-valued functional
specification.
