Changeset 2079


Ignore:
Timestamp:
Jun 14, 2012, 11:45:49 AM (5 years ago)
Author:
sacerdot
Message:

sigma_policy_specification restyled

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2078 r2079  
    773773  λsigma: Word → Word.
    774774  λpolicy: Word → bool.
     775  sigma (zero …) = zero … ∧
    775776  ∀ppc: Word. ∀ppc_ok.
    776777    let instr_list ≝ \snd program in
     
    780781    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
    781782    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
    782      sigma (zero …) = zero …
    783      ∧
    784       (nat_of_bitvector … ppc ≤ |instr_list| →
     783     (nat_of_bitvector … ppc ≤ |instr_list| →
    785784       next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction)))
    786785     ∧       
Note: See TracChangeset for help on using the changeset viewer.