/[eiffelstudio]/branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/observer_one_to_one/f_ooo_subject_d.e
ViewVC logotype

Diff of /branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/observer_one_to_one/f_ooo_subject_d.e

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 93732 by polikarn, Thu Nov 28 19:46:33 2013 UTC revision 93733 by polikarn, Mon Dec 16 12:32:04 2013 UTC
# Line 16  feature {NONE} -- Initialization Line 16  feature {NONE} -- Initialization
16                  note                  note
17                          status: creator                          status: creator
18                  require else                  require else
                         is_open -- default: creator  
19                          modify (Current) -- default: creator                          modify (Current) -- default: creator
20                  do                  do
                         set_observers([]) -- defalt: creator  
21                          wrap -- default: creator                          wrap -- default: creator
22                  ensure then                  ensure then
23                          is_wrapped -- default: creator                          is_wrapped -- default: creator

Legend:
Removed from v.93732  
changed lines
  Added in v.93733

  ViewVC Help
Powered by ViewVC 1.1.23