added postcondition

This commit is contained in:
Jocelyn Fiat 2024-06-19 08:36:35 +02:00
parent fe5a7d220e
commit d551f35d2f

View File

@ -59,6 +59,8 @@ feature {NONE} -- Initialization
default_create default_create
set_target (a_target) -- calls `draw' set_target (a_target) -- calls `draw'
-- draw -- draw
ensure
target_imp /= Void
end end
create_interface_objects create_interface_objects
@ -252,6 +254,7 @@ feature -- Element change
draw draw
ensure ensure
has_target: has_target (a_target) has_target: has_target (a_target)
target_imp /= Void
end end
set_parent_view (a_view: VIEW) set_parent_view (a_view: VIEW)