Forum

I have copied some code from an example for accessing an sqlite database. It uses an agent to get the returned rows:

    check_db (input_line: STRING)

    local

        df_db:       SQLITE_DATABASE
        df_db_query: SQLITE_QUERY_STATEMENT

        test_val: STRING

    do

        test_val := "whatever"

        create df_db.make_open_read_write ("Large.db")

        create df_db_query.make ("SELECT * FROM test_table WHERE test_val =%
                    % :TEST_VAL%
                    % ;", df_db)

        check df_db_query_is_compiled: df_db_query.is_compiled
            end

        df_db_query.execute_with_arguments (agent (returned_row: SQLITE_RESULT_ROW): BOOLEAN
                do
                    if returned_row.is_null (1) then
                        insert_into_db
                    end
                end,
            << create {SQLITE_STRING_ARG}.make  (":TEST_VAL", test_val) >>)

    end -- check_db

The problem I have is that I would like to pass input_line to the procedure insert_into_db. The inline procedure used by execute_with_arguments isn't able to see any variables outside its scope, but I presume there must be a way to pass an extra parameter to it? Everything I have tried simply refuses to compile with syntax errors.

In this case, I simply want to add a database entry if it doesn't already exist, but I can easily see the case where I would want to send the returned row along with some extra data to another procedure, so it must be doable.

I'm using eiffelstudio-bin 17.05.100416-1 installed via AUR in Arch.

When I try to run the default hello world project, i have this error in the Error List tab:

C Compiler Error: The use of `tempnam' is dangerous, better use `mkstemp'   FILE_NAME.c_tempnam (elks)  132, 4  

Error code: C Compiler Error

Error: External C/C++ compilation failed.
What to do: Check the external C/C++ compilation for details.

The use of `tempnam' is dangerous, better use `mkstemp' 

And in the Output tab, under External Compilations:

Preparing C compilation
Compiling C code in C1
Compiling C code in E1
/home/rivamarco/.es/eiffel_user_files/17.05/precomp/spec/linux-x86-64/EIFGENs/base-scoop-safe/W_code/preobj.o(Cobj8.o): in function "F236_6717":
(.text+0x7d19): warning: the use of `tempnam' is dangerous, better use `mkstemp'
C compilation completed

And obviusly, hello world program doesn't work.

I'm using gcc 7.2.1+20171224-2, if it's useful.

What can i do?

Thanks in advance.

Goodmorning. I've starting using Eiffel at the University.

I have this example:

    class
      CLASS_1

    create make

    feature
      x: INTEGER

      make
        do
         x:=0
        end

      increment(inc: INTEGER)
        do
          x:=x+inc
        end

      get_x: INTEGER
        do
          Result:=x
        end
    end

----------------
class
   CLASS_2

create make_2

feature
    make_2
        do
            print("EXAMPLE")
            meth_1
        end
    meth_1
    local
        instance: CLASS_1
        i: INTEGER
    do
        create instance.make
        from
                i:=0
            until
                i<20
            loop
                instance.increment(5)
            end
            io.put_string ("The result is: ")
            io.put_integer (instance.get_x)
    end
end

Why the result is always 0? It seems like it doesn't update the value. I've read that the client class attributes are read-only. Is it true?

I want to iterate through array in a precondition. But It seems precondition part doesn't allow use of "from" and "across" syntax.

Is there a way to iterate through array in precondition?

insert_last (s: STRING)
require
    new_is_longer_than_prevs:
-- here I want to iterate through array "arr" and if length of s is longer than all other previously stored string values in array
do
    arr.force (s, arr.upper + 1)
end

I get an error unknown identifier 'start'

my code:

visit_table(table: ETABLE)
    local
        t_array: ARRAY[ARRAY[ELEMENT]]
        b_header: BOOLEAN
        row_index: INTEGER
    do
        t_array := table.t_array
        b_header := table.b_header
        table.content := "<table>"
        row_index := 0

        from t_array.start
        until t_array.off
        loop

            table.content := table.content + "<tr>"
                from t_array.item.start
                until t_array.item.off
                loop
                    if row_index = 0 and b_header = TRUE then
                        table.content := table.content + "<th>" + t_array.item.content + "</th>"
                    else
                        table.content := table.content + "<td>" + t_array.item.content + "</td>"
                    end
                end
                table.content := table.content + "</tr>"
                row_index := row_index + 1
        end

        table.content := table.content + "</table>"
    end

I just want to parse through the objects of the 2d array and wrap html tags around them.
Is there something wrong with my syntax?

Is the Result keyword automatically recognized as the return value/object?
What is the proper syntax to be used?
Unfortunately, I cannot find a clear indication from the documentation and the various examples online.

I'm trying to compile a project (see this SO question) using Gobo compiler and its tools and I'm getting error messages refering to standard library equal(..). I'm sure that error is somewhere in the code I have and not in standard library but I don't know how to get some more info from geant. I'd like to know which class, function, line of code from my code invoked equal(..) or any other standard library function which might call it. And yes, I've already tried going through all equal(..)s in my code.

Error messages I get are like this:

[CATCALL] class SQL_GENERATOR_TSQL65 (ANY,95,8): type 'STRING_8' of actual argument #1 does not conform to type 'UC_STRING' of formal argument in feature `is_equal' in class 'UC_STRING'

This points to library\free_elks\src\elks\kernel\any.e:

    frozen equal (a: detachable ANY; b: like a): BOOLEAN
        -- Are `a' and `b' either both void or attached
        -- to objects considered equal?
    do
        if a = Void then
            Result := b = Void
        else
            Result := b /= Void and then
                        a.is_equal (b) -- <<<<<<< THIS LINE
        end
    ensure
        definition: Result = (a = Void and b = Void) or else
                    ((a /= Void and b /= Void) and then
                    a.is_equal (b))
    end

I'm trying to build xplain2sql using Gobo compiler and its tools. After issuing geant compile command I get a lot of similar errors:

[CATCALL] class SQL_GENERATOR_TSQL65 (SQL_GENERATOR,2610,5): type 'STRING_8' of actual argument #1 does not conform to type 'UC_STRING' of formal argument in feature `is_equal' in class 'UC_STRING'

Above error refers to the last line of this code:

    sql_infix_expression (a_left: XPLAIN_EXPRESSION; an_operator: STRING; a_right: XPLAIN_EXPRESSION): STRING
        -- SQL expression for multiplication/division, etc.
    require
        valid_left: a_left /= Void
        valid_right: a_right /= Void
        operator_not_empty: an_operator /= Void and then not an_operator.is_empty
    local
        left_value,
        right_value: STRING
    do
        if
            an_operator.is_equal (once "+") and then

I don't know Eiffel, I just want to compile this code. There were other build errors which I was able to fix using some common sense and experience from other programming languages but I don't know how to deal with this.

In eiffel, indexing usually starts from 1, not 0.

I have following 2 attributes:

arr: ARRAY[A]

link: LINKED_LIST[B]

For array, I can make its indexing starts from 0 purposely, like following:

arr.force (value, arr.count)

so that arr[0] will be readable.

However, I did similar thing to LINKED_LIST:

link.put_i_th (value, link.count)

However this gets precondition violation.

Is there any way to make LINKED_LIST indexing from 0, not 1? so that link[0] will be accessible?

I need an example if it is possible.

I want to simulate dice roll functionality. However, I don't get what I expect. I want to get a Dice with value ranging from 1 to 6 inclusively (dice).

I tried to find it in Eiffel Documentation, but it is very hard to do.

I have following code in my do~end scope of some feature:

add (tempA, tempB)

Here, type of arguments are:

tempA: A
tempB: B

Both are declared as local variable.

And, here is prototype of feature add:

add (a: A; b: B)

The compile error I get:

Formal argument type: Generic #1
Actual argument type: detachable Generic #1

How can I instant cast type of "tempA" and "tempB" to Generic type from detachable Generic type? so that I can pass them to add feature.

I am not changing prototype, but I can change type of "tempA" and "tempB" though.

I have a feature with post-condition as follow:

checkValue (k: K): detachable V
do
...
end
ensure
some_post_condition:
    checkKey (Result)

And here is prototype of "checkKey":

checkKey (v: V): BOOLEAN

Since "Result" is type of "detachable V", and I try to pass that as parameter to "checkKey " which only accept type of "V" but not "detachable V", thus it cannot compile.

Here is what compile error says:

Argument name: v
Argument position: 1
Formal argument type: Generic #1
Actual argument type: detachable Generic #1

How can I convert detachable Generic to Generic?

I have some codes like follow:

keys: LINKED_LIST[K]
...
test
local
    tempK:K
    tempI:INTEGER
do
...
across
    keys as cursor
loop
    tempK := cursor.item
    if tempK ~ 1 then
       tempI := tempK
    end
end
...
end

"cursor.item" is type of "K". However, the real value inside there is integer type.

thus, "if tempK ~ 1 then" works fine. But "tempI := tempK" doesn't work.

How can I convert tempK's K type to integer? so that it can compile?

I have following test case:

test_different_cursor: BOOLEAN
        local
            cursor: SET_ITERATION_CURSOR[INTEGER, INTEGER]
            sets: ARRAY[SET[INTEGER, INTEGER]]
        do
            create sets.make_empty

            check  attached {SET_ITERATION_CURSOR[INTEGER, INTEGER]} d.different_cursor as current_cursor then
                cursor := current_cursor
            end
            from
            until
                cursor.after
            loop
                sets.force (cursor.item, sets.count + 1)
                cursor.forth
            end

        end

Here, in loop of from~end, I try to call Array class's force feature, but the compiler keep saying following error for that line:

    Error code: VUAR(2)

Type error: non-compatible actual argument in feature call. 
What to do: make sure that type of actual argument is compatible with
  the type of corresponding formal argument. 

Class: MY_TESTS
Feature: test_different_cursor
Called feature: force (v: [like item] G; i: INTEGER_32) from ARRAY
Argument name: v
Argument position: 1
Formal argument type: SET [INTEGER_32, INTEGER_32]
Actual argument type: TUPLE [INTEGER_32, INTEGER_32]
Line: 193
        loop
->        sets.force (cursor.item, sets.count + 1)
          cursor.forth

In this case, it seems like I need to make SET class which inherits ARRAY class and redefine force feature there. But I am not really sure it's the correct way to fix compile error. Here is what my SET class look like:

class
    SET[A, B]

create
    make

feature
    valueA: A
    valueB: B

feature
    make (first: A; second: B)
        do
            valueA := first
            valueB := second
        end
end

What I have to do in order to fix this?

I am trying to return Result type being ITERABLE[K]. All I know is that Iterable inherits from ITERATION_CURSOR, so that I made following unworking code but it doesn't compile.

obtainKey (v: V): ITERABLE[G]
    local
        myCollection: ITERABLE [G]
        myCursor:ITERATION_CURSOR[G]
    do
        create {ITERABLE[G]} myCursor
        Result := myCursor

My guess is that I have to do something like following, if it was c++ or Java,

ITERATION_CURSOR myCursor = new ITERABLE;

I don't know. My assumption could be wrong.

How can I do this kind of thing in Eiffel and make above code work?

I try to use across 1|..|list.count as j all list.i_th(z) ~ old list.i_th(z) end

but it says unknown identifier z. Whats wrong with this syntax??

I have found one case that does not make sense.

I have following feature:

test_array_deep_copy: BOOLEAN
        local
            imp, old_imp: ARRAY[STRING]
        do
            comment("Test of a deep copy.")
            create {ARRAY[STRING]} imp.make_empty
            imp.force ("Alan", 1)
            imp.force ("Mark", 2)
            imp.force ("Tom", 3)

            old_imp := imp.deep_twin
            imp[2] := "Jim"

            Result :=
                across
                    1 |..| imp.count as j
                all
                    j.item /= 2 implies imp [j.item] = old_imp [j.item]
                end
            check not Result end
        end

Since it is deep copy, that means address of imp and old_imp are different, as well as that its attributes in both two also refers to different address.

So, this "Result" after across loop, it should be false because addresses in imp and old_imp at same index are different.

So when I debug this code, it say Result is set to be false after finishing across loop.

The problem is that "check not Result" does not make false to true.

If I run workbench system, it says following:

I do not know why. "not" before "Result" in "check not Result" statement should make its whole check true, so it should say "PASSED" in workbench system, but it fails.

why is that?

I just simply test a push_at feature of container class(made by array, basically). I dont know which part of my code triggers this violation.

push_at (i: INTEGER; s: STRING)

    require
        valid_index: i  >= 1
    do
        container [i] := s

    end

In my tester

local
        con: CONTAINER

do
          create {CONTAINER}con.make
          con.push_at (1,"A")
          con.push_at (2,"B")

 Result := con.get(1) ~ "A" and con.get(2) ~ "B"
 check Result end
 end

Thanks for the help!

I have implemented a query that tells if array is sorted or not. I want to make a good postcondition that will effectively check if array is sorted using across or something else.

I tried to do this like this:

is_sorted (a: ARRAY [INTEGER]): BOOLEAN
        -- Given an array, tell if it's sorted in ascending order
    require
        array_set: a /= Void
    local
        i, j, temp: INTEGER
    do
        Result := True

        from
            i := a.lower
            j := i + 1
        invariant
            (i >= a.lower) and (i <= a.upper)
        until
            i = (a.upper) or (Result = False)
        loop
            if a[i] > a[j] then
                Result := False
            end

            i := i + 1
            j := j + 1
        variant
            a.count - i + 1
        end -- End of loop

    ensure
          -- Check if ARRAY is sorted here
    end

I tried to write something like this:

ensure
    across a as el all (el.item <= el.forth.item) end

But this obviously doesn't work because el.forth is not a query, yet a command.

How can I make this across work or should I do something else?

I've just got the ACCOUNT old sample and write some code with the STRING owner's type:

class
ACCOUNT
create
make
feature
balance: INTEGER
owner: STRING
make
    do
        create owner.make_empty
    end
minimum_balance: INTEGER = 1000
open (who: STRING)
    do
        owner := who
    end

The application's code is:

acc: ACCOUNT
make
    do
        create acc.make
        acc.open ("Jill")
        ...

It is compiled and works. After I want to change owner type to a PERSON

owner: PERSON
...
open (who: PERSON)
    do
        owner := who
    end

and I created the PERSON class just as an extension to the STRING class:

class
PERSON
inherit
STRING
end

I believe this can work in every language but seems not in Eiffel. The code fails to compile with VGCC(6) and VEVI errors. Any ideas?

I'm trying to use an agent callback concurrently. Unfortunately, no matter what I do it always seems to run sequentially instead of parallel. (without the agent it doesn't)

main class(APPLICATION):

class
    APPLICATION

inherit
    ARGUMENTS

create
    make

feature {NONE} -- Initialization

    make
            -- Run application.
        local
            a1 : separate PROCEDURE
            a2 : separate PROCEDURE
        do
            create my_counter.make (1, 100_000_000)
            create my_counter2.make (2, 100_000_000)

            launch_counter(my_counter)
            launch_counter(my_counter2)

        end

feature -- Launch

    launch_counter(c: separate COUNTER)
        do
            c.run (5, agent print_hello)
        end

    print_hello
        do
            print("Hello!%N")
        end

feature -- Access

    my_counter : separate COUNTER
    my_counter2 : separate COUNTER

end

counter class:

class
    COUNTER

inherit
    EXECUTION_ENVIRONMENT


create
    make

feature -- Initilzation
    make (i: INTEGER; delay: INTEGER)
        do
            id := i
            delay_time := delay
        end

feature -- Stuff

    run (times: INTEGER; p: separate PROCEDURE)
    local
        c : INTEGER
    do
        from
            c := times
        until
            c = 0
        loop
            print("COUNTER: " + id.out)
            p.call
            sleep(delay_time)
            c := c - 1

        end

    end

feature {NONE} -- Access

    delay_time : INTEGER
    id: INTEGER

end

expected output:

COUNTER: 1Hello!
COUNTER: 2Hello!
COUNTER: 1Hello!
etc.

actual output:

COUNTER: 1Hello!
COUNTER: 1Hello!
COUNTER: 1Hello!
COUNTER: 1Hello!
COUNTER: 1Hello!
COUNTER: 2Hello!
COUNTER: 2Hello!
COUNTER: 2Hello!
COUNTER: 2Hello!
COUNTER: 2Hello!

What would I have to change to make this run as expected?

I've seen the terms entity, variable, and argument used to describe things about Eiffel, that look quite similar to me, and I wanted to understand what is the intention behind using either term instead of the other.

Arguments — Some routines require some data in order to run. Imagine a fictitious feature foo (x, y: INTEGER; z: BOOLEAN). This routine takes 3 arguments: x, y, and z. When you call the routine, you must give it three valid arguments, for instance foo(6, 92, False). These values we passed to the routine are called actual arguments, while the placeholders defined in the definition are called formal arguments.

I've read of object fields, which specify the place inside the object structure where values are stored (either references or expanded objects).

I think the only time I saw the term variables was for local variables, inside features.

And entity seems to be a generic term for denoting a data-container with a name, so local variables, arguments, and querys (features that return some data) are all examples of entities.

And in what category would Current and Result fall? Local variables?

Could someone help me with the terminology?

1. Assume that foo: ANY is an assignable entity.
2. What happens when I do foo := create {BOOLEAN}?

It would fail always, because BOOLEAN (an expanded type) does not conform to ANY (a reference type), correct?

I again ask for help with this problem. Below is Eiffel code for B&Z's Algorithm 2, which divides 3n digits [i.e. limbs] by 2n digits. Base-10 examples: 582/73 where n = 1 and 365,437/5942 where n = 2. For completeness, the entire feature is shown below. The error is after step 3. After the code, I show values pulled during debugging. The BIG_NUMBERs are in base-256 and shown in brackets (e.g. <4,12,217> = 4*256^2 + 12*256^1 + 217*256^0).

The feature gets the correct intermediate q_hat from `school_divide' in step 3a. The error is somewhere from step 4 to the end.

Here is the Eiffel feature:

three_by_two_divide (a, a3, b: like Current): TUPLE [quot, rem: like Current]
        -- Called by `two_by_one_divide'.  It has similar structure as
        -- `div_three_halves_by_two_halfs', but the arguments to this
        -- function have type {JJ_BIG_NATURAL} instead of like `digit'.
        -- See Burnikel & Zieler, "Fast Recursive Division", pp 4-8,
        -- Algorithm 2.
    require
        b_big_enough: b.count >= div_limit
        n_not_odd: b.count \\ 2 = 0
        b_has_2n_digits: b.count = a3.count * 2
        a_has_2n_digits: a.count = a3.count * 2
    local
        n: INTEGER
        is_a_too_small: BOOLEAN
        new_a, a1, a2: like Current
        b1, b2: like Current
        tup: TUPLE [quot, rem: like Current]
        q, q1, q2, r, r1: like Current
        c, d: like Current
    do
        if a.is_zero and a3.is_zero then
            Result := [new_big_number (zero_digit), new_big_number (zero_digit)]
        else
            n := b.count // 2
                -- 1) Split `a'.
            a1 := a.partition (a.count, n + 1)
            a2 := a.partition (n.max (1), 1)
                -- 2) Split `b'.
            b1 := b.partition (b.count, n + 1)
            b2 := b.partition (n.max (1), 1)
                -- 3) Distinguish cases.
                -- 3b) We know that the quotient will contain a one
                -- in the first digit.  Remember this and adjust `a'
                -- to meet B&S's precondition by subtracting `b' from `a'.
            if a1 >= b1 then
                is_a_too_small := true
                new_a := a - b
                check
                    new_a.count = 2 * n
                        -- because must preserve leading zeroes.
                end
                    -- 1) Split the `new_a'.
                a1 := new_a.partition (new_a.count, n + 1)
                a2 := new_a.partition (n.max (1), 1)
            else
                new_a := a
            end
                -- At this point, `a' MUST be less than 'b', so continue
                -- with step 3a).
                check
                a_now_small_enough: a1 < b1
                    -- because we just subtracted the normalized denominator.
            end
                -- 3a) Compute Q = floor ([A1,A2] / B1 with remainder.
            if b1.count < div_limit then
                tup := school_divide (new_a, b1)
            else
                tup := two_by_one_divide (new_a, b1)
            end
            q := tup.quot
            r1 := tup.rem
                -- 4) D = Q * B2
            d := q * b2
                -- 5) R1 * Beta^n + A3 - D.  (The paper says "a4".)
            r1.shift_left (n)
            r := r1 + a3 - d
                -- 6) As long as R < 0, repeat
            from
            until not r.is_negative
            loop
                r := r + b
                q.decrement
            end
            if is_a_too_small then
                q.extend (one_digit)
            end
            Result := [q, r]
        end
    ensure
        quotient_has_correct_count: Result.quot.count <= b.count
        valid_result: Result.quot * b + Result.rem ~ new_combined_number (a, a3)
    end

Here is the feature outlined with values pulled from debugging. Only lines that are executed are shown in this trace:

three_by_two_divide (a = <0,15,59,225>, a3 = <60,149>, b = <243,177,116,68>)
                     65,429,126,293 / 4,088,493,124 
                     EXPECTED: 15 rem 13,236,309 = [<15>, <201,248,85>] 
    n := b.count // 2 = 2
    a1 := a.partition (a.count, n + 1) = <0,15>
    a2 := a.partition (n.max (1), 1) = <59,225>
    b1 := b.partition (b.count, n + 1) = <243,177>
    b2 := b.partition (n.max (1), 1) = <116,68>
    new_a := a
    school_divide (new_a = <0,15,59,225>, b1 = <243,177>)
                            998,369 / 62,385 = 16 rem 209 = [<16>, <209>]
    q := tup.quot = <16>
    r1 := tup.rem = <209>            CORRECT to this point.
    d := q * b2 = <16> * <116,68> = <7,68,64>  = 476,224
    r1.shift_left (n) = <209,0,0>
    r := r1 + a3 - d = <201,248,85>  WRONG should be ? <-58,53,213,227>?
    until not r.is_negative
        r := r + b  =   <> + <243,177,116,68>  NEVER CALLED, but should be
        q.decrement
    end
    Result := [<16>, <201,248,85>]   WRONG! Should be [<15>, <185,123,158,97>]

As always, help is greatly appreciated. jjj

I need another set of eyes to tell me what is wrong with my Eiffel implementation of Burnikel and Ziegler's division, specifically "Algorithm 2 - 3n/2n". The Eiffel feature is shown below. The type "like Current" is an ARRAYED_LIST [NATURAL_8]. In other words, the implementation uses digits (i.e. limbs) containing 8-bit values, so numbers are in base-256. A manual trace of a failing call follows. (Sorry the arguments are so large, but I cannot reproduce the error with shorter values.) Execution follows step 3b in this case.

Here's the problem. The algorithm seems to be fine to Step 5, where the remainder "r" ends up with more digits then the divisor. I believe the error is in step 3b, perhaps with the call to feature `ones' which is "supposed" to supply a value that is "Beta^n - 1". (Maybe I do not understand B&Z's "Beta^n" notation.

Here is the Eiffel code:

three_by_two_divide (a, a3, b: like Current): TUPLE [quot, rem: like Current]
        -- Called by `two_by_one_divide'.  It has similar structure as
        -- `div_three_halves_by_two_halfs', but the arguments to this
        -- function have type {JJ_BIG_NATURAL} instead of like `digit'.
        -- See Burnikel & Zieler, "Fast Recursive Division", pp 4-8,
        -- Algorithm 2.
    require
        n_not_odd: b.count >= div_limit and b.count \\ 2 = 0
        b_has_2n_digits: b.count = a3.count * 2
        a_has_2n_digits: a.count = a3.count * 2
    local
        n: INTEGER
        a1, a2: like Current
        b1, b2: like Current
        tup: TUPLE [quot, rem: like Current]
        q, q1, q2, r, r1: like Current
        c, d: like Current
    do
        n := b.count // 2
            -- 1) Split `a'
        a1 := new_sub_number (n + 1, a.count, a)
        a2 := new_sub_number (1, n.max (1), a)
            -- 2) Split `b'.
        b1 := new_sub_number (n + 1, b.count, b)
        b2 := new_sub_number (1, n.max (1), b)
            -- 3) Distinguish cases.
        if a1 < b1 then
                -- 3a) compute Q = floor ([A1,A2] / B1 with remainder.
            if b1.count < div_limit then
                tup := school_divide (a, b1)
            else
                tup := two_by_one_divide (a, b1)
            end
            q := tup.quot
            r1 := tup.rem
        else
                -- 3b) Q = beta^n - 1 and ...
            q := ones (n)
                -- ... R1 = [A1,A2] - [B1,0] + [0,B1] = [A1,A2] - QB1.
            r1 := a + b1
            if n > 1 then
                b1.shift_left (n)
            else
                b1.bit_shift_left (zero_digit.bit_count // 2)
            end
            r1.subtract (b1)
        end
            -- 4) D = Q * B2
        d := q * b2
            -- 5) R1 * B^n + A3 - D.  (The paper says "a4".)
        r1.shift_left (n)
        r := r1 + a3 - d
            -- 6) As long as R < 0, repeat
        from
        until not r.is_negative
        loop
            r := r + b
            q.decrement
        end
        check
            remainder_small_enough: r.count <= b.count
                -- because remainder must be less than divisor.
        end
        Result := [q, r]
    ensure
   --   n_digit_remainder: Result.rem.count = b.count // 2
        quotient_has_correct_count: Result.quot.count <= b.count // 2
    end

In the trace, the arrow points to a line I believe is bad, but I don't know what to do with it. Here is the trace:

three_by_two_divide (a = [227,26,41,95,169,93,135,110], 
                     a3 = [92,164,19,39],
                     b =  [161,167,158,41,164,0,0,0]) 

    n := b.count // 2 = 4
        -- 1) Split `a'.
    a1 := new_sub_number (n + 1, a.count, a) = [227,26,41,95]
    a2 := new_sub_number (1, n.max (1), a) = [169,93,135,110]
        -- 2) Split `b'.
    b1 := new_sub_number (n + 1, b.count, b) = [161,167,158,41]
    b2 := new_sub_number (1, n.max (1), b) = [164,0,0,0]
        -- 3b) Q = beta^n -1 and ...
--> q := ones (4) = [255,255,255,255]          <-- Is this the error?
        -- ... R1 = [A1,A2] - [B1,0] + [0,B1].
    r1 := a + b1 = [227,26,41,96,75,5,37,151]
    b1.shift_left (n) = [161,167,158,41,0,0,0,0]                        
    r1.subtract (b1) = [65,114,139,55,75,5,37,151]
    d := q * b2 = [163,255,255,255,92,0,0,0]
    r1.shift_left (n) = [227,25,135,184,172,220,37,151,0,0,0,0]   -- too big!
    r := r1 + a3 - d -= [227,25,135,184,8,220,37,152,0,164,19,39] -- too big!

I know this is long, but any help is appreciated.

I have a class, which redefines the copy feature from ANY. I would like to add a new require condition, but I get this error:

Assertion in redeclaration uses just 'require' or 'ensure'. invalid precondition feature 'copy'

Code:

copy ( other : like Current )
require
    size_is_enough: Current.max_size >= other.count
do
    -- ...
end

Explanation:

This class contains an array, and I would like to check before copying, if the object has enough space for them

(emphasis mine)

Covariant redefinition of fields and functions provides no problems, but covariant redefinition of arguments does create a problem that illegal types can be passed as arguments.

But, if redefining field and function types covariantly causes no problems, then how come redefining an argument's type covariantly can cause trouble?

Covariant redefinition equals subtyping, right? And subtypes can take the place of their supertypes!

What's the catch?