class interface KL_PLATFORM
feature(s) from GENERAL
-- Access :
generating_type: STRING
-- Name of current object's generating type (type of
-- which it is a direct instance).
generator: STRING
-- Name of current object's generating class (base class
-- of the type of which it is a direct instance).
stripped (other: GENERAL): like other
-- Newly created object with fields copied from current object,
-- but limited to attributes of type of other.
require
conformance: conforms_to(other)
ensure
stripped_to_other: Result.same_type(other)
feature(s) from GENERAL
-- Status report :
conforms_to (other: GENERAL): BOOLEAN
-- Is dynamic type of Current a descendant of dynamic type of
-- other ?
--
-- Note: because of automatic conversion from expanded to reference
-- type when passing argument other, do not expect a correct
-- behavior with expanded types.
require
not is_expanded_type;
other_not_void: other /= Void
same_type (other: GENERAL): BOOLEAN
-- Is type of current object identical to type of other ?
require
not is_expanded_type;
other_not_void: other /= Void
ensure
definition: Result = (conforms_to(other) and other.conforms_to(Current))
feature(s) from GENERAL
-- Comparison :
equal (some: ANY; other: like some): BOOLEAN
-- Are some and other both Void or attached to
-- objects considered equal ?
ensure
definition: Result = (some = Void and other = Void) or else some /= Void and other /= Void and then some.is_equal(other)
is_equal (other: like Current): BOOLEAN
-- Is other attached to an object considered equal to
-- current object ?
require
other_not_void: other /= Void
ensure
consistent: standard_is_equal(other) implies Result;
symmetric: Result implies other.is_equal(Current)
standard_equal (some: ANY; other: like some): BOOLEAN
-- Are some and other both Void or attached to
-- field-by-field objects of the same type ?
-- Always use the default object comparison criterion.
ensure
definition: Result = (some = Void and other = Void) or else some /= Void and other /= Void and then some.standard_is_equal(other)
standard_is_equal (other: like Current): BOOLEAN
-- Are Current and other field-by-field identical?
require
other /= Void
ensure
symmetric: Result implies other.standard_is_equal(Current)
feature(s) from GENERAL
-- Deep Comparison :
deep_equal (some: ANY; other: like some): BOOLEAN
-- Are some and other either both Void or attached to
-- recursively isomorphic object structures ?
ensure
shallow_implies_deep: standard_equal(some,other) implies Result;
same_type: Result implies some.same_type(other);
symmetric: Result implies deep_equal(other,some)
feature(s) from GENERAL
-- Deep Comparison :
standard_deep_equal (some: ANY; other: like some): BOOLEAN
-- Are some and other either both Void or attached to
-- recursively isomorphic object structures ?
ensure
shallow_implies_deep: standard_equal(some,other) implies Result;
same_type: Result implies some.same_type(other);
symmetric: Result implies deep_equal(other,some)
is_deep_equal (other: like Current): BOOLEAN
-- Is Current recursively isomorph with other ?
require
other_not_void: other /= Void
ensure
symmetric: Result implies other.is_deep_equal(Current)
feature(s) from GENERAL
-- Duplication :
clone (other: ANY): like other
-- When argument other is Void, return Void
-- otherwise return other.twin.
ensure
equal: equal(Result,other)
twin: like Current
-- Return a new object with the dynamic type of Current.
-- Before being returned, the new object is initialized using
-- feature copy (Current is passed as the argument).
-- Thus, when feature copy of GENERAL is not redefined,
-- twin has exactly the same behaviour as standard_twin.
ensure
equal: Result.is_equal(Current)
copy (other: like Current)
-- Update current object using fields of object attached
-- to other, so as to yield equal objects.
require
other_not_void: other /= Void
ensure
is_equal: is_equal(other)
standard_clone (other: ANY): like other
-- Void if other is Void; otherwise new object
-- field-by-field identical to other.
-- Always use the default copying semantics.
ensure
equal: standard_equal(Result,other)
standard_twin: like Current
-- Return a new object with the dynamic type of Current.
-- Before being returned, the new object is initialized using
-- feature standard_copy (Current is passed as the argument).
standard_copy (other: like Current)
-- Copy every field of other onto corresponding field of
-- current object.
require
other_not_void: other /= Void
ensure
standard_is_equal(other)
feature(s) from GENERAL
-- Deep Duplication :
deep_clone (other: GENERAL): like other
-- Void if other is Void: otherwise, new object structure
-- recursively duplicated from the one attached to other.
ensure
deep_equal: deep_equal(other,Result)
feature(s) from GENERAL
-- Basic operations :
default: like Current
-- Default value of current type.
default_pointer: POINTER
-- Default value of type POINTER (avoid the need to
-- write p.default for some p of type POINTER).
ensure
Result = Result.default
default_rescue
-- Handle exception if no Rescue clause.
-- (Default: do nothing.)
do_nothing
-- Execute a null action.
feature(s) from GENERAL
-- Input and Output :
io: STD_INPUT_OUTPUT
-- Handle to standard file setup.
-- To use the standard input/output file.
-- Has type STD_FILES in ELKS 95.
ensure
Result /= Void
std_input: STD_INPUT
-- To use the standard input file.
std_output: STD_OUTPUT
-- To use the standard output file.
std_error: STD_ERROR
-- To use the standard error file.
feature(s) from GENERAL
-- Object Printing :
print (some: GENERAL)
-- Write terse external representation of some on
-- standard_output.
-- To customize printing, one may redefine
-- fill_tagged_out_memory or out_in_tagged_out_memory (see
-- for example how it works in class COLLECTION).
-- Not frozen in ELKS 95.
print_on (file: OUTPUT_STREAM)
-- Default printing of current object on a file.
-- One may redefine fill_tagged_out_memory or
-- out_in_tagged_out_memory to adapt the behavior of
-- print_on.
--
tagged_out: STRING
-- New string containing printable representation of current
-- object, each field preceded by its attribute name, a
-- colon and a space.
out: STRING
-- Create a new string containing terse printable
-- representation of current object.
out_in_tagged_out_memory
-- Append terse printable represention of current object
-- in tagged_out_memory.
tagged_out_memory: STRING
fill_tagged_out_memory
-- Append a viewable information in tagged_out_memory in
-- order to affect the behavior of out, tagged_out, etc.
feature(s) from GENERAL
-- Basic named file handling :
file_tools: FILE_TOOLS
file_exists (path: STRING): BOOLEAN
-- True if path is an existing readable file.
require
path /= Void
remove_file (path: STRING)
require
path /= Void
rename_file (old_path, new_path: STRING)
require
old_path /= Void;
new_path /= Void
feature(s) from GENERAL
-- Access to command-line arguments :
argument_count: INTEGER
-- Number of arguments given to command that started
-- system execution (command name does not count).
ensure
Result >= 0
argument (i: INTEGER): STRING
-- i th argument of command that started system execution
-- Gives the command name if i is 0.
require
i >= 0;
i <= argument_count
ensure
Result /= Void
command_arguments: FIXED_ARRAY[STRING]
-- Give acces to arguments command line including the
-- command name at index 0.
ensure
not Result.empty
get_environment_variable (name: STRING): STRING
-- To get the value of a system environment variable
-- (like "PATH" on Unix for example).
-- Gives Void when system variable name is undefined.
require
name /= Void
feature(s) from GENERAL
-- System calls and crashs :
crash
-- Print Run Time Stack and then exit with exit_failure_code.
trace_switch (flag: BOOLEAN)
-- May be used in combination with option "-trace" of
-- command compile_to_c (see compile_to_c.hlp for
-- details).
system (system_command_line: STRING)
-- To execute a system_command_line as for example, "ls -l" on UNIX.
die_with_code (code: INTEGER)
-- Terminate execution with exit status code code.
-- Do not print any message.
-- Note: you can use predefined exit_success_code or
-- exit_failure_code as well as another code you need.
exit_success_code: INTEGER
exit_failure_code: INTEGER
feature(s) from GENERAL
-- Maths constants :
Pi: DOUBLE
Evalue: DOUBLE
Deg: DOUBLE
-- Degrees/Radian
Phi: DOUBLE
-- Golden Ratio
feature(s) from GENERAL
-- Character names :
Ctrl_a: CHARACTER
Ctrl_b: CHARACTER
Ctrl_c: CHARACTER
Ctrl_d: CHARACTER
Ctrl_e: CHARACTER
Ctrl_f: CHARACTER
Ctrl_g: CHARACTER
Ch_bs: CHARACTER
Ch_tab: CHARACTER
Ctrl_j: CHARACTER
Ctrl_k: CHARACTER
Ctrl_l: CHARACTER
Ctrl_m: CHARACTER
Ctrl_n: CHARACTER
Ctrl_o: CHARACTER
Ctrl_p: CHARACTER
Ctrl_q: CHARACTER
Ctrl_r: CHARACTER
Ctrl_s: CHARACTER
Ctrl_t: CHARACTER
Ctrl_u: CHARACTER
Ctrl_v: CHARACTER
Ctrl_w: CHARACTER
Ctrl_x: CHARACTER
Ctrl_y: CHARACTER
Ctrl_z: CHARACTER
Ch_del: CHARACTER
feature(s) from GENERAL
-- Should not exist :
not_yet_implemented
feature(s) from GENERAL
-- For ELS Compatibility :
id_object (id: INTEGER): ANY
-- Object for which object_id has returned id;
-- Void if none.
require
id /= 0
object_id: INTEGER
-- Value identifying current reference object.
require
not is_expanded_type
feature(s) from GENERAL
-- The Guru section :
to_pointer: POINTER
-- Explicit conversion of a reference into POINTER type.
require
not is_expanded_type
is_expanded_type: BOOLEAN
-- Target is not evaluated (Statically computed).
-- Result is true if target static type is an expanded type.
-- Useful for formal generic type.
is_basic_expanded_type: BOOLEAN
-- Target is not evaluated (Statically computed).
-- Result is true if target static type is one of the
-- following types: BOOLEAN, CHARACTER, INTEGER, REAL,
-- DOUBLE or POINTER.
ensure
Result implies is_expanded_type
object_size: INTEGER
-- Gives the size of the current object at first level
-- only (pointed-to sub-object are not concerned).
-- The result is given in number of CHARACTER.
feature(s) from GENERAL
-- Implementation of GENERAL (do not use directly) :
se_assigned_from (other: GENERAL): BOOLEAN
-- To implement conforms_to (must only be called inside
-- conforms_to because of VJRV rule).
require
not is_expanded_type
feature(s) from PLATFORM
-- Maximum :
Maximum_character_code: INTEGER
-- Smallest and largest supported codes for CHARACTER values
Maximum_integer: INTEGER
-- Largest supported value of type INTEGER.
ensure
meaningful: Result >= 0
Maximum_real: REAL
-- Largest supported value of type REAL.
ensure
meaningful: Result >= 0.0
Maximum_double: DOUBLE
-- Largest supported value of type DOUBLE.
ensure
meaningful: Result >= Maximum_real
feature(s) from PLATFORM
-- Minimum :
Minimum_character_code: INTEGER
-- Smallest supported code for CHARACTER values.
Minimum_integer: INTEGER
-- Smallest supported value of type INTEGER.
ensure
meaningful: Result <= 0
Minimum_double: DOUBLE
-- Smallest supported value of type DOUBLE.
ensure
meaningful: Result <= 0.0
Minimum_real: REAL
-- Smallest supported value of type REAL.
ensure
meaningful: Result <= 0.0
feature(s) from PLATFORM
-- Bits :
Boolean_bits: INTEGER
-- Number of bits in a value of type BOOLEAN.
ensure
meaningful: Result >= 1
Character_bits: INTEGER
-- Number of bits in a value of type CHARACTER.
ensure
meaningful: Result >= 1;
large_enough: 2 ^ Result >= Maximum_character_code
Integer_bits: INTEGER
-- Number of bits in a value of type INTEGER.
ensure
meaningful: Result >= 1
Real_bits: INTEGER
-- Number of bits in a value of type REAL.
ensure
meaningful: Result >= 1
Double_bits: INTEGER
-- Number of bits in a value of type DOUBLE.
ensure
meaningful: Result >= 1;
meaningful: Result >= Real_bits
Pointer_bits: INTEGER
-- Number of bits in a value of type POINTER.
end of KL_PLATFORM