--- layout: fc_discuss_archives title: Message 85 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP - How to represent duplicate assumes?



Hi,

For this example, some of my behaviors share a set of assumes. For example, HighSaO2, LowSaO2, and RoundSaO2 share the assumes !Is_Adv_or_Mon_Failed predicate.

Is there a possibility to declare assumes that are shared by a set of behaviors only once, just to make the behavioral spec lean?


Thanks a lot.
Dharma



 behavior HighSaO2: // SaO2 exceeds max
    assumes !Is_Adv_or_Mon_Failed(mbMonitorFailed, mtstAdvisoryStatus.tenumState);
    assumes mtenumPruStatus == PRU_OFF;
    ensures mfSaO2 > nPULSEOX_MAX_VALUE ==> mtenumDataValidity == DATA_INVALID;
 
   behavior LowSaO2: // SaO2 below min
    assumes !Is_Adv_or_Mon_Failed(mbMonitorFailed, mtstAdvisoryStatus.tenumState);
    assumes mtenumPruStatus == PRU_OFF;
    ensures mfSaO2 < nPULSEOX_MIN_VALUE ==> mtenumDataValidity == DATA_INVALID;

   behavior RoundSaO2: // SaO2 rounded to the nearest int
     assumes !Is_Adv_or_Mon_Failed(mbMonitorFailed, mtstAdvisoryStatus.tenumState);
     ensures is_rounded(\old(mfSaO2), mfSaO2);

   behavior Reset:
    ensures mfSaO2 > nPULSEOX_MAX_VALUE ==> mfSaO2 == nPULSEOX_MAX_VALUE;