--- layout: fc_discuss_archives title: Message 85 from Frama-C-discuss on January 2014 ---
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;