--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on November 2011 ---
What is the right way to use floating-point addition in a specification? For example, I want to say ensures x == y + z; where x, y, and z are variables in the program, and I want the "+" to mean "floating-point addition" (i.e., whatever the "+" means inside the program), not "real (mathematical) addition". Thx, Steve