From 04c19bc7ccae1ce8e20733c075df5e9d6c448fc4 Mon Sep 17 00:00:00 2001
From: manuel <manuel@mausz.at>
Date: Wed, 29 Jun 2011 03:01:35 +0200
Subject: add replaceabality test

---
 eiffel-fragen/replaceability/base.e             | 13 ++++++++++++
 eiffel-fragen/replaceability/derived.e          | 25 ++++++++++++++++++++++
 eiffel-fragen/replaceability/derived2.e         | 28 +++++++++++++++++++++++++
 eiffel-fragen/replaceability/replaceability.ecf | 21 +++++++++++++++++++
 eiffel-fragen/replaceability/test.e             | 26 +++++++++++++++++++++++
 5 files changed, 113 insertions(+)
 create mode 100644 eiffel-fragen/replaceability/base.e
 create mode 100644 eiffel-fragen/replaceability/derived.e
 create mode 100644 eiffel-fragen/replaceability/derived2.e
 create mode 100644 eiffel-fragen/replaceability/replaceability.ecf
 create mode 100644 eiffel-fragen/replaceability/test.e

(limited to 'eiffel-fragen/replaceability')

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
-- 
cgit v1.2.3