+
Point of view
All features
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
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure