--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on April 2014 ---
Thank you for the explanation. When I use the Pre label in the final assertion of my example, these cannot be proven either. I have reformulated the behavior specifications into two equivalent ensures clauses as you have suggested, these can then be proved. However, I very much like bhavior specifications because they nicely match informal specifications and they can be labelled for reference in the documentation. Is there any other way apart from ghost variables to achieve my goal with behaviors? Frank