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

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

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

revision 93732 by polikarn, Mon Dec 16 09:25:16 2013 UTC revision 93733 by polikarn, Mon Dec 16 12:32:04 2013 UTC
# Line 14  feature Line 14  feature
14                  require                  require
15                          s.observer = Void                          s.observer = Void
16                          s.is_wrapped -- default: public                          s.is_wrapped -- default: public
                         is_open -- default: creator  
17    
18                          modify (s)                          modify (s)
19                          modify (Current) -- default: creator                          modify (Current) -- default: creator
20                  do                  do
                         set_owns ([]) -- default: creator  
                         set_subjects ([]) -- default: creator  
                         set_observers ([]) -- default: creator  
   
21                          subject := s                          subject := s
22                          s.register (Current)                          s.register (Current)
23                          check s.inv end                          check s.inv end

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

  ViewVC Help
Powered by ViewVC 1.1.23