+
Point of view
CONTAINER
deferred class WIDGET
require
- p = Void implies parent /= Void
- p /= Void implies parent = Void
- p /= Void implies p.has_child(Current)
ensure
frozen
effective function
frozen
effective function
frozen
effective function
frozen
effective function
frozen
effective function