Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Difference between default and user-defined behavior
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Fri, 09 Jul 2010 13:00:44 +0200
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