Changeset 723 for src/LTL


Ignore:
Timestamp:
Mar 30, 2011, 12:34:25 PM (9 years ago)
Author:
mulligan
Message:

Added dependent type internalising the invariant that LIN function bodies are non-empty and do not start with a label.

Location:
src/LTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r722 r723  
    11include "common/Graphs.ma".
    2 include "common/AST.ma".
    3 
    42include "utilities/IdentifierTools.ma".
    5 
    6 include "ASM/I8051.ma".
    7 include "ASM/String.ma".
    83
    94include "LIN/LIN.ma".
  • src/LTL/LTLToLIN.ma

    r722 r723  
    22include "LIN/LIN.ma".
    33
    4 definition translate_statement: ∀globals. LTLStatement globals → LINStatement globals ≝
     4definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝
    55  λglobals: list Identifier.
    66  λs: LTLStatement globals.
    77    match s with
    8     [ LIN_St_Return ⇒ LIN_St_Return ? globals
    9     | LIN_St_Sequential instr _ ⇒ LIN_St_Sequential ? globals instr it
     8    [ Joint_St_Return ⇒ Joint_St_Return ? globals
     9    | Joint_St_Sequential instr _ ⇒ Joint_St_Sequential ? globals instr it
    1010    ].
Note: See TracChangeset for help on using the changeset viewer.