class
	A

feature

	f
		require
			re: assert ("requ: ")
			re: print_g ("requ: ", g)
		once
			check ck: assert ("chec: ") end
			check ck: print_g ("chec: ", g) end
			print (g)
		ensure
			po: assert ("post: ")
			po: print_g ("post: ", g)
		end

	g: STRING once Result := "g%N" end

	assert (where: STRING): BOOLEAN is
			--
		do
			print (where)
			print (g)
			Result := True
		end

	print_g (where, a_g: STRING): BOOLEAN is
			--
		do
			print (where)
			print (a_g)
			Result := True
		end

invariant
	inv: assert ("invaA: ")
	inv2: print_g ("invaA: ", g)

end