Is there a way to have a separate object to be checked as ensure with the separate obj as l_obj statement?

I guess having a boolean function should work.

Any reason for that I don't understand?

set_position (a_pos: like position)
    do
        position := a_pos
        separate status_keeper as l_status_keeper_sep do
            l_status_keeper_sep.set_position (position)
        end
    ensure
        position = a_pos
        separate status_keeper as l_status_keeper_sep do -- the compiler doesn't agree with separate keyword here
            l_status_keeper_sep.position = a_pos
        end
    end

I'm a complete beginner to Eiffel and I'm implementing a linked list as an exercise. I get the following error in the feature has (which tells you if the list contains v).

Error code: VUTA(3)

Error: separate target of the Object_call is not controlled.
What to do: ensure the target of the call is controlled or is not separate.

Class: MY_LINKED_LIST [G]
Feature: has
Type: Generic #1
Line: 159
          then
->          if l_cursor_a.item.is_equal (v) then
              Result := True

The weird thing is that when I change the '.is_equal' for a '=' the error is gone. I don't know what 'controlled' in the error description means and what difference to it does make to use '=' in this context. The code is the following:

MY_LINKED_LIST[G]

class
    MY_LINKED_LIST[G]

feature -- Access

    item: G
        require
            not off
        do
            check
                off: attached cursor as l_cursor
            then
                Result := l_cursor.item
            end
        end

    first,
    last: detachable like item


feature -- Measurement

    count: INTEGER

feature -- Element change


feature -- Status report

    index: INTEGER

    before: BOOLEAN

    after: BOOLEAN

    has (v: like item): BOOLEAN
        require

        local
            l_cursor: like cursor
        do
            from
                l_cursor := first_element
            until
                not attached l_cursor or Result
            loop
                check
                    attached l_cursor as l_cursor_a
                then
                    if l_cursor_a.item.is_equal (v) then
                        Result := True
                    end
                    l_cursor := l_cursor_a.next
                end
            end
        ensure
            function_not_change_state: item = old item
        end


feature {NONE} -- Implementation

    cursor,
    first_element,
    last_element: detachable MY_CELL[G]


end -- class

MY_CELL[G]

class
    MY_CELL[G]

feature -- Access

    item: G

Is there a semantic behind not being able to have an agent into a ensure class routine or is it a current compiler restriction?

only_from_type (some_items: CHAIN[like Current]; a_type: detachable like {ENUMERATE}.measuring_point_type_generation): LINKED_LIST[like Current]
        -- extends Result with given some_items which are equal to given type
    do
        create Result.make
        across
            some_items is l_item
        loop
            check
                attached_type: attached l_item.type as l_type
            then
                if attached a_type as l_a_type and then l_type.is_equal (l_a_type) then
                    Result.extend (l_item)
                end
            end
        end
    ensure
        some_items.for_all (
            agent (an_item: like Current; a_type_2: detachable like {ENUMERATE}.measuring_point_type_generation) do
                if attached a_type_2 as l_type_2_a and then
                    attached an_item.type as l_item_type and then
                    l_item_type.is_equal (l_type_2_a)
                then
                    Result := True
                end
            end (a_type)
            )
        instance_free: Class
    end

gives following error

And I think there is a typo here, shouldn't it be Implementation constraint instead of contraint?

Error code: VUCR

Implementation contraint: The class feature only_from_type uses an inline agent.
What to do: Remove the inline agent from the code or make the feature a non-class one.
Class: MEASURING_POINT
Feature: only_from_type
Line: 183
        some_items.for_all (
->        agent (an_item: like Current; a_type_2: detachable like {ENUMERATE}.measuring_point_type_generation) do
            if attached a_type_2 as l_type_2_a and then

I know how to fix it (see my solution @bottom) but don't understand why this compilation error occurs, as in my mind, renamed attributes should be created by the Precursor into default_create. Why isn't that so?

NRJ_ENTITY

inherit
    ANY
        redefine
            default_create
        end

feature {NONE} -- Initialization

    default_create
        do
            create current_day
            create current_month
            create current_year
            Precursor
        end

feature -- Access

    current_day,
    current_month,
    current_year: ENERGY_UNIT

end

NRJ_CONSUMER

inherit
    NRJ_ENTITY

end

NRJ_GENERATOR

inherit
    NRJ_ENTITY

end

NRJ_GENERATOR_CONSUMER

inherit
    NRJ_GENERATOR
        rename
            current_day as current_day_generation,
            current_month as current_month_generation,
            current_year as current_year_generation
        redefine
            default_create
        select
            current_day_generation,
            current_month_generation,
            current_year_generation
        end
    NRJ_CONSUMER
        rename
            current_day as current_day_consumption,
            current_month as current_month_consumption,
            current_year as current_year_consumption
        redefine
            default_create
        end

feature {NONE} -- Initialize

    default_create
        do
            Precursor {NRJ_GENERATOR}
            Precursor {NRJ_CONSUMER}
        end

end

Error screenshot

Fix into NRJ_GENERATOR_CONSUMER

default_create
    do
        create current_day_consumption
        create current_month_consumption
        create current_year_consumption
        Precursor {NRJ_CONSUMER}
        Precursor {NRJ_GENERATOR}
    end

I need a cursor tree and I found CURSOR_TREE and RECURSIVE_CURSOR_TREE classes in EiffelStudio but they are deferred and I don't know how to implement them. Isn'it strange?

Id like to uncompress a file with bzip2 myFile.bz2 which class do I have to use for that?

I tried to find it into base kernel documentation which made the most sense for me and didn't find it

As far as I understood in Eiffel, the following code without assertions fails if the statement returns False

check
    i_m_alive: i.alive
then
    do_nothing
end

Maybe I'm badly using it but sometimes I'd like to check it without doing anything else.

• What is the exact behavior of this statement with and without assertions?
• Should I use a raise with an if statement?
• I sometimes try to add an else statement to the check ... then but its not implemented I'm sure for a reason, probably because there is no alternative as an exception is raised in case the statement returns True

Specially on EWF (Eiffel Web Framework) the only way I see to report an error and treat it is either to write into logs or sending the details to the referrer with some details which are sometimes not adequate to send to the user. Sending an email to the administrator is also a possiblity... I'm a bit lost, but know that the raise and Exception mecanisms is not the way Eiffel recommends to treat errors.

I'll dig further into the available documentation about that but think as me the TL;DR will be happy to have a more concise answer or more points of view about that.

How to declare an INTEGER_64 from a declared number?

("3000000000").to_integer_64

is the only way I found

What is the difference between twin and deep_twin which implies (and ensures) the difference between is_equal and is_deep_equal in eiffel?

I should test for equality two generic attributes like

a, b: G
...
Result := a.is_equal (b)

but VUTA (target rule validity) says "separate target of the Object_call is not controlled". What can I do?

I am defining like this in eiffel to swap the value. We cannot use the way we define in c++.

 swap(x,y):INTEGER
         do
            x;y := y;x
       end

How to define functions in Eiffel? I want to define heap sort but it is showing some error can someone help me clear my doubt about function.

 heapsort(array,N):INTEGER  -- heap_sort
            do
                heap_size : INTEGER
                heap_size := N

                build(array,N)

                from i := N until i >=2 loop

                    swap(array(1), array(i))
                    heap_size := heap_size-1
                    heapify(array,1,heap_size-1)

                end
            end

Is writing one rescue clause at the end of a program to end the program in Eiffel enough to handle exceptions such as pre, postconditions or invariant violations in any of the routines written in the program? Or should I write rescue clause for every function having pre and postconditions to handle exceptions?

I have read Eiffel documentation on error handling but I couldn't figure out.

Given a file input.txt, which consists of a number of elements in arrays and elements in the arrays, I should read the data and copy it to arrays in Eiffel. For example, for

3 
3 4 5
2 3 1

I should get len = 3, a1 = {3,4,5}, a2 = {2,3,1}.

I have tried the following but it was not successful

take_input
        -- Read user's input.
    local
        input: PLAIN_TEXT_FILE
        output: PLAIN_TEXT_FILE
        itr: INTEGER
    do
        create input.make_open_read ("input.txt")
        input.read_integer
        len := input.last_integer
        create output.make_open_write ("output.txt")
        create num.make_filled (0, 1, len)
        create rem.make_filled (0, 1, len)
        from
            input.start
            input.read_integer
            itr := 0
        until
            input.off
        loop
            itr := itr + 1
            if itr <= len then
                num [itr] := input.last_integer
                input.read_integer
            else
                rem [itr - len] := input.last_integer
                input.read_integer
            end
        end
        input.close
    end

Here Is there any way I can continously read the inputs rather than again starting from the Begginning of the file?

How can a mail be sent in eiffel with kernel library? which class to use?

Which library of the kernel should I use to sort a collection in eiffel?

where can I find an example of sort? are the tipical bubble sort, etc available?

Any sorter with agent would be very useful too to avoid having to do it with a comparable which is not implemented for example with PATH class

As I'd like to know if some object is into a LINKED_SET to prune it in my context, I'm unable to compare it as an object instead of its reference.

changeable_comparison_criterion: BOOLEAN
        -- May `object_comparison' be changed?
        -- (Answer: only if set empty; otherwise insertions might
        -- introduce duplicates, destroying the set property.)
    do
        Result := is_empty
    ensure then
        only_on_empty: Result = is_empty
    end

Into the SET class (as above) it seems that its not possible to change a set to compare_objects. So my questions are:

1. What is the semantic of not being able to compare objects into a SET
2. If my choice of LINKED_SET is wrong by misunderstanding of its semantic, how should I do for having a unique items collection based on object comparison and then being able to prune an item again based on object comparison again

I really don't understand as it seems to me the basics of type conformance. I have a Creation instruction lists explicit creation type which does not conform to type of target on create {JANITZA_DEVICE} l_device.make_from_file_path (a_file_path) with eiffel studio 19.5 enterprise.

SMA_INVERTER_MANAGER_CSV

class
    SMA_INVERTER_MANAGER_CSV

inherit
    SUNSPEC_DEVICE_CSV[SMA_INVERTER_MANAGER_DEVICE]

create
    make

SUNSPEC_DEVICE_CSV

deferred class
    SUNSPEC_DEVICE_CSV[G -> SUNSPEC_DEVICE create make_from_file_path end]

inherit
    CONSUMPTION_SECTOR_CSV[G]
        redefine
            process_file,
            set_header_csv
        end

feature --

    process_file (a_file_path: PATH)
        require else
            attached a_file_path.entry
            attached consumption_sector
        local
            l_device: like devices.item
        do
            check
                attached_consumption_sector: attached consumption_sector
            then
                if is_valid_file_path (a_file_path) then
                    if attached a_file_path.utf_8_name.has_substring ("janitza_UMG604") then
                        create {JANITZA_DEVICE} l_device.make_from_file_path (a_file_path) -- The compiler doesn't agree!
                    else
                        create l_device.make_from_file_path (a_file_path)
                    end
                    l_device.load_measuring_point (create_measuring_points, measuring_point_db_service, consumption_sector)
                    devices.extend (l_device)
                    Precursor (a_file_path) -- load measure_units from csv_row
                    devices.wipe_out
                end
            end
        ensure then
            devices.is_empty
        end

CONSUMPTION_SECTOR_CSV[G]

deferred class
    CONSUMPTION_SECTOR_CSV[G -> MEASURING_POINT_DEVICE]

feature -- Access

    devices: LINKED_SET[G]

SUNSPEC_DEVICE

class
    SUNSPEC_DEVICE

inherit
    MEASURING_POINT_DEVICE
        redefine
            default_create,
            set_measuring_point,
            out
        select
            serial
        end

    MODBUS_DEVICE
        rename
            serial as modbus_serial,
            set_serial as set_modbus_serial
        undefine
            make
        redefine
            default_create,
            make_from_file_path,
            name_from_file_path,
            out
        select
            set_modbus_serial
        end

create
    make_from_file_path

JANITZA_DEVICE

class
    JANITZA_DEVICE

inherit
    SUNSPEC_DEVICE
        redefine
            set_measure_units,
            name_from_file_path
        end

create
    make_from_file_path

Repeatedly inheriting from 2 classes having the same parent, I fall into the classic case of inheriting 2 times of the same attribute. I'd like to merge the 2 attributes into one and tried to do it with an undefine, but it gets me a compile error. The other solution I see is renaming the attribute from one of both parents, but as I understand each instance of my D class would have an useless attribute which is not what I want...

Error: Undefine subclause lists name of frozen feature or attribute or C external. What to do: unless you can change the status of the feature in the parent, remove its name from Undefine subclause since it cannot be undefined.

How to merge 2 attributes from repeatedly inherited classes

class A
    serial: STRING

end -- class A

class B

inherit
    A

end -- class B


class C

inherit
    A

end -- class C


class D

inherit
    B
        undefine 
            serial -- error seems to appear here in that case
        end
    C

end -- class D

How to specify when giving a generic parameter that it should implement some specific creation method? as LIST[G -> create make end] doesn't work :-(

In my particular case, * SMA_INVERTER_MANAGER_CSV has inherited from CONSUMPTION_SECTOR_MODBUS_DEVICE_CSVa list of devices as devices: LINKED_SET[G] as G -> MEASURING_POINT_MODBUS_DEVICE create make_from_file_path end.

I'd like the SMA_INVERTER_MANAGER_CSV class to be able into devices: LINKED_SET[G] to be able to have either JANITZA_DEVICE, SUNSPEC_DEVICE, ABB_DEVICE, etc. Giving the generic parameter as MEASURING_POINT_MODBUS_DEVICE seems to come out of a sense, but how do I specify that I'd like the creation method to be make_from_file_path

Hope the description is sufficient to understand, refactoring I think this question is linked -> explicit creation type not conforming to type of target

The only workaround for the moment I found working for the moment is

class
    SMA_INVERTER_MANAGER_CSV

inherit
    CONSUMPTION_SECTOR_MODBUS_DEVICE_CSV[SUNSPEC_DEVICE]

create
    make


end

but I'd like it to be

class
    SMA_INVERTER_MANAGER_CSV

inherit
    CONSUMPTION_SECTOR_MODBUS_DEVICE_CSV[MEASURING_POINT_MODBUS_DEVICE]

create
    make


end

which would generate a conformance problem because MEASURING_POINT_MODBUS_DEVICE generic parameter doesn't specify make_from_file_path as creation procedure as its deferred

I have an assignment that requires me to create an empty linked list key: LINKED_LIST [KEY], another linked list data_items_1: LINKED_LIST [DATA1] and a hash table data_items_2: HASH_TABLE [DATA2, KEY] in the constructor. The post condition that my professor put was

object_equality_for_keys: keys.object_comparison
object_equality_for_data_items_1: data_items_1.object_comparison
object_equality_for_data_items_2: data_items_2.object_comparison

When I run the program I get a contract violation. In the debugger it's always pointing to this line of code and I'm not sure why. What is the purpose of this post condition and how do I not violate this contract?

I have a method that shifts all the items, in an array, to the left by one position. In my post condition I need to ensure that my items have shifted to the left by one. I have already compared the first element of the old array to the last element of the new array. How do i across loop through the old array from 2 until count, loop through the new array from 1 until count-1 and compare them? This is my implementation so far.

        items_shifted:
                    old array.deep_twin[1] ~ array[array.count]
                        and
                    across 2 |..| (old array.deep_twin.count) as i_twin all
                        across 1 |..| (array.count-1) as i_orig  all
                            i_twin.item ~ i_orig.item
                            end
                        end



    end

I expected the result to be true but instead I get a contract violation pointing to this post condition. I have tested the method out manually by printing out the array before and after the method and I get the expected result.

As far as I understood the check with then is mandatory.

So what is the semantic of having to declare a local to avoid compiling error (object could be void)?

detachable dog: DOG

take_a_walk
    do
        check
            attached_dog: attached dog as l_dog
        then
            leash (l_dog) -- why not just leash (dog)?
            walk
        end
    end     

I'd like to create a class with both an instance_free (ensure class) feature and a deferred one.

why is that I can't call an instance_free feature in a deferred class but only on a descendant?

Don't understand the logic of that... is there for compiling reasons? or any sense I don't see? Where am I wrong with my logic?

Didn't find the answer on this doc, is the rescue clause called when redefining a feature?

Class A

class A

feature -- 

    process
        do
            do_stuff
        rescue
            on_fail
        end
end -- class

Class B

class B

inherit
    A
        redefine
            process
        end

feature -- 

    process
        do
            do_other_stuff -- do I have to call the rescue too?
        end
end -- class

I'm looking for a way to call Precursor on another feature. The context is that I redefine a routine calling another heir's feature that calls mine, and I'd like to call it explicitly. Is there a way to do something such as in java Precursor.feature_a.

If not, the only alternative I find is to write a feature_a_implementation and call it from redefined feature. Is there a particular reason not to have this mechanism? The consequences of doing that would be to define 2 times the contract of feature_a into feature_a and feature_a_implementation

Is there a way to get the project name and target at execution time or is it not stored into executable?

As mentioned on this question, there is no way to define a constant which I can redefine into a descendant.

In many of my cases, I'd like to have a constant which I can redefine. The alternatives I see to avoid a creation on each consultation which doesn't make sense would be

That's not doable

class A

feature -- Access

    Default_value: STRING = "some A value"

end -- Class


class B

inherit
    B
        redefine
            Default_value
        end

feature -- Access

    Default_value: STRING = "some B value"

end -- Class

Alternative with once instance_free

class A

feature -- Access

    Default_value: STRING
        once
            Result := "some A value"
        ensure
            instance_free: class
        end

end -- Class


class B

inherit
    B
        redefine
            Default_value
        end

feature -- Access

    Default_value: STRING
        once
            Result := "some B value"
        ensure
            instance_free: class
        end

end -- Class

As far as I understand, the once wouldn't be created with B value as the A class value would be taken

Alternative with attribute

class A

feature -- Access

    Default_value: STRING
        attribute
            Result := "some A value"
        ensure
            instance_free: class
        end

end -- Class


class B

inherit
    B
        redefine
            Default_value
        end

feature -- Access

    Default_value: STRING
        attribute
            Result := "some B value"
        ensure
            instance_free: class
        end

end -- Class

Would it be the only and good practice to do it?

I'd like to do grouping of regular expressions with eiffel. How do I do something like

l_reg.compile ("^([0-9]{3}) (rabbit[0-9]).*")
l_groups := l_reg.groups ("123 rabbit1")
my_first_rabbit := l_groups.at (2)

Didn't find any example on groups, LX_DFA_REGULAR_EXPRESSION class and other googlings

How do I concatenate a percent % string to a string?

as either do not work

s := "%%" + s + "%" 

I know its a special character but don't afford it neither do I find the doc...

UPDATE

The answer was one of my attempts, but it could stay an issue of the compiler/editor. After putting the example into the same feature, compiling, and replacing the old code the compiler did not complain anymore, but still stays as syntax coloration strange

As per this documentation, I'm trying to constrain a Generic parameter to 2 classes and need a default_create creation procedure call in my implementation.

I'm getting a Syntax error from compiler on the select clause. Why is that so?

I thought first that calling default_create will call the G one which could be a merge/renaming/etc. but seems that on that level I have to call either one of both or both renamed which makes sense for me. But why does this syntax fail?

The context and my code is following:

deferred class
    IDENTIFIABLE_CASH[G -> {IDENTIFIABLE[ANY],
                            DB_ENTITY select default_create end} create default_create end]

inherit
    DB_SERVICE_CASH[G]


feature -- Access

    cash_from_identifier (an_identifier: like {IDENTIFIABLE_DB_ENTITY[ANY]}.identifier): G
            -- Returns firt entity found like given an_identifier (like operator is used)
        local
            l_qry: COMPOSED_SQL_QUERY
        do
            across
                cash is l_item
            loop
                if l_item.identifier.is_equal(an_identifier) then
                    Result := l_item
                end
            end
            if not attached Result then
                create l_qry.make (item_prototype)
                l_qry.add_constraint (create {FIELD_CONSTRAINT}.make (Void, identifier_db_column_name, {CONSTRAINT}.Like_operator, an_identifier))
                load_entities (l_qry)
                if items.count > 0 then
                    Result := items.first
                else
                    create Result
                    check
                        item_not_found: False
                    end
                end

                cash.extend (Result)
            end
        end