--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on July 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Difference between default and user-defined behavior



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