Clean B
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