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

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/iterator/f_i_array.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: 598 byte(s)
AutoProof: continued ownership implementation.

1 note
2 explicit: "all"
3
4 class F_I_ARRAY
5
6 create
7 make
8
9 feature
10
11 make (a_lower, a_upper: INTEGER)
12 note
13 skip: True
14 require
15 is_open
16 a_lower = 1
17 a_upper >= 0
18 modify (Current)
19 do
20 ensure
21 count = a_upper
22 is_wrapped
23 end
24
25 count: INTEGER
26
27 put (a_value, a_index: INTEGER)
28 note
29 skip: True
30 require
31 is_wrapped
32 a_index > 0
33 a_index <= count
34
35 modify (Current)
36 do
37 ensure
38 is_wrapped
39 count = old count
40 end
41
42 item alias "[]" (a_index: INTEGER): INTEGER
43 note
44 skip: True
45 require
46 not is_open
47
48 modify ([])
49 do
50 ensure
51 not is_open
52 end
53
54 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23