/[eiffelstudio]/branches/eth/eve/Src/framework/eiffel2boogie/tests/advanced/functional/a_functional.e
ViewVC logotype

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/tests/advanced/functional/a_functional.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 93597 - (show annotations)
Tue Dec 3 00:48:44 2013 UTC (5 years, 10 months ago) by julian
File size: 600 byte(s)
AutoProof: special translation for lemma and functional
1 class A_FUNCTIONAL
2
3 feature
4
5 not_functional1
6 note
7 status: functional
8 do
9 end
10
11 not_functional2: INTEGER
12 note
13 status: functional
14 local
15 a: INTEGER
16 do
17 a := 1
18 Result := a
19 end
20
21 call_not_functional
22 local
23 a: INTEGER
24 do
25 not_functional1
26 a := not_functional2
27 end
28
29 functional1: INTEGER
30 note
31 status: functional
32 do
33 Result := 7
34 end
35
36 functional2 (a: INTEGER): INTEGER
37 note
38 status: functional
39 do
40 Result := a + 4
41 end
42
43 call_functional
44 do
45 check functional1 = 7 end
46 check functional2 (1) = 5 end
47 check functional2 (2) = 6 end
48 end
49
50 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23