Skip to content

Clean B

Khuu Minh Thang requested to merge mtk-cleanB into master

Closes #477 (closed)

  • updating invariant of address_space_typing, browse_treatment_context, translate_browse_path_1_i, channel_mgr_1_i
  • rewriting spec of local op in address_space_i
  • updating postcond browse_treatment_result_bs
  • rewriting spec of op in browse_treatment and browse_treatment_i
  • Seperating iterator op from browse_treatment by creating translate_browse_path_result_it
Edited by Vincent Monfort

Merge request reports