add replaceabality test

5 files changed, 113 insertions, 0 deletions

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 @@
+class
+        BASE
+
+feature
+        add10(num: INTEGER): INTEGER
+                require
+                        base_always_false: false -- always false
+                do
+                        RESULT := num + 10
+                ensure
+                        base_always_true: true
+                end
+end
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 @@
+class
+        DERIVED
+
+inherit
+        BASE
+                redefine add10
+                end
+
+feature
+        add10(num: INTEGER): INTEGER
+                require else
+                        -- my precondition
+                        derived_num_positive: num > 0
+                do
+                        RESULT := num + 10
+                ensure then
+                        -- my postcondition
+                        derived_result_equals_myresult: RESULT = myresult
+                end
+
+        myresult: INTEGER
+                do
+                        RESULT := 110
+                end
+end
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 @@
+class
+        DERIVED2
+
+inherit
+        BASE
+                redefine add10 select add10
+                end
+        DERIVED
+                rename add10 as derived_add10
+                redefine myresult
+                end
+
+feature
+        add10(num: INTEGER): INTEGER
+                require else
+                        -- stronger precondition
+                        derived2_num_between_1_and_10: num >= 1 and num <= 10
+                do
+                        RESULT := derived_add10(num)
+                ensure then
+                        -- weaken postcondition
+                end
+
+        myresult: INTEGER
+                do
+                        RESULT := 20
+                end
+end
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 @@
+<?xml version="1.0" encoding="ISO-8859-1"?>
+<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">
+        <target name="replaceability">
+                <description>replaceability test</description>
+                <root class="TEST" feature="run"/>
+                <version major="0" minor="1" release="0" build="0" product="TEST"/>
+                <option warning="true" is_attached_by_default="true" void_safety="all">
+                        <assertions precondition="true" postcondition="true" check="true" invariant="true" loop="true" supplier_precondition="true"/>
+                </option>
+                <setting name="console_application" value="true"/>
+                <precompile name="precompile" location="$ISE_PRECOMP\base.ecf"/>
+                <library name="base" location="$ISE_LIBRARY\library\base\base.ecf"/>
+                <cluster name="replaceability" location=".\" recursive="true">
+                        <file_rule>
+                                <exclude>/EIFGENs$</exclude>
+                                <exclude>/CVS$</exclude>
+                                <exclude>/.svn$</exclude>
+                        </file_rule>
+                </cluster>
+        </target>
+</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 @@
+class
+        TEST
+
+create
+        run
+
+feature {NONE} -- Initialization
+
+        run
+                local
+                        base: BASE
+                        derived: DERIVED
+                        derived2: DERIVED2
+                        ret: INTEGER
+                do
+                        create base
+                        create derived
+                        create derived2
+
+                        ret := derived.add10(100) -- works
+                        --ret := derived2.add10(100) -- fails due to stronger preconditions
+
+                        --ret := derived.add10(10) -- fails due to precondition
+                        ret := derived2.add10(10) -- works due to weaker preconditions
+                end
+end