Changeset 2205


Ignore:
Timestamp:
Jul 18, 2012, 12:27:01 PM (5 years ago)
Author:
campbell
Message:

Get correctness.ma type checking again.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r2103 r2205  
    2626  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
    2727  | S n' ⇒
    28     if mem_set … visited l then
     28    if l∈visited then
    2929     〈add_set ? required l, 〈None …, GOTO … globals l〉 :: generated〉
    3030    else
     
    4242             visit globals g required visited' generated' l2 n' in
    4343            let required'' ≝ add_set ? required' l1 in
    44              if mem_set … visited' l1 then
     44             if l1 ∈ visited' then
    4545               〈required', generated''〉
    4646             else
     
    7171       [ None ⇒ 〈None …,x〉
    7272       | Some l ⇒
    73           〈if mem_set … required' l then Some ? l else None ?,
     73          〈if l ∈ required' then Some ? l else None ?,
    7474           x〉])
    7575    reversed.
  • src/compiler.ma

    r2116 r2205  
    4141include "ASM/ASMCostsSplit.ma".
    4242
     43axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map). (*
    4344definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
    4445λp.
     
    5152  OK ? (assembly p sigma pol).
    5253cases daemon
    53 qed.
     54qed.*)
    5455
    5556include "RTLabs/semantics.ma".
  • src/correctness.ma

    r2150 r2205  
    1111  ∀input_program.
    1212
    13   not_wrong (exec_inf … clight_fullexec input_program) →
     13  not_wrong (exec_inf … clight_fullexec input_program) →
    1414 
    1515  ∀object_code,costlabel_map,labelled,cost_map.
Note: See TracChangeset for help on using the changeset viewer.