Changeset 2148 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jul 3, 2012, 4:14:45 AM (7 years ago)
Author:
sacerdot
Message:
  1. specification made more user-friendly for AssemblyProof?
  2. no more daemons in AssemblyProof?
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2147 r2148  
    707707     next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction))
    708708     ∧
    709      (nat_of_bitvector … pc < nat_of_bitvector … next_pc ∨
     709     (nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction < 2^16
     710      (*nat_of_bitvector … pc < nat_of_bitvector … next_pc*) ∨
    710711      S (nat_of_bitvector … ppc) = |instr_list| ∧ next_pc = zero …).
    711712
Note: See TracChangeset for help on using the changeset viewer.