A problem with using old qualifier in post-conditions

[Finnian Reilly]

I am wondering if anyone has an answer to this conundrum. I want to have a post-condition for `order_by' that checks that if there is a valid item before the call, then the `item' still refers to to the same object after the call.

deferred class EL_CHAIN [G]

inherit
   CHAIN [G]

feature -- Basic operations

   order_by (sort_value: FUNCTION [G, COMPARABLE]; in_ascending_order: BOOLEAN)
      -- sort all elements according to `sort_value' function
      local
         l_item: G; new_index: INTEGER
      do
         if not off then
            l_item := item
         end
         across ordered_by (sort_value, in_ascending_order) as v loop
            put_i_th (v.item, v.cursor_index)
            if v.item = l_item then
               new_index := v.cursor_index
            end
         end
         if new_index > 0 then
            go_i_th (new_index)
         end
      ensure
         same_item: (old off) or else (old item) = item
      end
end

The problem is that if `old off' is `True' than I don't want the `or else' part to be evaluated, which is normally what is supposed to happen. But unfortunately the compiler is not smart enough, and because of the presence of `old item' it always evaluates `item' on entry to the routine regardless of whether `old off' is true or false. If `off' is `True' that it cause an unwanted contract violation.

Can anyone think of a work around for this problem?

-- Finnian

[r...@amalasoft.com]

Perhaps using 'index' in the postcondition might work?

R

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/eiffel-users/36e03d19-aa20-4336-96b6-09f988e4cbcd%40googlegroups.com.

[Finnian Reilly]

Perhaps using 'index' in the postcondition might work?

That thought did occur to me but you still need to refer to `old i_th' which causes the same problem if index = 0.

[jjj]

Not elegant or tested, but...

old_state: TUPLE [bool: BOOLEAN, detachable val: like item]

...

do

    if off then

        old_state := [true, Void]

    else

        old_state := [false, item]

        l_item := item

    end

...

ensure

    same_item: old_state.bool or else state.val = item

end

 

[Eric Bezault]

On 25/01/2020 21:12, Finnian Reilly wrote:
>       ensure
>          same_item: (old off) or else (old item) = item
>       end

same_item: old off or else old (if off then Void else item end) = item

--
Eric Bezault
mailto:er...@gobosoft.com
http://www.gobosoft.com

[Finnian Reilly]

On 26/01/2020 08:10, Eric Bezault wrote:

same_item: old off or else old (if off then Void else item end) = item

That won't compile on 16.05 but a good suggestion. I came up with an equivalent

        ensure
            same_item: old off or else old item_or_void = item
        end

    item_or_void: like item

        do
            if not off then

                Result := item
            end
        end

Cheers Eric!

-- 
SmartDevelopersUseUnderScoresInTheirIdentifiersBecause_it_is_much_easier_to_read

[jjj]

But in "Result := item", the call to `item' returns the current item, not the item at the beginning of the routine.

[Larry Rix]

(attached (old off) as al_old_off and then old_off) or else ( (old_item) = item)

This?

[jjj]

I could be wrong, but unless ES has changed the compiler, old statements are not evaluated upon entry to the routine, so when you call old xxx in a post condition, you get the current status or `item' not the value as it was upon routine entry.  That's why you have to save the values to non-local attributes at the start.

jjj

[Gachoud Philippe]

Is there a place we could refer to for the old statement details of implementation and semantic? After your statement the doubt comes to my mind as how it could be done without evaluating ensure old statement if its not before the routine execution :S

[Gachoud Philippe]

Could you post the implementation of your item function? could be helpful to find a workaround

[Peter Gummer]

Gachoud Philippe <ph.ga...@gmail.com> wrote:
>
> Could you post the implementation of your item function? could be helpful to find a workaround

I would assume that `item’ is the standard `item’ query inherited via CHAIN.

I thought the whole point of this thread was that when `off’ is True, calling `item’ violates its precondition. The implementation doesn’t really matter here: It’s the contract that’s important.

Peter

[Gachoud Philippe]

knowing where the contract of item breaks would help me try to help ;-)

--
You received this message because you are subscribed to the Google Groups "Eiffel Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/eiffel-users/E24E5DA0-5536-4357-8552-4D6E66882985%40gmail.com.

--

**********************************************

Philippe Gachoud

Puerto Williams 6657

Las Condes

Santiago de Chile

+56 934022210
ph.ga...@gmail.com
**********************************************

[Finnian Reilly]

> Could you post the implementation of your item function? could be helpful to find a workaround

Thanks Gachoud, I solved it already with a suggestion from Eric. I should remember to mark the post as solved in future.

same_item: old off or else old item_or_void =

item

item_or_void: like item
   do
      if not off then

         Result := item
      end
   end

but the item was failing before when trying to index and array list with index = 0

[Larry Rix]

This is what the documentation has to say:

old

Introduces an old expression. Old expressions are valid only in the postconditions of routines.

Therefore—nothing has to be saved. I believe the compiler detects the "old" keyword and creates code that saves off the reference specifically for use at the end (exit) of the routine.

From the ECMA-367 Specification:

8.9.8 Validity: Old Expression rule     Validity code: VAOX

An Old expression oe of the form old e is valid if and only if it satisfies the following conditions:

1 It appears in a Postcondition part post of a feature.

2 It does not involve Result.

3 Replacing oe by e in post yields a valid Postcondition.

Informative text

Result is otherwise permitted in postconditions, but condition 2 rules it out since its value is meaningless on entry to the routine. Condition 3 simply states that old e is valid in a postcondition if e itself is. The expression e may not, for example, involve any local variables (although it might include Result were it not for condition 2), but may refer to features of the class and formal arguments of the routine.

End

[jjj]

Well, I learned something.  I just ran a test and seems "old" constructs are now evaluated upon entry to a feature.  Thanks ES.  Great change.  Sorry, I was going from "old" data.

jjj

[Carl Langford]

Another way is suggested by the informative text of section 8.9.9 of ECMA. An "Old Exception" is created when the old(item) is evaluated on entry. This exception can be tested for in a rescue clause, a local variable set, and the procedure retried which just returns with the collection having already been resorted.