class Test

	def foo(i as int, j as int) as int
		require
			i implies j
		ensure
			result implies i or j
		body
			return i + j

	def main is shared
		t = Test()
		t.foo(0, 0)
		t.foo(0, 1)
		t.foo(1, 1)
		expect RequireException
			t.foo(1, 0)