Sound and relatively complete total correctness proof rule for while loop
1. Context/Assertive_code; Loop_Body; confirm Inv => Q;
2. Context/Assume B_exp; Loop_Body;     Confirm Inv;
-------------------------------------------------------------------
Context / Assertive_code
Repeat
Loop_body;
maintaining Inv;
until B_Exp
Confirm Q