class
	A

feature

	f is
		do
		end

	s: STRING

invariant
	invari: not s.is_empty

end