--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on April 2014 ---
Hello Virgile, thanks for this interesting hint. I have seen a similar approach in this report, however, without using an automaton: Burghardt, J.; Carben, A.; Gerlach, J.; Pohl, H. & Voellinger, K. ACSL By Example. Towards a Verified C Standard Library Fraunhofer FIRST, 2013 I think it is a rather elaborate way to specify a seemingly simple behaviour. Moreover, in my real example I am working at, this behaviour is only part of a more complex specification: an erroneous situtation must occur three times in a row before an error code is returned, otherwise a default value is given back, or the proper value calculated and returned. I will first stick with Anne's proposal. When I have my specification got proper and there is still time left I will have a closer look at the Aorai manual. Frank