From b674dbddf70c630f1b290ac9a72646425ba76115 Mon Sep 17 00:00:00 2001 From: jvelilla Date: Fri, 8 Aug 2008 11:12:27 +0000 Subject: [PATCH] Add precondition in query i_th Remove infix "@" which is deprecated now. Add invariant for values to show that it is always not Void. Add postcondition of add. --- json/json_array.e | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/json/json_array.e b/json/json_array.e index 77b4aa72..ceb2af53 100644 --- a/json/json_array.e +++ b/json/json_array.e @@ -28,8 +28,10 @@ feature -- Initialization end feature -- Access - i_th alias "[]", infix "@" (i: INTEGER):JSON_VALUE is + i_th alias "[]" (i: INTEGER):JSON_VALUE is -- Item at `i'-th position + require + is_valid_index:valid_index (i) do Result := values.i_th (i) end @@ -55,7 +57,8 @@ feature -- Change Element do values.extend(value) ensure - has_new_value:old values.count + 1 = values.count + has_new_value:old values.count + 1 = values.count and + values.has (value) end feature -- Report @@ -100,5 +103,7 @@ feature -- Report feature {NONE} --Implementation values:ARRAYED_LIST[JSON_VALUE] +invariant + value_not_void: values /= Void end