class
	TEST

feature

	make
		do
			from
			invariant
				True
			until
				False
			loop
			variant
				1
			end
			from
			invariant
				True
			variant
				2
			until
				False
			loop
			end
			from
			invariant
				a: True
			until
				False
			loop
			variant
				b: 1
			end
			from
			invariant
				a: True
			variant
				b: 2
			until
				False
			loop
			end
		end

end