From 04c19bc7ccae1ce8e20733c075df5e9d6c448fc4 Mon Sep 17 00:00:00 2001 From: manuel Date: Wed, 29 Jun 2011 03:01:35 +0200 Subject: add replaceabality test --- .gitignore | 1 + bank-eiffel/bank.e | 4 +-- eiffel-fragen/nachbedingung/application.e | 37 ------------------------- eiffel-fragen/nachbedingung/child.e | 25 ----------------- eiffel-fragen/nachbedingung/counter.e | 30 -------------------- eiffel-fragen/nachbedingung/nachbedingung.ecf | 21 -------------- 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 +++++++++++++++++ 11 files changed, 116 insertions(+), 115 deletions(-) delete mode 100644 eiffel-fragen/nachbedingung/application.e delete mode 100644 eiffel-fragen/nachbedingung/child.e delete mode 100644 eiffel-fragen/nachbedingung/counter.e delete mode 100644 eiffel-fragen/nachbedingung/nachbedingung.ecf 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 diff --git a/.gitignore b/.gitignore index 0df8baa..1b080a7 100644 --- a/.gitignore +++ b/.gitignore @@ -13,3 +13,4 @@ pacman-c++/*.pb.cc .*.swp bank-eiffel/EIFGENs bank-eiffel/bank.data +eiffel-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 feature -- Basic operations - --fail_kovariant + fail_kovariant local retiree: RETIREE student: STUDENT @@ -74,7 +74,7 @@ feature -- Basic operations session do -- das auskommentieren, dann bekommt ihr eine exception wegen kovariant (das ist ein methodenaufruf): - fail_kovariant + --fail_kovariant from until 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 @@ -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 deleted file mode 100644 index fcbe8c3..0000000 --- a/eiffel-fragen/nachbedingung/child.e +++ /dev/null @@ -1,25 +0,0 @@ -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 deleted file mode 100644 index db93ce7..0000000 --- a/eiffel-fragen/nachbedingung/counter.e +++ /dev/null @@ -1,30 +0,0 @@ -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 deleted file mode 100644 index d55b076..0000000 --- a/eiffel-fragen/nachbedingung/nachbedingung.ecf +++ /dev/null @@ -1,21 +0,0 @@ - - - - - - - - - - /EIFGENs$ - /.svn$ - /CVS$ - - - - - - - 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 @@ + + + + replaceability test + + + + + + + + + /EIFGENs$ + /CVS$ + /.svn$ + + + + 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