From 0a061daf3cf101f408bb913d541bbda7ca0c52ca Mon Sep 17 00:00:00 2001
From: Harald Demel <tuempl@gmail.com>
Date: Wed, 29 Jun 2011 01:11:44 +0200
Subject: frage 3

---
 eiffel-fragen/eiffel-fragen.txt               |  6 +++++
 eiffel-fragen/nachbedingung/application.e     | 37 +++++++++++++++++++++++++++
 eiffel-fragen/nachbedingung/child.e           | 25 ++++++++++++++++++
 eiffel-fragen/nachbedingung/counter.e         | 30 ++++++++++++++++++++++
 eiffel-fragen/nachbedingung/nachbedingung.ecf | 21 +++++++++++++++
 5 files changed, 119 insertions(+)
 create mode 100644 eiffel-fragen/nachbedingung/application.e
 create mode 100644 eiffel-fragen/nachbedingung/child.e
 create mode 100644 eiffel-fragen/nachbedingung/counter.e
 create mode 100644 eiffel-fragen/nachbedingung/nachbedingung.ecf

diff --git a/eiffel-fragen/eiffel-fragen.txt b/eiffel-fragen/eiffel-fragen.txt
index 62fcef2..3fac8d0 100644
--- a/eiffel-fragen/eiffel-fragen.txt
+++ b/eiffel-fragen/eiffel-fragen.txt
@@ -16,6 +16,12 @@ Die Zusicherungen wirken sich zwangsl
 ----------------------------------------------------------------------------------------- 
 - Vorbedingungen dürfen im Untertyp nicht stärker und Nachbedingungen nicht schwächer werden, um Ersetzbarkeit zu garantieren. Der Eiffel-Compiler überprüft diese Bedingungen. Ist es (trotz eingeschalteter Überprüfung von Zusicherungen) möglich, diese Bedingungen zu umgehen? Wenn ja, wie?
 
+Ja, indem ein "redefine" von Metodhen gemacht wird, die einem "ensure" verwendet werden kann dieses schwächer werden ohne, dass der Compiler es merkt.
+
+Im Bsp:
+Der interne Zustand von "item" dürfte nie negativ werden, daher auch ct.get() nie einen negativen wert liefern.
+Bei CHILD wird der interene Zustand allerdings negativ, sichtbar durch ch.get().
+
  
 ----------------------------------------------------------------------------------------- 
 - Eiffel erlaubt kovariante Eingangsparametertypen. Unter welchen Bedingungen führt das zu Problemen, und wie äußern sich diese? Können Sie ein Programm schreiben, in dem die Verwendung kovarianter Eingangsparametertypen zu einer Exception führt?
diff --git a/eiffel-fragen/nachbedingung/application.e b/eiffel-fragen/nachbedingung/application.e
new file mode 100644
index 0000000..6babd0c
--- /dev/null
+++ b/eiffel-fragen/nachbedingung/application.e
@@ -0,0 +1,37 @@
+indexing
+	description : "nachbedingung application root class"
+	date        : "$Date: 2008-12-29 15:41:59 -0800 (Mon, 29 Dec 2008) $"
+	revision    : "$Revision: 76432 $"
+
+class
+	APPLICATION
+
+inherit
+	ARGUMENTS
+
+create
+	make
+
+feature {NONE} -- Implementation
+	ct: COUNTER
+	ch: CHILD
+
+feature {NONE} -- Initialization
+
+	make
+			-- Run application.
+		do
+			print ("nachbedingung%N")
+
+			create ct
+			ct.set(3)
+			print ("ct " + ct.get().out + "%N")
+
+			create ch
+			ch.set(-2)
+			print ("ch " + ch.get().out + "%N")
+
+			print ("done%N")
+		end
+
+end
diff --git a/eiffel-fragen/nachbedingung/child.e b/eiffel-fragen/nachbedingung/child.e
new file mode 100644
index 0000000..fcbe8c3
--- /dev/null
+++ b/eiffel-fragen/nachbedingung/child.e
@@ -0,0 +1,25 @@
+class
+               CHILD
+inherit
+	COUNTER
+		redefine
+			set,
+			checkval
+	    end
+
+feature -- Element change
+
+    set (some_value: INTEGER) is
+            -- Set value of counter to some_value.
+             do
+                         item := some_value - 10
+             ensure then
+             			 checkval > 0
+             end
+
+    checkval: INTEGER is
+    		-- Get value of counter
+    		do
+    			Result := item + 20
+    		end
+end
diff --git a/eiffel-fragen/nachbedingung/counter.e b/eiffel-fragen/nachbedingung/counter.e
new file mode 100644
index 0000000..db93ce7
--- /dev/null
+++ b/eiffel-fragen/nachbedingung/counter.e
@@ -0,0 +1,30 @@
+class
+               COUNTER
+
+feature -- Access
+
+    item: INTEGER
+                          -- Counter's value.
+
+feature -- Element change
+
+    set (some_value: INTEGER) is
+            -- Set value of counter to some_value.
+             do
+                         item := some_value
+             ensure
+             			 checkval > 0
+             end
+
+    get: INTEGER is
+    		-- Get value of counter
+    		do
+    			Result := item
+    		end
+
+    checkval: INTEGER is
+    		-- Get value of counter
+    		do
+    			Result := item
+    		end
+end
diff --git a/eiffel-fragen/nachbedingung/nachbedingung.ecf b/eiffel-fragen/nachbedingung/nachbedingung.ecf
new file mode 100644
index 0000000..d55b076
--- /dev/null
+++ b/eiffel-fragen/nachbedingung/nachbedingung.ecf
@@ -0,0 +1,21 @@
+<?xml version="1.0" encoding="ISO-8859-1"?>
+<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">
+	<target name="nachbedingung">
+		<root feature="make" class="APPLICATION"/>
+		<option warning="true">
+			<assertions precondition="true" postcondition="true" check="true" invariant="true" loop="true" supplier_precondition="true"/>
+		</option>
+		<precompile name="base_pre" location="$ISE_PRECOMP/base.ecf"/>
+		<library name="base" location="$ISE_LIBRARY/library/base/base.ecf"/>
+		<cluster name="nachbedingung" location=".\" recursive="true">
+			<file_rule>
+				<exclude>/EIFGENs$</exclude>
+				<exclude>/.svn$</exclude>
+				<exclude>/CVS$</exclude>
+			</file_rule>
+		</cluster>
+	</target>
+	<target name="nachbedingung_dotnet" extends="nachbedingung">
+		<setting name="msil_generation" value="true"/>
+	</target>
+</system>
-- 
cgit v1.2.3