Ignore:
Timestamp:
Mar 28, 2013, 12:07:56 AM (7 years ago)
Author:
campbell
Message:

Add "only one return" invariant to RTLabs functions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_syntax.ma

    r2936 r2992  
    9090; f_entry     : Σl:label. present ?? f_graph l
    9191; f_exit      : Σl:label. present ?? f_graph l
     92; f_only_exit : ∀l. lookup … f_graph l = Some ? St_return → l = f_exit
    9293}.
    9394
Note: See TracChangeset for help on using the changeset viewer.