First, let's derive a rule for repeat:

           {P and (not e)} S {P}
   -----------------------------------------
   {P and (not e)} repeat S until e {P and e}


This rule is justified by the following fact:

	repeat S until e == S; while (not e) do S

and the rules for ; and while

                                           {P and (not e)} S {P}
                                     --------------------------------
{P and (not e)} S {P}                {P} while (not e) do S {P and e}  
------------------------------------------------------------------------
  {P and (not e)} S; while (not e) do S {P and e}


Now we can use the new rule to prove the following:

    { x>=0 AND y>5 } x=x+y { x>=0 }       { x>=0 } y=y-1 { x>=0 }
    -------------------------------------------------------------
            { x>=0 AND y>5 } x=x+y; y=y-1 { x>=0 }
  -----------------------------------------------------------------
  { x>=0 AND y>5 } repeat x=x+y; y=y-1 until y<=5 { x>=0 AND y<=5 }