fact: Definition desugarBehaviour (specs:list FULL_SPEC_CASE.t) (m:METHOD.t) : list FULL_SPEC_CASE.t := let setSpecCaseType (spec:FULL_SPEC_CASE.t) (sct:SpecCaseType) : FULL_SPEC_CASE.t := let (_,v,r,cc,case) := spec in FULL_SPEC_CASE.Build_t sct v r cc case in let setVisibility (spec:FULL_SPEC_CASE.t) (vo:option Visibility) : FULL_SPEC_CASE.t := let (sct,_,r,cc,case) := spec in FULL_SPEC_CASE.Build_t sct vo r cc case in let desugar1 (spec0:FULL_SPEC_CASE.t) : FULL_SPEC_CASE.t := let vis := match FULL_SPEC_CASE.visibility spec0, FULL_SPEC_CASE.specCaseType spec0 with | Some v', _ => v' | None, lightweight => METHOD.visibility m | None, _ => Package end in match FULL_SPEC_CASE.specCaseType spec0 with | lightweight => let spec1 := setSpecCaseType spec0 behaviour in let spec2 := setVisibility spec1 (Some vis) in let spec3 := addDefaults spec2 m (lightweightDefaults spec2 m) in spec3 | normal_behaviour => let spec1 := setSpecCaseType spec0 behaviour in let spec2 := setVisibility spec1 (Some vis) in let spec3 := addBody spec2 (signalsC false (Exception_e, (: false' :)%jml)) in spec3 | exceptional_behaviour => let spec1 := setSpecCaseType spec0 behaviour in let spec2 := setVisibility spec1 (Some vis) in let spec2 := addBody spec2 (ensuresC false (: false' :)%jml) in spec2 | behaviour => setVisibility spec0 (Some vis) end in map desugar1 specs.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)