summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore1
-rw-r--r--bank-eiffel/bank.e4
-rw-r--r--eiffel-fragen/nachbedingung/application.e37
-rw-r--r--eiffel-fragen/nachbedingung/child.e25
-rw-r--r--eiffel-fragen/nachbedingung/counter.e30
-rw-r--r--eiffel-fragen/nachbedingung/nachbedingung.ecf21
-rw-r--r--eiffel-fragen/replaceability/base.e13
-rw-r--r--eiffel-fragen/replaceability/derived.e25
-rw-r--r--eiffel-fragen/replaceability/derived2.e28
-rw-r--r--eiffel-fragen/replaceability/replaceability.ecf21
-rw-r--r--eiffel-fragen/replaceability/test.e26
11 files changed, 116 insertions, 115 deletions
diff --git a/.gitignore b/.gitignore
index 0df8baa..1b080a7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,3 +13,4 @@ pacman-c++/*.pb.cc
13.*.swp 13.*.swp
14bank-eiffel/EIFGENs 14bank-eiffel/EIFGENs
15bank-eiffel/bank.data 15bank-eiffel/bank.data
16eiffel-fragen/replaceability/EIFGENs
diff --git a/bank-eiffel/bank.e b/bank-eiffel/bank.e
index 8a3fd2c..7b7105c 100644
--- a/bank-eiffel/bank.e
+++ b/bank-eiffel/bank.e
@@ -53,7 +53,7 @@ feature {NONE} -- Initialization
53 53
54feature -- Basic operations 54feature -- Basic operations
55 55
56 --fail_kovariant 56 fail_kovariant
57 local 57 local
58 retiree: RETIREE 58 retiree: RETIREE
59 student: STUDENT 59 student: STUDENT
@@ -74,7 +74,7 @@ feature -- Basic operations
74 session 74 session
75 do 75 do
76 -- das auskommentieren, dann bekommt ihr eine exception wegen kovariant (das ist ein methodenaufruf): 76 -- das auskommentieren, dann bekommt ihr eine exception wegen kovariant (das ist ein methodenaufruf):
77 fail_kovariant 77 --fail_kovariant
78 from 78 from
79 until 79 until
80 over 80 over
diff --git a/eiffel-fragen/nachbedingung/application.e b/eiffel-fragen/nachbedingung/application.e
deleted file mode 100644
index 6babd0c..0000000
--- a/eiffel-fragen/nachbedingung/application.e
+++ /dev/null
@@ -1,37 +0,0 @@
1indexing
2 description : "nachbedingung application root class"
3 date : "$Date: 2008-12-29 15:41:59 -0800 (Mon, 29 Dec 2008) $"
4 revision : "$Revision: 76432 $"
5
6class
7 APPLICATION
8
9inherit
10 ARGUMENTS
11
12create
13 make
14
15feature {NONE} -- Implementation
16 ct: COUNTER
17 ch: CHILD
18
19feature {NONE} -- Initialization
20
21 make
22 -- Run application.
23 do
24 print ("nachbedingung%N")
25
26 create ct
27 ct.set(3)
28 print ("ct " + ct.get().out + "%N")
29
30 create ch
31 ch.set(-2)
32 print ("ch " + ch.get().out + "%N")
33
34 print ("done%N")
35 end
36
37end
diff --git a/eiffel-fragen/nachbedingung/child.e b/eiffel-fragen/nachbedingung/child.e
deleted file mode 100644
index fcbe8c3..0000000
--- a/eiffel-fragen/nachbedingung/child.e
+++ /dev/null
@@ -1,25 +0,0 @@
1class
2 CHILD
3inherit
4 COUNTER
5 redefine
6 set,
7 checkval
8 end
9
10feature -- Element change
11
12 set (some_value: INTEGER) is
13 -- Set value of counter to some_value.
14 do
15 item := some_value - 10
16 ensure then
17 checkval > 0
18 end
19
20 checkval: INTEGER is
21 -- Get value of counter
22 do
23 Result := item + 20
24 end
25end
diff --git a/eiffel-fragen/nachbedingung/counter.e b/eiffel-fragen/nachbedingung/counter.e
deleted file mode 100644
index db93ce7..0000000
--- a/eiffel-fragen/nachbedingung/counter.e
+++ /dev/null
@@ -1,30 +0,0 @@
1class
2 COUNTER
3
4feature -- Access
5
6 item: INTEGER
7 -- Counter's value.
8
9feature -- Element change
10
11 set (some_value: INTEGER) is
12 -- Set value of counter to some_value.
13 do
14 item := some_value
15 ensure
16 checkval > 0
17 end
18
19 get: INTEGER is
20 -- Get value of counter
21 do
22 Result := item
23 end
24
25 checkval: INTEGER is
26 -- Get value of counter
27 do
28 Result := item
29 end
30end
diff --git a/eiffel-fragen/nachbedingung/nachbedingung.ecf b/eiffel-fragen/nachbedingung/nachbedingung.ecf
deleted file mode 100644
index d55b076..0000000
--- a/eiffel-fragen/nachbedingung/nachbedingung.ecf
+++ /dev/null
@@ -1,21 +0,0 @@
1<?xml version="1.0" encoding="ISO-8859-1"?>
2<system xmlns="http://www.eiffel.com/developers/xml/configuration-1-5-0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.eiffel.com/developers/xml/configuration-1-5-0 http://www.eiffel.com/developers/xml/configuration-1-5-0.xsd" name="nachbedingung" uuid="9ECF2BF2-5CA9-4126-B34E-978C47241CCD">
3 <target name="nachbedingung">
4 <root feature="make" class="APPLICATION"/>
5 <option warning="true">
6 <assertions precondition="true" postcondition="true" check="true" invariant="true" loop="true" supplier_precondition="true"/>
7 </option>
8 <precompile name="base_pre" location="$ISE_PRECOMP/base.ecf"/>
9 <library name="base" location="$ISE_LIBRARY/library/base/base.ecf"/>
10 <cluster name="nachbedingung" location=".\" recursive="true">
11 <file_rule>
12 <exclude>/EIFGENs$</exclude>
13 <exclude>/.svn$</exclude>
14 <exclude>/CVS$</exclude>
15 </file_rule>
16 </cluster>
17 </target>
18 <target name="nachbedingung_dotnet" extends="nachbedingung">
19 <setting name="msil_generation" value="true"/>
20 </target>
21</system>
diff --git a/eiffel-fragen/replaceability/base.e b/eiffel-fragen/replaceability/base.e
new file mode 100644
index 0000000..61f0eb9
--- /dev/null
+++ b/eiffel-fragen/replaceability/base.e
@@ -0,0 +1,13 @@
1class
2 BASE
3
4feature
5 add10(num: INTEGER): INTEGER
6 require
7 base_always_false: false -- always false
8 do
9 RESULT := num + 10
10 ensure
11 base_always_true: true
12 end
13end
diff --git a/eiffel-fragen/replaceability/derived.e b/eiffel-fragen/replaceability/derived.e
new file mode 100644
index 0000000..9a409bd
--- /dev/null
+++ b/eiffel-fragen/replaceability/derived.e
@@ -0,0 +1,25 @@
1class
2 DERIVED
3
4inherit
5 BASE
6 redefine add10
7 end
8
9feature
10 add10(num: INTEGER): INTEGER
11 require else
12 -- my precondition
13 derived_num_positive: num > 0
14 do
15 RESULT := num + 10
16 ensure then
17 -- my postcondition
18 derived_result_equals_myresult: RESULT = myresult
19 end
20
21 myresult: INTEGER
22 do
23 RESULT := 110
24 end
25end
diff --git a/eiffel-fragen/replaceability/derived2.e b/eiffel-fragen/replaceability/derived2.e
new file mode 100644
index 0000000..232ea6c
--- /dev/null
+++ b/eiffel-fragen/replaceability/derived2.e
@@ -0,0 +1,28 @@
1class
2 DERIVED2
3
4inherit
5 BASE
6 redefine add10 select add10
7 end
8 DERIVED
9 rename add10 as derived_add10
10 redefine myresult
11 end
12
13feature
14 add10(num: INTEGER): INTEGER
15 require else
16 -- stronger precondition
17 derived2_num_between_1_and_10: num >= 1 and num <= 10
18 do
19 RESULT := derived_add10(num)
20 ensure then
21 -- weaken postcondition
22 end
23
24 myresult: INTEGER
25 do
26 RESULT := 20
27 end
28end
diff --git a/eiffel-fragen/replaceability/replaceability.ecf b/eiffel-fragen/replaceability/replaceability.ecf
new file mode 100644
index 0000000..1cd86ef
--- /dev/null
+++ b/eiffel-fragen/replaceability/replaceability.ecf
@@ -0,0 +1,21 @@
1<?xml version="1.0" encoding="ISO-8859-1"?>
2<system xmlns="http://www.eiffel.com/developers/xml/configuration-1-7-0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.eiffel.com/developers/xml/configuration-1-7-0 http://www.eiffel.com/developers/xml/configuration-1-7-0.xsd" name="replaceability" uuid="ABD750A4-A528-4FEE-A7EA-37791A0D0F37">
3 <target name="replaceability">
4 <description>replaceability test</description>
5 <root class="TEST" feature="run"/>
6 <version major="0" minor="1" release="0" build="0" product="TEST"/>
7 <option warning="true" is_attached_by_default="true" void_safety="all">
8 <assertions precondition="true" postcondition="true" check="true" invariant="true" loop="true" supplier_precondition="true"/>
9 </option>
10 <setting name="console_application" value="true"/>
11 <precompile name="precompile" location="$ISE_PRECOMP\base.ecf"/>
12 <library name="base" location="$ISE_LIBRARY\library\base\base.ecf"/>
13 <cluster name="replaceability" location=".\" recursive="true">
14 <file_rule>
15 <exclude>/EIFGENs$</exclude>
16 <exclude>/CVS$</exclude>
17 <exclude>/.svn$</exclude>
18 </file_rule>
19 </cluster>
20 </target>
21</system>
diff --git a/eiffel-fragen/replaceability/test.e b/eiffel-fragen/replaceability/test.e
new file mode 100644
index 0000000..09a0821
--- /dev/null
+++ b/eiffel-fragen/replaceability/test.e
@@ -0,0 +1,26 @@
1class
2 TEST
3
4create
5 run
6
7feature {NONE} -- Initialization
8
9 run
10 local
11 base: BASE
12 derived: DERIVED
13 derived2: DERIVED2
14 ret: INTEGER
15 do
16 create base
17 create derived
18 create derived2
19
20 ret := derived.add10(100) -- works
21 --ret := derived2.add10(100) -- fails due to stronger preconditions
22
23 --ret := derived.add10(10) -- fails due to precondition
24 ret := derived2.add10(10) -- works due to weaker preconditions
25 end
26end
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-11 20:43:35 +0000