Re: [eiffel_software] preconditions in {ARRAY}.subcopy too strong?

[Emmanuel Stapf]

We can certainly weaken the precondition and have the following precondition to
allow for empty arrays for which we have `upper + 1 = lower':

        subcopy (other: ARRAY [like item]; start_pos, end_pos, index_pos: INTEGER)
                        -- Copy items of `other' within bounds `start_pos' and
`end_pos'
                        -- to current array starting at index `index_pos'.
                require
                        other_not_void: other /= Void
                        valid_start_pos: start_pos >= other.lower
                        valid_end_pos: end_pos <= other.upper
                        valid_bounds: (start_pos <= end_pos) or (start_pos =
end_pos + 1)
                        valid_index_pos: index_pos >= other.lower
                        enough_space: (upper - index_pos) >= (end_pos - start_pos)


> P.S. Execution of the workbench code shows the violated precondition but
> if I execute the code in the debugger (which I did first) I get a
> strange catcall warning. If I activate execution recording and execute
> the code in the debugger ES dies with the message
> "GLib:ERROR:gmain.c:2095:g_main_dispatch: assertion failed: (source)"

Can you submit a problem report for that which reproduces this?

Thanks,
Manu


------------------------------------------------------------------------------
Crystal Reports - New Free Runtime and 30 Day Trial
Check out the new simplified licensing option that enables unlimited
royalty-free distribution of the report engine for externally facing
server and web deployment.
http://p.sf.net/sfu/businessobjects
_______________________________________________
freeelks-devel mailing list
[hidden email]
https://lists.sourceforge.net/lists/listinfo/freeelks-devel

[Emmanuel Stapf]

> valid_bounds is not necessary because it is a consequence of
> valid_start_pos and valid_end_pos and the invariant.

Not true. If you have an empty array with lower = 1 and upper = 0. Your assertions
allows a value of start_pos which is 1 and end_pos which is -23 and if index_pos
is 1 and the Current array has a lower = 1 and upper = 50, it will pass your
assertions but frankly it does not mean very much, this is why I prefer to keep
`valid_bounds'.

Note that those discussion should go to the FreeELKS mailing list as you know
since Eiffel Software is not the only one to have a say in that matter.
 
> Do you want me to submit a problem report with respect to the
> catcall warnings?

If you are 100% sure of you, yes.

Regards,
Manu



------------------------------------------------------------------------------
Crystal Reports - New Free Runtime and 30 Day Trial
Check out the new simplified licensing option that enables unlimited
royalty-free distribution of the report engine for externally facing
server and web deployment.
http://p.sf.net/sfu/businessobjects
_______________________________________________
freeelks-devel mailing list
[hidden email]
https://lists.sourceforge.net/lists/listinfo/freeelks-devel

[Peter Gummer-2]

Emmanuel Stapf [ES] wrote:
> valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
>  

Just out of curiosity, why not simplify that precondition to this:

        valid_bounds: start_pos <= end_pos + 1


Seems a lot clearer to me.

- Peter Gummer


------------------------------------------------------------------------------
Crystal Reports - New Free Runtime and 30 Day Trial
Check out the new simplified licensing option that enables unlimited
royalty-free distribution of the report engine for externally facing
server and web deployment.
http://p.sf.net/sfu/businessobjects
_______________________________________________
freeelks-devel mailing list
[hidden email]
https://lists.sourceforge.net/lists/listinfo/freeelks-devel

[Emmanuel Stapf]

> Just out of curiosity, why not simplify that precondition to this:
>
> valid_bounds: start_pos <= end_pos + 1

I didn't want to change too much of the original so that we clearly see the
differences, but you are right it could be simplified.

Manu


------------------------------------------------------------------------------
Crystal Reports - New Free Runtime and 30 Day Trial
Check out the new simplified licensing option that enables unlimited
royalty-free distribution of the report engine for externally facing
server and web deployment.
http://p.sf.net/sfu/businessobjects
_______________________________________________
freeelks-devel mailing list
[hidden email]
https://lists.sourceforge.net/lists/listinfo/freeelks-devel