deferred class
	TEST1

feature

	s: detachable STRING

invariant
	s_not_void: s = Void

end