--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on July 2010 ---
Hi, the Jessie tutorial defines Default behavior and User-defined behavior on p. 5 as follows: - Default behavior: VC in this group concern the verification of a function?s default behavior, which includes verification of its postcondition, frame condition, loop invariants and intermediate assertions. - User-defined behavior: VC in this group concern the verification of a function?s user-defined behavior, which includes verification of its postcondition, frame condition, loop invariants and intermediate assertions for this specific behavior. I assume that user-defined behavior refers to behavior defined by the user with the keyword "behavior". If this is true, I suggest to point this out more clearly in the tutorial. Also, both the definition of Default behavior and User-defined behavior are circular, which should be avoided. on p. 7, also Normal behavior is mentioned. What is this? -- Regards, Boris