Derivation of REPEAT loop inference rule

Here is an alternate method for deriving the REPEAT loop inference rule. It starts with the WHILE loop inference rule, and the semantic equivalence of a REPEAT and an "unrolled" WHILE.

Thanks to Dean Herington for the derivation.


Consider a `repeat loop' construct:

	repeat S until B

Its inference rule as derived by the "flowchart" method is:

	{ P } S { Q }, (Q and ~B) ==> P
	----------------------------------
	{ P } repeat S until B { Q and B }

Let's derive the same inference rule by defining the repeat loop construct
to be equivalent to:

	S; while ~B do S

1.  { P } S { Q }			assume
2.  (Q and ~B) ==> P			assume
3.  { Q and ~B } S { Q }		restrict the precondition of 1 using 2
4.  { Q } while ~B do S { Q and B }	apply `while' rule to 3
5.  { P } S; while ~B do S { Q and B }	compose 1 and 4
6.  { P } repeat S until B { Q and B }	recast 5 using definition of `repeat'

Thus, given 1 and 2 we may conclude 6.