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

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/composite/f_com_list.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 93378 - (show annotations)
Thu Nov 14 15:57:08 2013 UTC (5 years, 11 months ago) by julian
File size: 1177 byte(s)
AutoProof: continued ownership implementation.

1 note
2 description: "Subset of the interface of V_LIST needed for the example."
3 explicit: "all"
4
5 class F_COM_LIST [G]
6
7 create
8 make
9
10 feature {NONE} -- Initialization
11
12 make
13 note
14 skip: True
15 require
16 is_open -- default: creator
17 modify (Current) -- default: creator
18 do
19 ensure
20 is_wrapped -- default: creator
21 is_empty
22 end
23
24 feature -- Specification
25
26 sequence: MML_SET [G]
27 note
28 skip: True
29 status: specification
30 attribute
31 end
32
33 feature -- Access
34
35 is_empty: BOOLEAN
36 note
37 skip: True
38 require
39 modify ([])
40 do
41 ensure
42 Result = sequence.is_empty
43 end
44
45 count: INTEGER
46 note
47 skip: True
48 require
49 modify ([])
50 do
51 ensure
52 -- Result = sequence.count
53 end
54
55 item alias "[]" (i: INTEGER): G
56 note
57 skip: True
58 require
59 1 <= i and i < count
60
61 modify ([])
62 do
63 ensure
64 sequence.has (Result)
65 -- Result = sequence [i]
66 end
67
68 has (x: G) : BOOLEAN
69 note
70 skip: True
71 require
72 modify ([])
73 do
74 ensure
75 Result = sequence.has (x)
76 end
77
78 feature -- Extension
79
80 extend_back (v: G)
81 note
82 skip: True
83 require
84 is_wrapped
85 modify (Current)
86 do
87 ensure
88 sequence = old (sequence & v)
89 is_wrapped
90 end
91
92 end

Properties

Name Value
svn:eol-style native
svn:keywords Author Date ID Revision

  ViewVC Help
Powered by ViewVC 1.1.23