Documentation MRiscX

Index🔗

Symbols

  1. \mathbb{U}_{64}

A

  1. apply_spec
  2. auto_seq

B

  1. BL_SUBSET
  2. BL_TO_WL

D

  1. DSL

H

  1. hoare_triple_up

I

  1. Instr
  2. Instr.Add­Immediate
    1. Constructor of Instr
  3. Instr.Add­Register
    1. Constructor of Instr
  4. Instr.Copy­Register
    1. Constructor of Instr
  5. Instr.Decrement
    1. Constructor of Instr
  6. Instr.Increment
    1. Constructor of Instr
  7. Instr.Jump
    1. Constructor of Instr
  8. Instr.Jump­Eq
    1. Constructor of Instr
  9. Instr.Jump­Eq­Zero
    1. Constructor of Instr
  10. Instr.Jump­Gt
    1. Constructor of Instr
  11. Instr.Jump­Le
    1. Constructor of Instr
  12. Instr.Jump­Neq
    1. Constructor of Instr
  13. Instr.Jump­Neq­Zero
    1. Constructor of Instr
  14. Instr.Load­Address
    1. Constructor of Instr
  15. Instr.Load­Immediate
    1. Constructor of Instr
  16. Instr.Load­Word­Immediate
    1. Constructor of Instr
  17. Instr.Load­Word­Reg
    1. Constructor of Instr
  18. Instr.Panic
    1. Constructor of Instr
  19. Instr.Store­Word
    1. Constructor of Instr
  20. Instr.Sub­Immediate
    1. Constructor of Instr
  21. Instr.Sub­Register
    1. Constructor of Instr
  22. Instr.XOR
    1. Constructor of Instr
  23. Instr.Xor­Immediate
    1. Constructor of Instr

P

  1. PC
  2. POST_WEAK
  3. PRE_STR
  4. Postcondition
  5. Precondition

S

  1. S_COND
  2. S_LOOP
  3. S_SEQ
  4. Structured Programming
  5. sapply_s_seq
  6. sapply_s_seq''
  7. specification_Load­Immediate

U

  1. Unstructured Programming

W

  1. WL_TO_BL
  2. weak
  3. weak transition relation