Bug in KI_PLATFORM?

I think there is a bug in the postcondition of Boolean_bits in 
ki_platform.ge revision 1.9. Boolean_bytes is a once routine in 
KL_PLATFORM that depends on Boolean_bits (using VE or SE). But the 
postcondition of Boolean_bits uses the result of Boolean_bytes. Here 
is the definition of Boolean_bits in KI_PLATFORM

Boolean_bits: INTEGER is
    -- Number of bits in a value of type BOOLEAN
  deferred
  ensure
    large_enough: Result >= 1
    small_enough: Result <= Boolean_bytes * Byte_bits
  end

Notice how this is different from the postcondition in Character_bits 
for example:

Character_bits: INTEGER is
    -- Number of bits in a value of type CHARACTER
  deferred
  ensure
    -- Note: Postcondition commented out to avoid recursive
    -- call in once-function in KL_PLATFORM:
    -- definition: Result = Character_bytes * Byte_bits
    more_than_byte: Result >= Byte_bits
  end

I think Boolean_bits was just missed.

Brian






------------------------ Yahoo! Groups Sponsor --------------------~--> 
Fair play? Video games influencing politics. Click and talk back!
http://us.click.yahoo.com/T8sf5C/tzNLAA/TtwFAA/saFolB/TM
--------------------------------------------------------------------~-> 

To Post a message, send it to:   [email protected]
To Unsubscribe, send a blank message to: [email protected] 
Yahoo! Groups Links

<*> To visit your group on the web, go to:
    http://groups.yahoo.com/group/gobo-eiffel/

<*> To unsubscribe from this group, send an email to:
    [email protected]

<*> Your use of Yahoo! Groups is subject to:
    http://docs.yahoo.com/info/terms/